Structures · Analysis
ProbabilityTheory.IsFiniteKernel
A kernel is finite if every measure in its image is finite, with a uniform bound.
- Defined in
- Mathlib.Probability.Kernel.Defs
- Shape
- One type argument · adds exists_univ_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every ProbabilityTheory.IsFiniteKernel is also a
Provided automatically by
Concrete types that are instances2
- Bool
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by225
- ProbabilityTheory.posterior
- ProbabilityTheory.Kernel.condKernel
- ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure
- ProbabilityTheory.Kernel.rnDeriv_add_singularPart
- ProbabilityTheory.Kernel.integrable_density
- ProbabilityTheory.Kernel.mutuallySingular_singularPart
- MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd
- ProbabilityTheory.Kernel.bound_lt_top
- ProbabilityTheory.Kernel.setIntegral_densityProcess
- ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice
- ProbabilityTheory.absolutelyContinuous_posterior
- ProbabilityTheory.compProd_posterior_eq_map_swap
- ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd
- ProbabilityTheory.compProd_posterior_eq_swap_comp
- ProbabilityTheory.eq_condKernel_of_measure_eq_compProd
- ProbabilityTheory.Kernel.ae_eq_of_compProd_eq
- ProbabilityTheory.Kernel.condKernelUnitBorel
- ProbabilityTheory.Kernel.withDensity_rnDeriv_mutuallySingularSetSlice
- ProbabilityTheory.Kernel.integrable_densityProcess
- ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp
- ProbabilityTheory.Kernel.martingale_densityProcess
- ProbabilityTheory.IsCondKernelCDF.setLIntegral
- MeasureTheory.Measure.MutuallySingular.compProd_of_right
- ProbabilityTheory.Kernel.integral_density
- ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone
- ProbabilityTheory.setIntegral_condKernel
- ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt
- ProbabilityTheory.avgRisk_eq_lintegral_lintegral_lintegral
- ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le
- ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat
- ProbabilityTheory.Kernel.condKernelBorel
- ProbabilityTheory.setLIntegral_toKernel_univ
- ProbabilityTheory.swap_compProd_posterior
- ProbabilityTheory.Kernel.tendsto_densityProcess_limitProcess
- ProbabilityTheory.Kernel.setLIntegral_density
- ProbabilityTheory.posterior_eq_withDensity_of_countable
- ProbabilityTheory.Kernel.singularPart_eq_singularPart_measure
- ProbabilityTheory.Kernel.setLIntegral_rnDeriv
- ProbabilityTheory.Kernel.tendsto_integral_density_of_antitone
- ProbabilityTheory.Kernel.eq_rnDeriv_measure
- ProbabilityTheory.parallelProd_posterior_comp_copy_comp
- ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable
- ProbabilityTheory.IsArgminEstimator.avgRisk_eq_lintegral_iInf
- ProbabilityTheory.Kernel.densityProcess_fst_univ_ae
- ProbabilityTheory.setLIntegral_condKernel
- ProbabilityTheory.Kernel.density_ae_eq_limitProcess
- ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess
- ProbabilityTheory.Kernel.rnDerivAux_le_one
- ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel
- ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat