English
For bounded continuous functions f, g on a finite-measure space, the L2 inner product equals the integral of the pointwise product with conjugation.
Русский
Для ограниченных непрерывных функций f, g на пространстве с конечной мерой внутр. произведение L2 равно интегралу по точечному произведению с сопряжением.
LaTeX
$$$⟪f,g⟫_{L^2} = \\int f(x) \\overline{g(x)} \\, dμ(x)$$$
Lean4
/-- For bounded continuous functions `f`, `g` on a finite-measure topological space `α`, the L^2
inner product is the integral of their pointwise inner product. -/
theorem inner_toLp (f g : α →ᵇ 𝕜) :
⟪BoundedContinuousFunction.toLp 2 μ 𝕜 f, BoundedContinuousFunction.toLp 2 μ 𝕜 g⟫ = ∫ x, g x * conj (f x) ∂μ :=
by
apply integral_congr_ae
have hf_ae := f.coeFn_toLp 2 μ 𝕜
have hg_ae := g.coeFn_toLp 2 μ 𝕜
filter_upwards [hf_ae, hg_ae] with _ hf hg
rw [hf, hg]
simp
