[Merged by Bors] - refactor(Probability): Make kernels a type

[YaelDillies]

Turn kernel : AddSubmonoid (α → MeasureTheory.Measure β) into Kernel : Type _. This is similar to #12386 but here to gain access to dot notation rather than for performance reasons.

---

A later PR will rename the predicates like IsMarkovKernel, IsFiniteKernel... to use dot notation.

[github-actions]

PR summary 55463f2bba

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Kernel
+ Kernel.apply_eq_measure_condKernel_of_compProd_eq
+ Kernel.condKernel_apply_eq_condKernel
+ Kernel.continuous_integral_integral
+ Kernel.indep_biSup_compl
+ Kernel.indep_biSup_limsup
+ Kernel.indep_iSup_directed_limsup
+ Kernel.indep_iSup_limsup
+ Kernel.indep_limsup_atBot_self
+ Kernel.indep_limsup_atTop_self
+ Kernel.indep_limsup_self
+ Kernel.integral_fn_integral_add
+ Kernel.integral_fn_integral_sub
+ Kernel.integral_integral_add
+ Kernel.integral_integral_add'
+ Kernel.integral_integral_sub
+ Kernel.integral_integral_sub'
+ Kernel.lintegral_fn_integral_sub
+ Kernel.measurable_lintegral_indicator_const
+ Kernel.measure_eq_zero_or_one_of_indepSet_self
+ Kernel.measure_eq_zero_or_one_or_top_of_indepSet_self
+ Kernel.measure_le_bound
+ Kernel.measure_zero_or_one_of_measurableSet_limsup
+ Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot
+ Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop
+ add_apply
+ coe_add
+ coe_nsmul
+ coe_zero
+ instAdd
+ instAddCommMonoid
+ instCovariantAddLE
+ instFunLike
+ instOrderBot
+ instPartialOrder
+ instSMulNat
+ instZero
+ instance (priority := 100) isFiniteKernel_of_isFiniteKernel_fst {κ : Kernel α (β × γ)}
+ instance (priority := 100) isFiniteKernel_of_isFiniteKernel_snd {κ : Kernel α (β × γ)}
+ instance (κ : Kernel α β) [IsSFiniteKernel κ] (f : α → β → ℝ≥0) :
+ nsmul_apply
++-- compProd_add_right
++-- compProd_zero_left
+-+- compProd
+-+- compProd_add_left
+-+- compProd_zero_right
- coeFn_add
- coeFn_zero
- instance (priority := 100) isFiniteKernel_of_isFiniteKernel_fst {κ : kernel α (β × γ)}
- instance (priority := 100) isFiniteKernel_of_isFiniteKernel_snd {κ : kernel α (β × γ)}
- instance (κ : kernel α β) [IsSFiniteKernel κ] (f : α → β → ℝ≥0) :
- instance {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] :
- kernel.apply_eq_measure_condKernel_of_compProd_eq
- kernel.condKernel_apply_eq_condKernel
- kernel.continuous_integral_integral
- kernel.indep_biSup_compl
- kernel.indep_biSup_limsup
- kernel.indep_iSup_directed_limsup
- kernel.indep_iSup_limsup
- kernel.indep_limsup_atBot_self
- kernel.indep_limsup_atTop_self
- kernel.indep_limsup_self
- kernel.instCovariantAddLE
- kernel.instOrderBot
- kernel.integral_fn_integral_add
- kernel.integral_fn_integral_sub
- kernel.integral_integral_add
- kernel.integral_integral_add'
- kernel.integral_integral_sub
- kernel.integral_integral_sub'
- kernel.lintegral_fn_integral_sub
- kernel.measurable_lintegral_indicator_const
- kernel.measure_eq_zero_or_one_of_indepSet_self
- kernel.measure_eq_zero_or_one_or_top_of_indepSet_self
- kernel.measure_le_bound
- kernel.measure_zero_or_one_of_measurableSet_limsup
- kernel.measure_zero_or_one_of_measurableSet_limsup_atBot
- kernel.measure_zero_or_one_of_measurableSet_limsup_atTop

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[RemyDegenne]

The important changes are only in Kernel.Basic, right?

[RemyDegenne]

Looks good!
bors d+

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

Thanks for the quick review!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style