instInnerProductSpace — Mathlib

English

The space lp G 2 is equipped with the inner product ⟪f,g⟫ = ∑' i ⟪f(i), g(i)⟫, making it a real/complex Hilbert space depending on 𝕜.

Русский

Пространство lp G 2 оснащено внут. произведением ⟪f,g⟫ = ∑' i ⟪f(i), g(i)⟫, образуя гильбертово пространство (в зависимости от 𝕜).

LaTeX

$$$ \\langle f,g \\rangle = \\sum\\_' i \\langle f(i), g(i) \\rangle $$$

Lean4

instance instInnerProductSpace : InnerProductSpace 𝕜 (lp G 2) :=
  {
    lp.normedAddCommGroup (E := G) (p :=
      2) with
    inner := fun f g => ∑' i, ⟪f i, g i⟫
    norm_sq_eq_re_inner := fun f =>
      by
      calc
        ‖f‖ ^ 2 = ‖f‖ ^ (2 : ℝ≥0∞).toReal := by norm_cast
        _ = ∑' i, ‖f i‖ ^ (2 : ℝ≥0∞).toReal := (lp.norm_rpow_eq_tsum ?_ f)
        _ = ∑' i, ‖f i‖ ^ (2 : ℕ) := by norm_cast
        _ = ∑' i, re ⟪f i, f i⟫ := by simp [norm_sq_eq_re_inner (𝕜 := 𝕜)]
        _ = re (∑' i, ⟪f i, f i⟫) := (RCLike.reCLM.map_tsum ?_).symm
      · norm_num
      · exact summable_inner f f
    conj_inner_symm := fun f g => by
      calc
        conj _ = conj (∑' i, ⟪g i, f i⟫) := by congr
        _ = ∑' i, conj ⟪g i, f i⟫ := RCLike.conjCLE.map_tsum
        _ = ∑' i, ⟪f i, g i⟫ := by simp only [inner_conj_symm]
        _ = _ := by congr
    add_left := fun f₁ f₂ g =>
      by
      calc
        _ = ∑' i, ⟪(f₁ + f₂) i, g i⟫ := ?_
        _ = ∑' i, (⟪f₁ i, g i⟫ + ⟪f₂ i, g i⟫) := by simp only [inner_add_left, Pi.add_apply, coeFn_add]
        _ = (∑' i, ⟪f₁ i, g i⟫) + ∑' i, ⟪f₂ i, g i⟫ := (Summable.tsum_add ?_ ?_)
        _ = _ := by congr
      · congr
      · exact summable_inner f₁ g
      · exact summable_inner f₂ g
    smul_left := fun f g c =>
      by
      calc
        _ = ∑' i, ⟪c • f i, g i⟫ := ?_
        _ = ∑' i, conj c * ⟪f i, g i⟫ := by simp only [inner_smul_left]
        _ = conj c * ∑' i, ⟪f i, g i⟫ := tsum_mul_left
        _ = _ := ?_
      · simp only [coeFn_smul, Pi.smul_apply]
      · congr }

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