English
Equivalence of representations: the sum formula holds when applying the inverse map to ℓ²-coordinates.
Русский
Эквивалентность формул суммы: сумма образов равна обратному отображению на ℓ²-координатах.
LaTeX
$$$ HasSum (\\lambda i, LinearIsometry.instFunLike.coe (V i) (b_i)) (b.repr.symm f) $$$
Lean4
protected theorem hasSum_repr_symm (b : HilbertBasis ι 𝕜 E) (f : ℓ²(ι, 𝕜)) :
HasSum (fun i => f i • b i) (b.repr.symm f) := by
classical
suffices H :
(fun i : ι => f i • b i) = fun b_1 : ι =>
b.repr.symm.toContinuousLinearEquiv <| (fun i : ι => lp.single 2 i (f i) (E := (fun _ : ι => 𝕜))) b_1
by
rw [H]
have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.ofNat_ne_top f
exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this
ext i
apply b.repr.injective
letI : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance
have : lp.single (E := (fun _ : ι => 𝕜)) 2 i (f i * 1) = f i • lp.single 2 i 1 :=
lp.single_smul (E := (fun _ : ι => 𝕜)) 2 i (f i) (1 : 𝕜)
rw [mul_one] at this
rw [LinearIsometryEquiv.map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm
