Theorems · Theorem · functional analysis

MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one

∀ {α : Type u_1} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}
  (hs : MeasurableSet s) (ht : MeasurableSet t)
  (hμs : autoParam (μ s ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one._auto_1)
  (hμt : autoParam (μ t ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one._auto_3),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs 1) (MeasureTheory.indicatorConstLp 2 ht hμt 1) = ↑(μ.real (s ∩ t))

The inner product in L2 of indicators of two sets with finite measure is the measure of the intersection.

Defined in

Mathlib.MeasureTheory.Function.L2Space

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLike