English
The value of the Pi-orthonormal basis at a pair j equals the corresponding unit vector embedded in the j-th slot: (Pi.orthonormalBasis B) j = toLp 2 (Pi.single j.fst (B j.fst j.snd)).
Русский
Значение Pi-ортонормированного базиса в точке j равно соответствующему единичному вектору, помещённому в j-ю позицию.
LaTeX
$$$\Pi\text{.orthonormalBasis } B\; j = \operatorname{toLp}_2(\Pi\text{single } j.fst (B j.fst j.snd))$$$
Lean4
/-- `Pi.orthonormalBasis (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i))` is the
`Σ i, ι i`-indexed orthonormal basis on `Π i, E i` given by `B i` on each component. -/
protected def _root_.Pi.orthonormalBasis {η : Type*} [Fintype η] {ι : η → Type*} [∀ i, Fintype (ι i)] {𝕜 : Type*}
[RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace 𝕜 (E i)]
(B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) : OrthonormalBasis ((i : η) × ι i) 𝕜 (PiLp 2 E) where
repr := .trans (.piLpCongrRight 2 fun i => (B i).repr) (.symm <| .piLpCurry 𝕜 2 fun _ _ => 𝕜)
