integral_condExpL2_eq_of_fin_meas_real

English

For any f ∈ Lp 2 μ and measurable set s with μ(s) finite, the integral over s of condExpL2 equals the integral over s of f.

Русский

Для любого f ∈ Lp2 μ и измеримого множества s с конечной μ-мерой, интеграл по s от condExpL2 равен интегралу по s от f.

LaTeX

$$$\int_{x \in s} (\operatorname{condExpL2} E \, 𝕜 \; hm \; f : α \to_2[μ] E)(x) \, dμ(x) = \int_{x \in s} f(x) \, dμ(x)$$$

Lean4

theorem integral_condExpL2_eq_of_fin_meas_real (f : Lp 𝕜 2 μ) (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) :
    ∫ x in s, (condExpL2 𝕜 𝕜 hm f : α → 𝕜) x ∂μ = ∫ x in s, f x ∂μ :=
  by
  rw [← L2.inner_indicatorConstLp_one (𝕜 := 𝕜) (hm s hs) hμs f]
  have h_eq_inner :
    ∫ x in s, (condExpL2 𝕜 𝕜 hm f : α → 𝕜) x ∂μ = ⟪indicatorConstLp 2 (hm s hs) hμs (1 : 𝕜), condExpL2 𝕜 𝕜 hm f⟫ := by
    rw [L2.inner_indicatorConstLp_one (hm s hs) hμs]
  rw [h_eq_inner, ← inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable hm hs hμs]

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