inner_condExpL2_eq_inner_fun — Mathlib

English

Let hm ≤ m0 and g be AEStronglyMeasurable; for any f, the inner product of condExpL2(f) with g equals the inner product of f with g.

Русский

Пусть hm ≤ m0 и g лежит в AEStronglyMeasurable; тогда ⟪condExpL2 f, g⟫ = ⟪f, g⟫ для всех f.

LaTeX

$$$\langle (\operatorname{condExpL2} E \ 𝕜 \; hm \; f : α \to_2[μ] E), g \rangle = \langle f, g \rangle$$$

Lean4

theorem inner_condExpL2_eq_inner_fun (hm : m ≤ m0) (f g : α →₂[μ] E) (hg : AEStronglyMeasurable[m] g μ) :
    ⟪(condExpL2 E 𝕜 hm f : α →₂[μ] E), g⟫ = ⟪f, g⟫ := by
  symm
  rw [← sub_eq_zero, ← inner_sub_left, condExpL2]
  simp only [← Submodule.starProjection_apply, mem_lpMeas_iff_aestronglyMeasurable.mpr hg,
    Submodule.starProjection_inner_eq_zero f g]

Похожие утверждения