innerProductSpace — Mathlib

English

The symmetric property of equivalence holds: the inverse equivalence respects reversal of index bijection.

Русский

Свойство симметрии эквивалентности: обратная эквивалентность сохраняет направление биекции индексов.

LaTeX

$$$(hv.equiv hv' e).symm = hv'.equiv hv e.symm$$$

Lean4

instance innerProductSpace {ι : Type*} [Fintype ι] (f : ι → Type*) [∀ i, NormedAddCommGroup (f i)]
    [∀ i, InnerProductSpace 𝕜 (f i)] : InnerProductSpace 𝕜 (PiLp 2 f)
    where
  inner x y := ∑ i, ⟪x i, y i⟫
  norm_sq_eq_re_inner x := by simp only [PiLp.norm_sq_eq_of_L2, map_sum, ← norm_sq_eq_re_inner]
  conj_inner_symm := by
    intro x y
    unfold inner
    rw [map_sum]
    apply Finset.sum_congr rfl
    rintro z -
    apply inner_conj_symm
  add_left x y
    z :=
    show (∑ i, ⟪x i + y i, z i⟫ = ∑ i, ⟪x i, z i⟫ + ∑ i, ⟪y i, z i⟫) by
      simp only [inner_add_left, Finset.sum_add_distrib]
  smul_left x y
    r := show (∑ i : ι, ⟪r • x i, y i⟫ = conj r * ∑ i, ⟪x i, y i⟫) by simp only [Finset.mul_sum, inner_smul_left]

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