inner_indicatorConstLp_eq_inner_setIntegral

English

The inner product of an indicator constant on a set with f equals the inner product of the constant with the integral of f over the set.

Русский

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

LaTeX

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

Lean4

/-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs c` and `f` is
equal to the inner product of the constant `c` and the integral of `f` over `s`. -/
theorem inner_indicatorConstLp_eq_inner_setIntegral [CompleteSpace E] [NormedSpace ℝ E] (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (c : E) (f : Lp E 2 μ) : (⟪indicatorConstLp 2 hs hμs c, f⟫ : 𝕜) = ⟪c, ∫ x in s, f x ∂μ⟫ := by
  rw [← integral_inner (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs),
    L2.inner_indicatorConstLp_eq_setIntegral_inner]

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