Structures · Analysis
ProbabilityTheory.IsSFiniteKernel
A kernel is s-finite if it can be written as the sum of countably many finite kernels.
- Defined in
- Mathlib.Probability.Kernel.Defs
- Shape
- One type argument · adds tsum_finite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances3
- Bool
- SFinKer.carrier
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by225
- ProbabilityTheory.Kernel.withDensity
- ProbabilityTheory.Kernel.compProd_apply
- ProbabilityTheory.Kernel.parallelComp_apply
- MeasureTheory.Measure.compProd_apply
- ProbabilityTheory.Kernel.singularPart
- ProbabilityTheory.Kernel.prod_apply
- ProbabilityTheory.Kernel.withDensity_apply
- ProbabilityTheory.Kernel.seq
- ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
- MeasureTheory.Measure.snd_compProd
- MeasureTheory.Measure.compProd_eq_comp_prod
- ProbabilityTheory.Kernel.withDensity_apply'
- MeasureTheory.Measure.compProd_apply_prod
- ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
- ProbabilityTheory.Kernel.ae_ae_of_ae_compProd
- ProbabilityTheory.Kernel.lintegral_compProd
- ProbabilityTheory.Kernel.kernel_sum_seq
- MeasureTheory.Measure.lintegral_compProd
- ProbabilityTheory.Kernel.prod_apply'
- ProbabilityTheory.Kernel.withDensity_of_not_measurable
- ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
- Measurable.lintegral_kernel_prod_right
- MeasureTheory.Measure.absolutelyContinuous_compProd_iff
- MeasureTheory.Integrable.integral_compProd
- ProbabilityTheory.Kernel.fst_compProd
- ProbabilityTheory.Kernel.prod_apply_prod
- MeasureTheory.Measure.compProd_map
- MeasureTheory.Measure.compProd_congr
- ProbabilityTheory.Kernel.setLIntegral_compProd
- ProbabilityTheory.Kernel.compProd_restrict
- MeasureTheory.Measure.integrable_compProd_iff
- MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'
- ProbabilityTheory.integral_compProd
- ProbabilityTheory.Kernel.map_prod_map
- MeasureTheory.Measure.AbsolutelyContinuous.compProd_right
- ProbabilityTheory.Kernel.singularPart_compl_mutuallySingularSetSlice
- MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd
- ProbabilityTheory.setIntegral_compProd
- ProbabilityTheory.Kernel.singularPart_def
- Measurable.lintegral_kernel_prod_left
- MeasureTheory.Measure.integral_compProd
- ProbabilityTheory.Kernel.parallelComp_comp_prod
- ProbabilityTheory.integrable_compProd_iff
- MeasureTheory.Measure.absolutelyContinuous_of_compProd
- MeasureTheory.Measure.ae_ae_of_ae_compProd
- ProbabilityTheory.Kernel.compProd_apply_prod
- ProbabilityTheory.Kernel.compProd_null
- MeasureTheory.Integrable.ae_of_compProd
- ProbabilityTheory.Kernel.partialTraj_eq_prod
- ProbabilityTheory.Kernel.lintegral_prod
Ancestors0
No ancestors.