feat(ProbabilityTheory): Conditional Jensen's Inequality

[CoolRmal]

This PR adds conditional Jensen's inequality.

---

[github-actions]

PR summary e2292a327e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.NormedSpace.HahnBanach.Separation	1854	1857	+3 (+0.16%)

Import changes for all files

Files	Import difference
56 files Mathlib.Analysis.BoundedVariation Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.SumIntegralComparisons Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircleAdd Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Extreme Mathlib.Dynamics.Ergodic.RadonNikodym Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.JacobianOneDim Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.IntegralConvolution Mathlib.MeasureTheory.Group.ModularCharacter Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.Periodic Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.DistribChar Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Order.UpperLower Mathlib.NumberTheory.WellApproximable Mathlib.Probability.Density Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.WithDensity	1
Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual	2
4 files Mathlib.Analysis.Convex.Cone.Dual Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.NormedSpace.HahnBanach.Separation	3
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (new file)	2185

---

Declarations diff

+ ConvexOn.convex_RCLike_epigraph
+ ConvexOn.iSup_affine_eq_of_separableSpace
+ LowerSemicontinuous.isClosed_RCLike_epigraph
+ Measurable.codRestrict
+ condExpL1_comp_affine
+ condExpL1_comp_continuousLinearMap
+ conditional_jensen
+ conditional_jensen_of_separableSpace
+ iInter_nat_halfSpaces_eq
+ iInter_nat_halfSpaces_eq_of_prod

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[RemyDegenne]

Nice PR! Here are a first few general comments. I did not review the proofs of the lemmas yet.

I think that the file should be placed in the folder MeasureTheory/Function/ConditionalExpectation.

[RemyDegenne]

Please revert that change. A PR should not change anything in lake-manifest.json.

[RemyDegenne]

You should add an explanation of what the inequality is.

[RemyDegenne]

According to the docstring of TopologicalSpace.SeparableSpace, you should instead use SecondCountableTopology here.

[RemyDegenne]

That lemma is about convex functions in general and not specifically about conditional expectations, so it should be moved to a file about convex functions.

All the auxiliary lemmas of this file should be moved to other more appropriate files.

[RemyDegenne]

Let's put the description of the lemma first. The reference is not as important to a person reading the docstring while coding.

Suggested change

	/-- Lemma 1.2.10 in [Hytonen_VanNeerven_Veraar_Wies_2016]: a convex lower-semicontinuous function
	is the supremum of a sequence of affine functions in a separable space. -/
	/-- A convex lower-semicontinuous function is the supremum of a sequence of affine functions
	in a separable space.
	Lemma 1.2.10 in [Hytonen_VanNeerven_Veraar_Wies_2016]. -/

[RemyDegenne]

That docstring does not explain what the lemma does, and refers to a lemma from an unknown source.

[RemyDegenne]

Can you please add a TODO in the file docstring to say that this should possibly be generalized to sigma-finite measures?

[RemyDegenne]

In Mathlib, for uniformity and to avoid duplication of some lemmas, we state all inequalities with ≤, not ≥. Can you change that everywhere in your code?

Suggested change

	⋂ (i : ℕ), {x | re ((L i) x) - c i ≥ 0} = s ∧
	⋂ (i : ℕ), {x | 0 ≤ re ((L i) x) - c i} = s ∧

Also, why not {x | c i ≤ re ((L i) x)}?