inner_def — Mathlib

English

The L2 inner product is defined by the integral of the pointwise inner product of two L2 functions.

Русский

Внутреннее произведение в L2 задаётся как интеграл покоординатного скалярного произведения двух функций L2.

LaTeX

$$$⟪f,g⟫_{L^2} = ∫_{α} ⟪f(a), g(a)⟫ \\, dμ(a)$$$

Lean4

theorem inner_def (f g : α →₂[μ] E) : ⟪f, g⟫ = ∫ a : α, ⟪f a, g a⟫ ∂μ :=
  rfl

Похожие утверждения