Real

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

Statistics

Metric	Count
Definitions	0
Theorems uniformIntegrable_condExp, ae_bdd_condExp_of_ae_bdd, eLpNorm_one_condExp_le_eLpNorm, integral_abs_condExp_le, rnDeriv_ae_eq_condExp, setIntegral_abs_condExp_le	6
Total	6

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_bdd_condExp_of_ae_bdd 📖	mathematical	Filter.Eventually Real Real.instLE abs Real.lattice Real.instAddGroup NNReal.toReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	Measure.instOuterMeasureClass Real.instCompleteSpace lt_of_lt_of_le setIntegral_gt_gt NNReal.coe_nonneg Integrable.integrableOn Integrable.abs instHasSolidNormReal Real.instIsOrderedAddMonoid integrable_condExp LT.lt.ne' ENNReal.instCanonicallyOrderedAdd LE.le.trans setIntegral_abs_condExp_le measurableSet_lt BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal HasSolidNorm.orderClosedTopology measurable_const StronglyMeasurable.measurable PseudoEMetricSpace.pseudoMetrizableSpace StronglyMeasurable.norm stronglyMeasurable_condExp setIntegral_mono_ae IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology aestronglyMeasurable_const lt_of_le_of_lt setLIntegral_mono Measurable.coe_nnreal_ennreal Measurable.nnnorm StronglyMeasurable.mono enorm_eq_nnnorm ENNReal.coe_le_coe Real.nnnorm_of_nonneg norm_nonneg le_of_lt LT.lt.ne condExp_of_not_integrable Filter.mp_mem Filter.univ_mem' Pi.zero_apply abs_zero IsOrderedAddMonoid.toAddLeftMono abs_nonneg covariant_swap_add_of_covariant_add condExp_of_not_le Filter.Eventually.of_forall
eLpNorm_one_condExp_le_eLpNorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Real.instCompleteSpace eLpNorm_mono_ae Filter.mp_mem Measure.instOuterMeasureClass Filter.EventuallyLE.trans Filter.EventuallyEq.le Filter.EventuallyEq.symm condExp_neg condExp_mono instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Integrable.neg Integrable.abs ae_of_all neg_le_abs le_abs_self Filter.univ_mem' abs_le_abs eLpNorm_one_eq_lintegral_enorm ENNReal.toReal_eq_toReal_iff' LT.lt.ne hasFiniteIntegral_iff_enorm integrable_condExp integral_norm_eq_lintegral_enorm StronglyMeasurable.aestronglyMeasurable StronglyMeasurable.mono stronglyMeasurable_condExp integral_condExp integral_congr_ae condExp_zero integrable_zero abs_nonneg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add abs_eq_self condExp_of_not_sigmaFinite eLpNorm_zero zero_le ENNReal.instCanonicallyOrderedAdd condExp_of_not_le condExp_of_not_integrable
integral_abs_condExp_le 📖	mathematical	—	Real Real.instLE integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal abs Real.lattice Real.instAddGroup condExp Real.instCompleteSpace	—	Real.instCompleteSpace integral_eq_lintegral_of_nonneg_ae Filter.univ_mem' Measure.instOuterMeasureClass abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add AEStronglyMeasurable.norm StronglyMeasurable.aestronglyMeasurable StronglyMeasurable.mono stronglyMeasurable_condExp ENNReal.toReal_mono ofReal_norm_eq_enorm LT.lt.ne eLpNorm_one_eq_lintegral_enorm eLpNorm_one_condExp_le_eLpNorm condExp_of_not_integrable abs_zero integral_const MulZeroClass.mul_zero integral_nonneg IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal condExp_of_not_le integral_zero
rnDeriv_ae_eq_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass SignedMeasure.rnDeriv VectorMeasure.trim ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Measure.withDensityᵥ InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Measure.trim condExp Real.instCompleteSpace	—	ae_eq_condExp_of_forall_setIntegral_eq Real.instCompleteSpace Integrable.integrableOn integrable_of_integrable_trim SignedMeasure.integrable_rnDeriv Integrable.withDensityᵥ_trim_eq_integral SignedMeasure.withDensityᵥ_rnDeriv_eq Integrable.withDensityᵥ_trim_absolutelyContinuous withDensityᵥ_apply setIntegral_trim Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace SignedMeasure.measurable_rnDeriv StronglyMeasurable.aestronglyMeasurable
setIntegral_abs_condExp_le 📖	mathematical	MeasurableSet	Real Real.instLE integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Measure.restrict abs Real.lattice Real.instAddGroup condExp Real.instCompleteSpace	—	Real.instCompleteSpace integral_indicator integral_congr_ae Measure.instOuterMeasureClass Filter.EventuallyEq.fun_comp condExp_indicator Filter.EventuallyEq.trans Filter.Eventually.of_forall Real.norm_eq_abs norm_indicator_eq_indicator_norm Filter.EventuallyEq.symm LE.le.trans integral_abs_condExp_le le_of_eq condExp_of_not_integrable abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid integral_const MulZeroClass.mul_zero integral_nonneg IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal abs_nonneg covariant_swap_add_of_covariant_add condExp_of_not_le integral_zero

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformIntegrable_condExp 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasurableSpace MeasurableSpace.instLE	MeasureTheory.UniformIntegrable Real.normedAddCommGroup MeasureTheory.condExp Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Real.instCompleteSpace measurableSet_le BorelSpace.opensMeasurable NNReal.borelSpace OrderTopology.to_orderClosedTopology NNReal.instOrderTopology NNReal.instSecondCountableTopology measurable_const Measurable.nnnorm Real.borelSpace MeasureTheory.StronglyMeasurable.measurable PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.StronglyMeasurable.mono MeasureTheory.stronglyMeasurable_condExp MeasureTheory.memLp_one_iff_integrable MeasureTheory.uniformIntegrable_of le_rfl ENNReal.one_ne_top MeasureTheory.StronglyMeasurable.aestronglyMeasurable LE.le.trans le_of_eq MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_eq_zero_iff MeasureTheory.AEStronglyMeasurable.indicator one_ne_zero NeZero.charZero_one ENNReal.instCharZero Filter.mp_mem MeasureTheory.condExp_congr_ae Filter.univ_mem' Set.indicator_univ MeasureTheory.condExp_zero zero_le ENNReal.instCanonicallyOrderedAdd MeasureTheory.MemLp.eLpNorm_indicator_le LT.lt.le mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE ENNReal.toNNReal_pos LT.lt.ne MeasureTheory.MemLp.eLpNorm_lt_top ENNReal.toReal_one ENNReal.rpow_one enorm_eq_nnnorm MeasureTheory.mul_meas_ge_le_pow_eLpNorm ENNReal.le_div_iff_mul_le ENNReal.coe_ne_zero LT.lt.ne' ENNReal.coe_lt_top mul_comm ENNReal.div_le_iff_le_mul inv_nonneg IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ENNReal.coe_mul ENNReal.coe_toNNReal mul_assoc ENNReal.ofReal_eq_coe_nnreal ENNReal.ofReal_mul mul_inv_cancel₀ ENNReal.ofReal_one one_mul MeasureTheory.eLpNorm_one_condExp_le_eLpNorm le_trans MeasureTheory.eLpNorm_congr_ae MeasureTheory.condExp_indicator

---

← Back to Index