Structures · Analysis
MeasureTheory.IsFiniteMeasure
A measure μ is called finite if μ univ < ∞.
- Shape
- One type argument · adds measure_univ_lt_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every MeasureTheory.IsFiniteMeasure is also a
Provided automatically by
Concrete types that are instances4
- Real
- AddCircle
- Prod
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by1,066
- MeasureTheory.measure_ne_top
- MeasureTheory.integrable_const
- ProbabilityTheory.condDistrib
- ProbabilityTheory.condExpKernel
- ProbabilityTheory.CondIndepFun
- MeasureTheory.measure_lt_top
- MeasureTheory.Measure.condKernel
- MeasureTheory.Measure.toSignedMeasure
- ProbabilityTheory.CondIndep
- ProbabilityTheory.posterior
- ProbabilityTheory.iCondIndepFun
- ProbabilityTheory.CondIndepSets
- ContinuousMap.toLp
- ProbabilityTheory.iCondIndep
- MeasureTheory.memLp_const
- ProbabilityTheory.HasCondSubgaussianMGF
- MeasureTheory.MemLp.integrable
- BoundedContinuousFunction.toLp
- ProbabilityTheory.condDistrib_def
- ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
- MeasureTheory.Lp.const
- MeasureTheory.Measure.toSignedMeasure_apply_measurable
- BoundedContinuousFunction.lintegral_lt_top_of_nnreal
- ProbabilityTheory.CondIndepSet
- MeasureTheory.MemLp.mono_exponent
- ProbabilityTheory.iCondIndepSets
- MeasureTheory.Measure.lintegral_rnDeriv_lt_top
- BoundedContinuousFunction.integrable
- MeasureTheory.Measure.sigmaFiniteSetGE
- MeasureTheory.Measure.integrable_toReal_rnDeriv
- MeasureTheory.Measure.ext_of_charFunDual
- ProbabilityTheory.condExpKernel_eq
- MeasureTheory.HasFiniteIntegral.of_bounded
- ProbabilityTheory.iCondIndepSet
- ProbabilityTheory.condExpKernel_ae_eq_condExp
- MeasureTheory.Measure.ext_of_charFun
- MeasureTheory.Measure.sigmaFiniteSetWRT'
- MeasureTheory.Measure.toSignedMeasure_sub_apply
- ProbabilityTheory.compProd_map_condDistrib
- MeasureTheory.IsFiniteMeasure.measure_univ_lt_top
- MeasureTheory.Integrable.of_bound
- MeasureTheory.MemLp.of_bound
- ProbabilityTheory.variance_add
- ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map
- MeasureTheory.condExp_const
- ProbabilityTheory.covarianceBilinDual_self_eq_variance
- MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub
- MeasureTheory.VectorMeasure.integral_const
- ProbabilityTheory.isCondKernelCDF_condCDF
- MeasureTheory.Measure.sub_apply