inner_condExpL2_left_eq_right — Mathlib

English

Let hm be a refinement of sigma-algebras with f and g belonging to L2 with respect to μ. The L2 conditional expectation is self-adjoint: the inner product of condExpL2(f) with g equals the inner product of f with condExpL2(g).

Русский

Пусть hm задаёт вложенность сигма-алгебр, и f,g ∈ L2(μ; E). Тогда условное ожидание в L2 является самосопряженным: ⟪condExpL2 f, g⟫ = ⟪f, condExpL2 g⟫.

LaTeX

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

Lean4

theorem inner_condExpL2_left_eq_right (hm : m ≤ m0) {f g : α →₂[μ] E} :
    ⟪(condExpL2 E 𝕜 hm f : α →₂[μ] E), g⟫ = ⟪f, (condExpL2 E 𝕜 hm g : α →₂[μ] E)⟫ :=
  haveI : Fact (m ≤ m0) := ⟨hm⟩
  Submodule.inner_starProjection_left_eq_right _ f g

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