English
For bounded continuous maps f,g, the L2 inner product of their L2-representatives equals the integral of their pointwise product with conjugation.
Русский
Для ограниченных непрерывных отображений f,g согласно их представлениям в L2, внутреннее произведение равно интегралу точного произведения с сопряжением.
LaTeX
$$$⟪\\mathrm{toLp}_2(f), \\mathrm{toLp}_2(g)⟫ = ∫ f(x) \\overline{g(x)} \\, dμ(x)$$$
Lean4
/-- 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. -/
theorem inner_toLp (f g : C(α, 𝕜)) :
⟪ContinuousMap.toLp 2 μ 𝕜 f, ContinuousMap.toLp 2 μ 𝕜 g⟫ = ∫ x, g x * conj (f x) ∂μ :=
by
apply integral_congr_ae
have hf_ae := f.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
have hg_ae := g.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
filter_upwards [hf_ae, hg_ae] with _ hf hg
rw [hf, hg]
simp
