setIntegral_condExpL1 — Mathlib

English

For any scalar c in 𝕜 and function f, condExpL1 hm μ (c·f) = c·condExpL1 hm μ f.

Русский

Для скаляра c∈𝕜 и функции f выполняется condExpL1 hm μ (c·f) = c·condExpL1 hm μ f.

LaTeX

$$$condExpL1 hm μ (c\cdot f) = c\cdot condExpL1 hm μ f$$$

Lean4

/-- The integral of the conditional expectation `condExpL1` over an `m`-measurable set is equal to
the integral of `f` on that set. See also `setIntegral_condExp`, the similar statement for
`condExp`. -/
theorem setIntegral_condExpL1 (hf : Integrable f μ) (hs : MeasurableSet[m] s) :
    ∫ x in s, condExpL1 hm μ f x ∂μ = ∫ x in s, f x ∂μ :=
  by
  simp_rw [condExpL1_eq hf]
  rw [setIntegral_condExpL1CLM (hf.toL1 f) hs]
  exact setIntegral_congr_ae (hm s hs) (hf.coeFn_toL1.mono fun x hx _ => hx)

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