English
For hm ≤ m0, f,g ∈ L2 and AEStronglyMeasurable g, the conditional expectation preserves inner products with g: ⟪condExpL2 f, g⟫ = ⟪f, g⟫.
Русский
Для hm ≤ m0, f,g ∈ L2, AEStronglyMeasurable g: ⟪condExpL2 f, g⟫ = ⟪f, g⟫.
LaTeX
$$$\langle (\operatorname{condExpL2} E' \, 𝕜 \; hm \; f : α \to_2[μ] E'), g \rangle = \langle f, g \rangle$$$
Lean4
theorem condExpL2_ae_eq_zero_of_ae_eq_zero (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) {f : Lp ℝ 2 μ}
(hf : f =ᵐ[μ.restrict s] 0) : condExpL2 ℝ ℝ hm f =ᵐ[μ.restrict s] (0 : α → ℝ) :=
by
suffices h_nnnorm_eq_zero : ∫⁻ x in s, ‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ ∂μ = 0
by
rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero
· refine h_nnnorm_eq_zero.mono fun x hx => ?_
dsimp only at hx
rw [Pi.zero_apply] at hx ⊢
· rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
· refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)
exact (Lp.stronglyMeasurable _).measurable
refine le_antisymm ?_ (zero_le _)
refine (lintegral_nnnorm_condExpL2_le hs hμs f).trans (le_of_eq ?_)
rw [lintegral_eq_zero_iff]
· refine hf.mono fun x hx => ?_
dsimp only
rw [hx]
simp
· exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)
