Basic

📁 Source: Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Statistics

Metric	Count
Definitions condExp, condExpUnexpander, «term__[_|_]»	3
Theorems comp_condExp_add_const_comm, comp_condExp_comm, condExp, condExpL2_ae_eq_condExp, condExpL2_ae_eq_condExp', ae_eq_condExp_of_forall_setIntegral_eq, condExp_add, condExp_ae_eq_condExpL1, condExp_ae_eq_condExpL1CLM, condExp_bot, condExp_bot', condExp_bot_ae_eq, condExp_condExp_of_le, condExp_congr_ae, condExp_congr_ae_trim, condExp_const, condExp_def, condExp_finset_sum, condExp_mono, condExp_neg, condExp_nonneg, condExp_nonpos, condExp_ofNat, condExp_of_aestronglyMeasurable', condExp_of_not_integrable, condExp_of_not_le, condExp_of_not_sigmaFinite, condExp_of_sigmaFinite, condExp_of_stronglyMeasurable, condExp_smul, condExp_sub, condExp_zero, eLpNorm_condExp_le, integrable_condExp, integral_condExp, integral_condExp_indicator, setIntegral_condExp, stronglyMeasurable_condExp, tendsto_condExpL1_of_dominated_convergence, tendsto_condExp_unique	40
Total	43

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_condExp_add_const_comm 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule Real.normedField funLike MeasureTheory.condExp	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem comp_condExp_comm Filter.univ_mem' MeasureTheory.condExp_const AddRightCancelSemigroup.toIsRightCancelAdd Filter.EventuallyEq.trans Filter.EventuallyEq.symm MeasureTheory.condExp_add integrable_comp RingHomIsometric.ids MeasureTheory.integrable_const
comp_condExp_comm 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField funLike MeasureTheory.condExp	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq integrable_comp RingHomIsometric.ids MeasureTheory.Integrable.integrableOn MeasureTheory.integrable_condExp integral_comp_comm MeasureTheory.Integrable.restrict MeasureTheory.setIntegral_condExp Continuous.comp_aestronglyMeasurable cont MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.stronglyMeasurable_condExp MeasureTheory.condExp_of_not_sigmaFinite map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass MeasureTheory.condExp_of_not_le

MeasureTheory

Definitions

