inner_indicatorConstLp_one — Mathlib

English

The inner product with the indicator of a set and the function f equals the integral of f over that set.

Русский

Внутреннее произведение индикатора множества и функции f равно интегралу f по этому множеству.

LaTeX

$$$⟪\\mathrm{indicator}_{s}, f⟫ = \\int_{s} f(x) \\, dμ(x)$$$

Lean4

/-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs (1 : 𝕜)` and
a real or complex function `f` is equal to the integral of `f` over `s`. -/
theorem inner_indicatorConstLp_one (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (f : Lp 𝕜 2 μ) :
    ⟪indicatorConstLp 2 hs hμs (1 : 𝕜), f⟫ = ∫ x in s, f x ∂μ := by
  rw [L2.inner_indicatorConstLp_eq_inner_setIntegral 𝕜 hs hμs (1 : 𝕜) f]; simp

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