instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal

English

Let f and g be square-integrable vector-valued functions on a measure space (α, μ). Then the inner product in the L2 space is given by integrating the pointwise inner product.

Русский

Пусть f и g являются квадратно интегрируемыми функциями с значениями в E на мере μ. Тогда внутреннее произведение в пространстве L2 задаётся интегрированием покоординатного скалярного произведения.

LaTeX

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

Lean4

instance : Inner 𝕜 (α →₂[μ] E) :=
  ⟨fun f g => ∫ a, ⟪f a, g a⟫ ∂μ⟩

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