Theorems · Theorem · functional analysis

MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp

∀ {α : 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 t : Set α} [CompleteSpace E]
  (hs : MeasurableSet s) (ht : MeasurableSet t)
  (hμs : autoParam (μ s ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp._auto_1)
  (hμt : autoParam (μ t ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp._auto_3) (a b : E),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs a) (MeasureTheory.indicatorConstLp 2 ht hμt b) =
    μ.real (s ∩ t) • inner 𝕜 a b

The inner product in L2 of two indicatorConstLps, i.e. functions which are constant a : E and b : E on measurable s t : Set α with finite measure, respectively, is ⟪a, b⟫ times the measure of s ∩ t.

Defined in

Mathlib.MeasureTheory.Function.L2Space

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace