Commit 2026-03-18 19:14 9ea92097

View on Github →

feat(ProbabilityTheory): Conditional Jensen's Inequality (#27953) This PR adds several variants of the conditional Jensen's inequality. I made some changes to Mathlib/Analysis/Convex/Approximation.lean because I need the sequence of affine functions to be bouneded above at each point in the proof of conditional_jensen_hereditarilyLindelofSpace.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Approximation.lean

Created Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean

added theorem AEStronglyMeasurable.norm_condExp_le

added theorem ConcaveOn.condExp_map_le

added theorem ConcaveOn.condExp_map_le_of_finiteDimensional

added theorem ConcaveOn.condExp_map_le_univ

added theorem Convex.condExp_mem

added theorem ConvexOn.map_condExp_le

added theorem ConvexOn.map_condExp_le_of_finiteDimensional

added theorem ConvexOn.map_condExp_le_univ

Modified Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

added theorem Measurable.codRestrict

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem IsCountablySpanning.null_of_forall_inter_null

added theorem IsCountablySpanning.null_of_forall_restrict_null

added theorem MeasureTheory.Measure.forall_measure_inter_isCountablySpanning_eq_zero

Modified Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean