orthonormalBasis_apply — Mathlib

English

Applying the Pi-orthonormalBasis to an index j recovers the corresponding basis element from the i-th component, via the canonical isomorphisms.

Русский

Применение Pi-ортонормBasis к индексу j возвращает соответствующий элемент базиса из компоненты i через канонические изоморфизмы.

LaTeX

$$$\,\text{Pi.orthonormalBasis apply }\! B\; j = (\text{component})$$$

Lean4

@[simp]
theorem _root_.Pi.orthonormalBasis_apply {η : Type*} [Fintype η] [DecidableEq η] {ι : η → Type*} [∀ i, Fintype (ι i)]
    {𝕜 : Type*} [RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace 𝕜 (E i)]
    (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) (j : (i : η) × (ι i)) :
    Pi.orthonormalBasis B j = toLp _ (Pi.single _ (B j.fst j.snd)) := by
  classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans, LinearIsometryEquiv.symm_symm,
    LinearIsometryEquiv.piLpCongrRight_symm, LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, EuclideanSpace.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp only [Pi.single_eq_same, EuclideanSpace.toLp_single, OrthonormalBasis.repr_symm_single]
  · simp only [Pi.single_eq_of_ne' hi, toLp_zero, map_zero]

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