Theorems · Theorem · functional analysis

MeasureTheory.ContinuousMap.inner_toLp

∀ {α : Type u_1} {𝕜 : Type u_2} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
  [inst_3 : RCLike 𝕜] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsFiniteMeasure μ] [inst_5 : CompactSpace α]
  (f g : C(α, 𝕜)),
  inner 𝕜 ((ContinuousMap.toLp 2 μ 𝕜) f) ((ContinuousMap.toLp 2 μ 𝕜) g) = ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

For continuous functions f, g on a compact, finite-measure topological space α, the L^2 inner product is the integral of their pointwise inner product.

Defined in

Mathlib.MeasureTheory.Function.L2Space

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceRCLikeMeasureTheory.IsFiniteMeasureCompactSpace