innerProductSpace — Mathlib

English

The space of square-integrable functions from α to E forms an inner product space over 𝕜 with inner product given by the integral of pointwise inner products.

Русский

Пространство квадратно интегрируемых функций образует пространство с внутренним произведением над 𝕜, где ⟪f,g⟫ = ∫ ⟪f(a), g(a)⟫ dμ.

LaTeX

$$$\\langle f,g \\rangle_{L^2} = \\int_{α} ⟪f(a), g(a)\\rangle \\, dμ(a)$$$

Lean4

instance innerProductSpace : InnerProductSpace 𝕜 (α →₂[μ] E)
    where
  norm_sq_eq_re_inner := norm_sq_eq_re_inner
  conj_inner_symm _ _ := by simp_rw [inner_def, ← integral_conj, inner_conj_symm]
  add_left := add_left'
  smul_left := smul_left'

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