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

Initializing...

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