Name	Category	Theorems
condExp 📖	CompOp	142 math math: ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul, eLpNorm_condExp_le, Martingale.stoppedValue_ae_eq_restrict_eq, ProbabilityTheory.condDistrib_ae_eq_condExp, condExp_bilin_of_stronglyMeasurable_left, setIntegral_condExp, ProbabilityTheory.condIndep_iff, ContinuousLinearMap.comp_condExp_comm, ProbabilityTheory.Kernel.condExp_traj', martingale_condExp, ProbabilityTheory.condExp_ae_eq_integral_condDistrib_id, ContinuousLinearMap.comp_condExp_add_const_comm, BorelCantelli.martingalePart_process_ae_eq, condExp_ae_eq_restrict_zero, condExp_bilin_of_aestronglyMeasurable_right, MemLp.condExpL2_ae_eq_condExp, ProbabilityTheory.condExp_ae_eq_integral_condDistrib, condExp_congr_ae_trim, integrable_condExp, condExp_stopping_time_ae_eq_restrict_eq, ProbabilityTheory.iCondIndep_iff, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, Filtration.condExp_condExp, condExp_smul_of_aestronglyMeasurable_right, condExp_zero, Integrable.tendsto_eLpNorm_condExp, ProbabilityTheory.condIndepSets_singleton_iff, BorelCantelli.predictablePart_process_ae_eq, ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, condExp_mul_of_aestronglyMeasurable_right, condExp_of_stronglyMeasurable, Integrable.tendsto_ae_condExp, Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range, condExp_finset_sum, condExp_neg, condExp_mul_of_stronglyMeasurable_right, ProbabilityTheory.condExpKernel_ae_eq_condExp', condExp_bilin_of_aestronglyMeasurable_left, condExp_condExp_of_le, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, condExp_congr_ae, ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel, condExp_ofNat, condExp_stronglyMeasurable_simpleFunc_mul, ProbabilityTheory.condIndepSet_iff, condExp_mul_of_aestronglyMeasurable_left, condExp_nonneg, Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le, ProbabilityTheory.integral_condVar_add_variance_condExp, condExp_mono, condExp_stronglyMeasurable_simpleFunc_bilin, condExp_of_not_integrable, condExp_of_not_le, condExp_indicator, ProbabilityTheory.iCondIndepSets_singleton_iff, condExp_stronglyMeasurable_mul_of_bound, ProbabilityTheory.condExp_set_generateFrom_singleton, ProbabilityTheory.condExp_generateFrom_singleton, condExp_smul, condExp_bot, Martingale.stoppedValue_min_ae_eq_condExp, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel, ProbabilityTheory.Kernel.condExp_traj, condExp_def, tendsto_sum_indicator_atTop_iff', condExp_const, ProbabilityTheory.condIndepSets_iff, ProbabilityTheory.iCondIndepSet_iff, condExp_add, condExp_ae_eq_condExpL1, MemLp.condExp, ProbabilityTheory.condVar_ae_le_condExp_sq, integral_condExp, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib, setIntegral_abs_condExp_le, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel', condExp_ae_eq_condExpL1CLM, tendsto_ae_condExp, condExp_nonpos, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup, rnDeriv_ae_eq_condExp, condExp_stopping_time_ae_eq_restrict_eq_of_countable, ProbabilityTheory.condExpKernel_ae_eq_condExp, condExp_stopping_time_ae_eq_restrict_eq_of_countable_range, Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const, condExp_of_aestronglyMeasurable', ProbabilityTheory.condExpKernel_ae_eq_trim_condExp, condExp_min_stopping_time_ae_eq_restrict_le_const, Supermartingale.condExp_ae_le, Martingale.stoppedValue_ae_eq_condExp_of_le_const, ProbabilityTheory.iCondIndepSets_iff, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib₀, condExp_smul_of_aestronglyMeasurable_left, tendsto_eLpNorm_condExp, eLpNorm_one_condExp_le_eLpNorm, integral_condExp_indicator, condExp_of_not_sigmaFinite, ProbabilityTheory.condExp_ae_eq_integral_condDistrib', ProbabilityTheory.Kernel.condExp_densityProcess, stronglyMeasurable_condExp, MemLp.condExpL2_ae_eq_condExp', Martingale.condExp_ae_eq, ProbabilityTheory.condVar_of_sigmaFinite, ProbabilityTheory.iCondIndepFun_iff, ae_mem_limsup_atTop_iff, ae_bdd_condExp_of_ae_bdd, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop, martingalePart_eq_sum, condExp_restrict_ae_eq_restrict, ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt, condExp_of_sigmaFinite, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot, condExp_stronglyMeasurable_mul_of_bound₀, submartingale_iff_condExp_sub_nonneg, condExp_bilin_of_stronglyMeasurable_right, Martingale.condExp_stopping_time_ae_eq_restrict_eq_const, Integrable.uniformIntegrable_condExp_filtration, Martingale.ae_eq_condExp_limitProcess, condExp_indep_eq, condExp_aestronglyMeasurable_bilin_of_bound, Martingale.eq_condExp_of_tendsto_eLpNorm, condExp_bot', ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp, condExp_sub, ProbabilityTheory.condIndepFun_iff, ae_eq_condExp_of_forall_setIntegral_eq, condExp_stronglyMeasurable_bilin_of_bound, Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range, ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self, condExp_indicator_aux, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib', integral_abs_condExp_le, ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le, condExp_min_stopping_time_ae_eq_restrict_le, Submartingale.ae_le_condExp, Submartingale.condExp_sub_nonneg, condExp_mul_of_stronglyMeasurable_left, Martingale.stoppedValue_ae_eq_condExp_of_le, condExp_bot_ae_eq, condExp_ae_eq_restrict_of_measurableSpace_eq_on, Integrable.uniformIntegrable_condExp
condExpUnexpander 📖	CompOp	—
«term__[_|_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_condExp_of_forall_setIntegral_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup IntegrableOn integral Measure.restrict AEStronglyMeasurable	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp	—	ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' Integrable.integrableOn integrable_condExp setIntegral_condExp StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_condExp
condExp_add 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Measure.instOuterMeasureClass Filter.EventuallyEq.trans condExp_ae_eq_condExpL1 SeminormedAddCommGroup.toIsTopologicalAddGroup condExpL1_add Lp.coeFn_add Filter.EventuallyEq.add Filter.EventuallyEq.symm condExp_of_not_sigmaFinite add_zero condExp_of_not_le
condExp_ae_eq_condExpL1 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal condExpL1	—	Measure.instOuterMeasureClass aestronglyMeasurable_condExpL1 condExp_of_sigmaFinite Filter.EventuallyEq.symm condExpL1_of_aestronglyMeasurable' StronglyMeasurable.aestronglyMeasurable SeminormedAddCommGroup.toIsTopologicalAddGroup condExpL1_undef Lp.coeFn_zero
condExp_ae_eq_condExpL1CLM 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp AEEqFun.cast AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Lp.instModule NormedCommRing.toNormedRing Real.normedCommRing NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike condExpL1CLM Integrable.toL1	—	Filter.EventuallyEq.trans Measure.instOuterMeasureClass SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal NormedSpace.toIsBoundedSMul condExp_ae_eq_condExpL1 Filter.Eventually.of_forall condExpL1_eq
condExp_bot 📖	mathematical	—	condExp Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder integral	—	condExp_bot' IsProbabilityMeasure.neZero probReal_univ inv_one one_smul
condExp_bot' 📖	mathematical	—	condExp Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv Measure.real Set.univ integral	—	stronglyMeasurable_condExp stronglyMeasurable_bot_iff AddTorsor.nonempty TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace integral_condExp bot_le IsFiniteMeasure.toSigmaFinite isFiniteMeasure_trim integral_const smul_assoc IsScalarTower.left smul_eq_mul inv_mul_cancel₀ measureReal_def ENNReal.toReal_eq_zero_iff Measure.instNeZeroENNRealCoeSetUniv measure_ne_top one_smul sigmaFinite_trim_bot_iff condExp_of_not_sigmaFinite not_isFiniteMeasure_iff inv_zero zero_smul
condExp_bot_ae_eq 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv Measure.real Set.univ integral	—	Measure.instOuterMeasureClass eq_zero_or_neZero ae_zero Filter.eventually_bot Filter.Eventually.of_forall condExp_bot'
condExp_condExp_of_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp	—	Measure.instOuterMeasureClass LE.le.trans ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' Integrable.integrableOn integrable_condExp setIntegral_condExp StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_condExp condExp_of_not_integrable condExp_zero Filter.EventuallyEq.refl condExp_of_not_sigmaFinite
condExp_congr_ae 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	condExp	—	Measure.instOuterMeasureClass Filter.EventuallyEq.trans condExp_ae_eq_condExpL1 SeminormedAddCommGroup.toIsTopologicalAddGroup condExpL1_congr_ae Filter.EventuallyEq.refl Filter.EventuallyEq.symm condExp_of_not_sigmaFinite condExp_of_not_le
condExp_congr_ae_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Measure.trim condExp	—	Measure.instOuterMeasureClass StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable EMetricSpace.metrizableSpace stronglyMeasurable_condExp condExp_congr_ae
condExp_const 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condExp	—	condExp_of_stronglyMeasurable IsFiniteMeasure.toSigmaFinite isFiniteMeasure_trim stronglyMeasurable_const integrable_const
condExp_def 📖	mathematical	—	condExp MeasurableSpace MeasurableSpace.instLE SigmaFinite Measure.trim Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup StronglyMeasurable Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	aestronglyMeasurable_condExpL1
condExp_finset_sum 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp Finset.sum Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Finset.induction_on Measure.instOuterMeasureClass Finset.sum_empty condExp_zero Filter.EventuallyEq.refl Finset.sum_insert Filter.EventuallyEq.trans condExp_add Finset.mem_insert_self integrable_finset_sum' IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Finset.forall_of_forall_insert Filter.EventuallyEq.add
condExp_mono 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	condExp	—	Measure.instOuterMeasureClass Filter.EventuallyEq.trans_le condExp_ae_eq_condExpL1 Filter.EventuallyLE.trans_eq condExpL1_mono Filter.EventuallyEq.symm condExp_of_not_sigmaFinite Filter.EventuallyLE.refl condExp_of_not_le
condExp_neg 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Measure.instOuterMeasureClass neg_one_smul condExp_smul
condExp_nonneg 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	condExp	—	Measure.instOuterMeasureClass condExp_zero condExp_mono integrable_zero condExp_of_not_integrable Filter.EventuallyLE.refl
condExp_nonpos 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	condExp	—	Measure.instOuterMeasureClass condExp_zero condExp_mono integrable_zero condExp_of_not_integrable Filter.EventuallyLE.refl
condExp_ofNat 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	Measure.instOuterMeasureClass Nat.cast_smul_eq_nsmul nsmul_eq_mul condExp_smul
condExp_of_aestronglyMeasurable' 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp	—	Filter.EventuallyEq.trans Measure.instOuterMeasureClass condExp_congr_ae condExp_of_stronglyMeasurable integrable_congr Filter.EventuallyEq.refl Filter.EventuallyEq.symm
condExp_of_not_integrable 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	condExp Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	aestronglyMeasurable_condExpL1 condExp_of_sigmaFinite condExp_of_not_sigmaFinite condExp_of_not_le
condExp_of_not_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condExp Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	aestronglyMeasurable_condExpL1 condExp_def
condExp_of_not_sigmaFinite 📖	mathematical	MeasurableSpace MeasurableSpace.instLE SigmaFinite Measure.trim	condExp Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	aestronglyMeasurable_condExpL1 condExp_def Mathlib.Tactic.Push.not_and_eq
condExp_of_sigmaFinite 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condExp Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup StronglyMeasurable AEEqFun.cast AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal condExpL1 aestronglyMeasurable_condExpL1 Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	aestronglyMeasurable_condExpL1 condExp_def
condExp_of_stronglyMeasurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	condExp	—	aestronglyMeasurable_condExpL1 condExp_of_sigmaFinite
condExp_smul 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	Measure.instOuterMeasureClass Filter.EventuallyEq.trans condExp_ae_eq_condExpL1 SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal NormedSpace.toIsBoundedSMul condExpL1_smul Filter.Eventually.mp Filter.Eventually.mono Lp.coeFn_smul condExp_of_not_sigmaFinite smul_zero condExp_of_not_le
condExp_sub 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Measure.instOuterMeasureClass sub_eq_add_neg Filter.EventuallyEq.trans condExp_add Integrable.neg Filter.EventuallyEq.add Filter.EventuallyEq.rfl condExp_neg
condExp_zero 📖	mathematical	—	condExp Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	condExp_of_stronglyMeasurable stronglyMeasurable_zero integrable_zero condExp_of_not_sigmaFinite condExp_of_not_le
eLpNorm_condExp_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm condExp InnerProductSpace.toNormedSpace Real Real.instRCLike instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne Ne.lt_top' SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul fact_one_le_two_ennreal eLpNorm_congr_ae MemLp.condExpL2_ae_eq_condExp' le_trans eLpNorm_condExpL2_le MemLp.coeFn_toLp le_refl condExp_of_not_integrable eLpNorm_zero ENNReal.instCanonicallyOrderedAdd condExp_of_not_sigmaFinite condExp_of_not_le
integrable_condExp 📖	mathematical	—	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup condExp	—	Integrable.congr integrable_condExpL1 Filter.EventuallyEq.symm Measure.instOuterMeasureClass condExp_ae_eq_condExpL1 condExp_of_not_sigmaFinite integrable_zero condExp_of_not_le
integral_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	integral condExp	—	setIntegral_condExp MeasurableSet.univ setIntegral_univ condExp_of_not_integrable integral_zero integral_undef
integral_condExp_indicator 📖	mathematical	Measurable MeasurableSet	integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal condExp MeasurableSpace.comap Real.instCompleteSpace Set.indicator Real.instZero Real.instOne Measure.real	—	Measurable.comap_le Real.instCompleteSpace integral_condExp integral_indicator setIntegral_const smul_eq_mul mul_one
setIntegral_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasurableSet	integral Measure.restrict condExp	—	setIntegral_congr_ae Filter.Eventually.mono Measure.instOuterMeasureClass condExp_ae_eq_condExpL1 setIntegral_condExpL1
stronglyMeasurable_condExp 📖	mathematical	—	StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup condExp	—	aestronglyMeasurable_condExpL1 condExp_of_sigmaFinite stronglyMeasurable_zero condExp_of_not_sigmaFinite condExp_of_not_le
tendsto_condExpL1_of_dominated_convergence 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Integrable Real Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.Eventually Real.instLE Norm.norm NormedAddCommGroup.toNorm ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Tendsto Filter.atTop Nat.instPreorder nhds	AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal condExpL1 Lp.instNormedAddCommGroup fact_one_le_one_ennreal	—	Measure.instOuterMeasureClass tendsto_setToFun_of_dominated_convergence SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal dominatedFinMeasAdditive_condExpInd
tendsto_condExp_unique 📖	—	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instLE Norm.norm NormedAddCommGroup.toNorm Filter.EventuallyEq condExp	—	—	Measure.instOuterMeasureClass Filter.EventuallyEq.trans condExp_ae_eq_condExpL1 Filter.EventuallyEq.symm SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.ext_iff Lp.ext fact_one_le_one_ennreal tendsto_condExpL1_of_dominated_convergence tendsto_nhds_unique_of_eventuallyEq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Eventually.of_forall condExp_of_not_sigmaFinite Filter.EventuallyEq.refl condExp_of_not_le

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	MeasureTheory.condExp InnerProductSpace.toNormedSpace Real Real.instRCLike	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.mono MeasureTheory.stronglyMeasurable_condExp LE.le.trans_lt MeasureTheory.eLpNorm_condExp_le eLpNorm_lt_top MeasureTheory.condExp_of_not_le
condExpL2_ae_eq_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule InnerProductSpace.toNormedSpace NormedSpace.toIsBoundedSMul Submodule.setLike MeasureTheory.lpMeas DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike MeasureTheory.condExpL2 toLp MeasureTheory.condExp	—	Nat.instAtLeastTwoHAddOfNat condExpL2_ae_eq_condExp' MeasureTheory.memLp_one_iff_integrable mono_exponent one_le_two IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim
condExpL2_ae_eq_condExp' 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule InnerProductSpace.toNormedSpace NormedSpace.toIsBoundedSMul Submodule.setLike MeasureTheory.lpMeas DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike MeasureTheory.condExpL2 toLp MeasureTheory.condExp	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul fact_one_le_two_ennreal MeasureTheory.integrableOn_condExpL2_of_measure_ne_top LT.lt.ne MeasureTheory.integral_condExpL2_eq MeasureTheory.setIntegral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass coeFn_toLp Filter.univ_mem' MeasureTheory.aestronglyMeasurable_condExpL2

---

← Back to Index