Integrable

📁 Source: Mathlib/Probability/Independence/Integrable.lean

Statistics

Metric	Count
Definitions Integrable	1
Theorems isProbabilityMeasure_of_indepFun, isProbabilityMeasure_of_indepFun	2
Total	3

BoxIntegral

Definitions

Name	Category	Theorems
Integrable 📖	MathDef	9 math math: integrable_of_continuousOn, integrable_const, integrable_of_bounded_and_ae_continuous, HasIntegral.integrable, integrable_iff_cauchy_basis, integrable_iff_cauchy, integrable_zero, integrable_neg, integrable_of_bounded_and_ae_continuousWithinAt

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isProbabilityMeasure_of_indepFun 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.IndepFun	MeasureTheory.IsProbabilityMeasure	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.one_ne_top MeasureTheory.memLp_one_iff_integrable

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isProbabilityMeasure_of_indepFun 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.IndepFun	MeasureTheory.IsProbabilityMeasure	—	MeasureTheory.Measure.instOuterMeasureClass Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq ENNReal.instCanonicallyOrderedAdd exists_seq_strictAnti_tendsto NNReal.instOrderTopology NNReal.instDenselyOrdered IsStrictOrderedRing.toNoMaxOrder NNReal.instIsStrictOrderedRing TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.mp_mem MeasureTheory.ae_all_iff instCountableNat Filter.univ_mem' NNReal.instCanonicallyOrderedAdd ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LT.lt.le meas_ge_lt_top LT.lt.ne' ProbabilityTheory.IndepFun.measure_inter_preimage_eq_mul IsClosed.measurableSet isClosed_le continuous_const continuous_nnnorm MeasurableSet.univ ENNReal.mul_eq_left LT.lt.ne Set.inter_univ

---

← Back to Index