CondJensen

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

Statistics

Metric	Count
Definitions	0
Theorems norm_condExp_le, condExp_map_le, condExp_map_le_of_finiteDimensional, condExp_map_le_univ, condExp_mem, map_condExp_le, map_condExp_le_of_finiteDimensional, map_condExp_le_univ	8
Total	8

AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_condExp_le 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Norm.norm NormedAddCommGroup.toNorm MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace MeasureTheory.condExp_of_not_le norm_zero Filter.EventuallyLE.refl MeasureTheory.condExp_of_not_sigmaFinite MeasureTheory.integrable_norm_iff MeasureTheory.condExp_of_not_integrable ConvexOn.map_condExp_le_univ convexOn_univ_norm Continuous.lowerSemicontinuous instOrderTopologyReal continuous_norm MeasureTheory.Integrable.norm

ConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp_map_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id UpperSemicontinuousOn Real.instPreorder Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem Real.instCompleteSpace MeasureTheory.condExp_neg ConvexOn.map_condExp_le neg Real.instIsOrderedAddMonoid UpperSemicontinuousOn.neg MeasureTheory.Integrable.neg Filter.univ_mem' IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
condExp_map_le_of_finiteDimensional 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace MeasureTheory.condExp_neg ConvexOn.map_condExp_le_of_finiteDimensional neg Real.instIsOrderedAddMonoid MeasureTheory.Integrable.neg Filter.univ_mem' IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
condExp_map_le_univ 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ConcaveOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ UpperSemicontinuous Real.instPreorder MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace MeasureTheory.condExp_neg ConvexOn.map_condExp_le_univ neg Real.instIsOrderedAddMonoid UpperSemicontinuous.neg MeasureTheory.Integrable.neg Filter.univ_mem' IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp_mem 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Eventually Set Set.instMembership MeasureTheory.condExp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass RCLike.iInter_countable_halfSpaces_eq IsScalarTower.left SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul NormedSpace.toLocallyConvexSpace instCountableNat Real.instCompleteSpace ContinuousLinearMap.comp_condExp_comm MeasureTheory.condExp_mono instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing ContinuousLinearMap.integrable_comp RingHomIsometric.ids MeasureTheory.integrable_const Filter.mp_mem Filter.univ_mem' MeasureTheory.condExp_const

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_condExp_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id LowerSemicontinuousOn Real.instPreorder Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	MeasureTheory.Measure.instOuterMeasureClass IsCountablySpanning.null_of_forall_restrict_null Real.instCompleteSpace MeasureTheory.isCountablySpanning_spanningSets MeasureTheory.measurableSet_spanningSets MeasureTheory.condExp_restrict_ae_eq_restrict MeasureTheory.isFiniteMeasure_restrict LT.lt.ne LE.le.trans_lt MeasureTheory.le_trim MeasureTheory.measure_spanningSets_lt_top MeasureTheory.ae_restrict_of_ae MeasureTheory.Integrable.restrict Filter.mp_mem Filter.univ_mem'
map_condExp_le_of_finiteDimensional 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	map_condExp_le_univ Continuous.lowerSemicontinuous instOrderTopologyReal continuousOn_univ continuousOn isOpen_univ
map_condExp_le_univ 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ConvexOn Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ LowerSemicontinuous Real.instPreorder MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	map_condExp_le lowerSemicontinuousOn_univ_iff MeasureTheory.Measure.instOuterMeasureClass isClosed_univ

---

← Back to Index