Theorems · Theorem · functional analysis

MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner

∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {s : Set α} (f : ↥(MeasureTheory.Lp E 2 μ))
  (hs : MeasurableSet s) (c : E) (hμs : μ s ≠ ⊤),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs c) f = ∫ (x : α) in s, inner 𝕜 c (↑↑f x) ∂μ

The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs c and f is equal to the integral of the inner product over s: ∫ x in s, ⟪c, f x⟫ ∂μ.

Defined in

Mathlib.MeasureTheory.Function.L2Space

Cited by

2 results in Mathlib

Foundations

Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpace