Conditional expectation of L^2 is L^2

Stream: Is there code for X?

[Yaël Dillies]

I am still working on defining the conditional variance. Do we have that the L^2 norm of μ[f | m] is less than the L^2 norm of f?

[Yaël Dillies]

Here is my attempt:

import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

namespace MeasureTheory
variable {Ω R E : Type*} {f : Ω → E}
  {m m₀ : MeasurableSpace Ω} {μ : Measure Ω} {s : Set Ω}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]

@[simp] alias Memℒp.zero := zero_memℒp

lemma eLpNorm_condexp_le : eLpNorm (μ[f | m]) 2 μ ≤ eLpNorm f 2 μ := sorry

protected lemma Memℒp.condexp (hf : Memℒp f 2 μ) : Memℒp (μ[f | m]) 2 μ := by
  by_cases hm : m ≤ m₀
  · exact ⟨(stronglyMeasurable_condexp.mono hm).aestronglyMeasurable,
      eLpNorm_condexp_le.trans_lt hf.eLpNorm_lt_top⟩
  · simp [condexp_of_not_le hm]

[Etienne Marion]

Does docs#MeasureTheory.norm_condexpL2_le help?

[Rémy Degenne]

The right thing to do would be to prove Jensen's inequality for the conditional expectation, which should be this:

import Mathlib
open ProbabilityTheory MeasureTheory

example {α X : Type*} {m mα : MeasurableSpace α} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [CompleteSpace X]
    (hm : m ≤ mα) {μ : Measure α} [SigmaFinite (μ.trim hm)]
    {f : α → X} {φ : X → ℝ} (hφ_cvx : ConvexOn ℝ Set.univ φ) (hφ_cont : LowerSemicontinuous φ)
    (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
    ∀ᵐ x ∂μ, φ ((μ[f | m]) x) ≤ (μ[φ ∘ f | m]) x :=
  sorry

For a reference, see Hytönen et al., Analysis in Banach Spaces (volume 1), proposition 2.6.29 (conditional Jensen) and corollary 2.6.30 (Lp-contractivity).
Let me tag @Alex Nguyen who was working on that a few weeks ago.

[Rémy Degenne]

It's also the last missing piece for a proof of the data-processing inequality for f-divergences that @Lorenzo Luccioli talked about at Lean Together.