(i : Fin d) (x : lpFiniteModes (Occ d)) (α : Occ d) : (((ann i (ann i x) : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) α = (Real.sqrt ((α i : ℝ) + 1) : ℂ) * (Real.sqrt ((α i...

Initializing...

(i : Fin d) (x : lpFiniteModes (Occ d)) (α : Occ d) : (((ann i (ann i x) : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) α = (Real.sqrt ((α i : ℝ) + 1) : ℂ) * (Real.sqrt ((α i... · Prove2Me