[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ Summable fun i => inner (↑f i) (↑g i)
[PROOFSTEP]
refine' summable_of_norm_bounded (fun i => ‖f i‖ * ‖g i‖) (lp.summable_mul _ f g) _
[GOAL]
case refine'_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ Real.IsConjugateExponent (ENNReal.toReal 2) (ENNReal.toReal 2)
[PROOFSTEP]
rw [Real.isConjugateExponent_iff]
[GOAL]
case refine'_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ ENNReal.toReal 2 = ENNReal.toReal 2 / (ENNReal.toReal 2 - 1)
[PROOFSTEP]
norm_num
[GOAL]
case refine'_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ 1 < ENNReal.toReal 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ ∀ (i : ι), ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
i : ι
⊢ ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
[PROOFSTEP]
exact norm_inner_le_norm (𝕜 := 𝕜) _ _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
⊢ ‖f‖ ^ 2 = ↑re (inner f f)
[PROOFSTEP]
calc
  ‖f‖ ^ 2 = ‖f‖ ^ (2 : ℝ≥0∞).toReal := by norm_cast
  _ = ∑' i, ‖f i‖ ^ (2 : ℝ≥0∞).toReal := (lp.norm_rpow_eq_tsum ?_ f)
  _ = ∑' i, ‖f i‖ ^ (2 : ℕ) := by norm_cast
  _ = ∑' i, re ⟪f i, f i⟫ := by
    congr
    funext i
    rw [norm_sq_eq_inner (𝕜 := 𝕜)]
      -- porting note: `simp` couldn't do this anymore
  _ = re (∑' i, ⟪f i, f i⟫) := (IsROrC.reClm.map_tsum ?_).symm
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
⊢ ‖f‖ ^ 2 = ‖f‖ ^ ENNReal.toReal 2
[PROOFSTEP]
norm_cast
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
⊢ ∑' (i : ι), ‖↑f i‖ ^ ENNReal.toReal 2 = ∑' (i : ι), ‖↑f i‖ ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
⊢ ∑' (i : ι), ‖↑f i‖ ^ 2 = ∑' (i : ι), ↑re (inner (↑f i) (↑f i))
[PROOFSTEP]
congr
[GOAL]
case e_f
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
⊢ (fun i => ‖↑f i‖ ^ 2) = fun i => ↑re (inner (↑f i) (↑f i))
[PROOFSTEP]
funext i
[GOAL]
case e_f.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
i : ι
⊢ ‖↑f i‖ ^ 2 = ↑re (inner (↑f i) (↑f i))
[PROOFSTEP]
rw [norm_sq_eq_inner (𝕜 := 𝕜)]
  -- porting note: `simp` couldn't do this anymore
[GOAL]
case calc_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
⊢ 0 < ENNReal.toReal 2
[PROOFSTEP]
norm_num
[GOAL]
case calc_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f : { x // x ∈ lp G 2 }
⊢ Summable fun i => inner (↑f i) (↑f i)
[PROOFSTEP]
exact summable_inner f f
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
⊢ ↑(starRingEnd 𝕜) (inner g f) = inner f g
[PROOFSTEP]
calc
  conj _ = conj (∑' i, ⟪g i, f i⟫) := by congr
  _ = ∑' i, conj ⟪g i, f i⟫ := IsROrC.conjCle.map_tsum
  _ = ∑' i, ⟪f i, g i⟫ := by simp only [inner_conj_symm]
  _ = _ := by congr
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
⊢ ↑(starRingEnd 𝕜) (inner g f) = ↑(starRingEnd 𝕜) (∑' (i : ι), inner (↑g i) (↑f i))
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
⊢ ∑' (i : ι), ↑(starRingEnd 𝕜) (inner (↑g i) (↑f i)) = ∑' (i : ι), inner (↑f i) (↑g i)
[PROOFSTEP]
simp only [inner_conj_symm]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
⊢ ∑' (i : ι), inner (↑f i) (↑g i) = inner f g
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f₁ f₂ g : { x // x ∈ lp G 2 }
⊢ inner (f₁ + f₂) g = inner f₁ g + inner f₂ g
[PROOFSTEP]
calc
  _ = ∑' i, ⟪(f₁ + f₂) i, g i⟫ := ?_
  _ = ∑' i, (⟪f₁ i, g i⟫ + ⟪f₂ i, g i⟫) := by simp only [inner_add_left, Pi.add_apply, coeFn_add]
  _ = (∑' i, ⟪f₁ i, g i⟫) + ∑' i, ⟪f₂ i, g i⟫ := (tsum_add ?_ ?_)
  _ = _ := by congr
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f₁ f₂ g : { x // x ∈ lp G 2 }
⊢ ∑' (i : ι), inner (↑(f₁ + f₂) i) (↑g i) = ∑' (i : ι), (inner (↑f₁ i) (↑g i) + inner (↑f₂ i) (↑g i))
[PROOFSTEP]
simp only [inner_add_left, Pi.add_apply, coeFn_add]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f₁ f₂ g : { x // x ∈ lp G 2 }
⊢ ∑' (i : ι), inner (↑f₁ i) (↑g i) + ∑' (i : ι), inner (↑f₂ i) (↑g i) = inner f₁ g + inner f₂ g
[PROOFSTEP]
congr
[GOAL]
case calc_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f₁ f₂ g : { x // x ∈ lp G 2 }
⊢ inner (f₁ + f₂) g = ∑' (i : ι), inner (↑(f₁ + f₂) i) (↑g i)
[PROOFSTEP]
congr
[GOAL]
case calc_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f₁ f₂ g : { x // x ∈ lp G 2 }
⊢ Summable fun i => inner (↑f₁ i) (↑g i)
[PROOFSTEP]
exact summable_inner f₁ g
[GOAL]
case calc_3
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f₁ f₂ g : { x // x ∈ lp G 2 }
⊢ Summable fun i => inner (↑f₂ i) (↑g i)
[PROOFSTEP]
exact summable_inner f₂ g
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
c : 𝕜
⊢ inner (c • f) g = ↑(starRingEnd 𝕜) c * inner f g
[PROOFSTEP]
calc
  _ = ∑' i, ⟪c • f i, g i⟫ := ?_
  _ = ∑' i, conj c * ⟪f i, g i⟫ := by simp only [inner_smul_left]
  _ = conj c * ∑' i, ⟪f i, g i⟫ := tsum_mul_left
  _ = _ := ?_
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
c : 𝕜
⊢ ∑' (i : ι), inner (c • ↑f i) (↑g i) = ∑' (i : ι), ↑(starRingEnd 𝕜) c * inner (↑f i) (↑g i)
[PROOFSTEP]
simp only [inner_smul_left]
[GOAL]
case calc_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
c : 𝕜
⊢ inner (c • f) g = ∑' (i : ι), inner (c • ↑f i) (↑g i)
[PROOFSTEP]
simp only [coeFn_smul, Pi.smul_apply]
[GOAL]
case calc_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
src✝ : NormedAddCommGroup { x // x ∈ lp G 2 } := normedAddCommGroup
f g : { x // x ∈ lp G 2 }
c : 𝕜
⊢ ↑(starRingEnd 𝕜) c * ∑' (i : ι), inner (↑f i) (↑g i) = ↑(starRingEnd 𝕜) c * inner f g
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ inner (lp.single 2 i a) f = inner a (↑f i)
[PROOFSTEP]
refine' (hasSum_inner (lp.single 2 i a) f).unique _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ HasSum (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) (inner a (↑f i))
[PROOFSTEP]
convert hasSum_ite_eq i ⟪a, f i⟫ using 1
[GOAL]
case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) = fun b' => if b' = i then inner a (↑f i) else 0
[PROOFSTEP]
ext j
[GOAL]
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
⊢ inner (↑(lp.single 2 i a) j) (↑f j) = if j = i then inner a (↑f i) else 0
[PROOFSTEP]
rw [lp.single_apply]
[GOAL]
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
⊢ inner (if h : j = i then (_ : i = j) ▸ a else 0) (↑f j) = if j = i then inner a (↑f i) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
h : j = i
⊢ inner ((_ : i = j) ▸ a) (↑f j) = inner a (↑f i)
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f : { x // x ∈ lp G 2 }
j : ι
a : G j
⊢ inner ((_ : j = j) ▸ a) (↑f j) = inner a (↑f j)
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
h : ¬j = i
⊢ inner 0 (↑f j) = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ inner f (lp.single 2 i a) = inner (↑f i) a
[PROOFSTEP]
simpa [inner_conj_symm] using congr_arg conj (@inner_single_left _ 𝕜 _ _ _ _ i a f)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
⊢ Summable fun i => ↑(V i) (↑f i)
[PROOFSTEP]
rw [hV.summable_iff_norm_sq_summable]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
⊢ Summable fun i => ‖↑f i‖ ^ 2
[PROOFSTEP]
convert (lp.memℓp f).summable _
[GOAL]
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
x✝ : ι
⊢ ‖↑f x✝‖ ^ 2 = ‖↑f x✝‖ ^ ENNReal.toReal 2
[PROOFSTEP]
norm_cast
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
⊢ 0 < ENNReal.toReal 2
[PROOFSTEP]
norm_num
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f g : { x // x ∈ lp G 2 }
⊢ (fun f => ∑' (i : ι), ↑(V i) (↑f i)) (f + g) =
    (fun f => ∑' (i : ι), ↑(V i) (↑f i)) f + (fun f => ∑' (i : ι), ↑(V i) (↑f i)) g
[PROOFSTEP]
simp only [tsum_add (hV.summable_of_lp f) (hV.summable_of_lp g), lp.coeFn_add, Pi.add_apply, LinearIsometry.map_add]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
c : 𝕜
f : { x // x ∈ lp G 2 }
⊢ AddHom.toFun
      { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
        map_add' :=
          (_ :
            ∀ (f g : { x // x ∈ lp G 2 }),
              ∑' (x : ι), ↑(V x) (↑f x + ↑g x) = ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
      (c • f) =
    ↑(RingHom.id 𝕜) c •
      AddHom.toFun
        { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
          map_add' :=
            (_ :
              ∀ (f g : { x // x ∈ lp G 2 }),
                ∑' (x : ι), ↑(V x) (↑f x + ↑g x) = ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
        f
[PROOFSTEP]
simpa only [LinearIsometry.map_smul, Pi.smul_apply, lp.coeFn_smul] using tsum_const_smul c (hV.summable_of_lp f)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
⊢ ‖↑{
            toAddHom :=
              { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                map_add' :=
                  (_ :
                    ∀ (f g : { x // x ∈ lp G 2 }),
                      ∑' (x : ι), ↑(V x) (↑f x + ↑g x) = ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) },
            map_smul' :=
              (_ :
                ∀ (c : 𝕜) (f : { x // x ∈ lp G 2 }),
                  AddHom.toFun
                      { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                        map_add' :=
                          (_ :
                            ∀ (f g : { x // x ∈ lp G 2 }),
                              ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                      (c • f) =
                    ↑(RingHom.id 𝕜) c •
                      AddHom.toFun
                        { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                          map_add' :=
                            (_ :
                              ∀ (f g : { x // x ∈ lp G 2 }),
                                ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                  ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                        f) }
        f‖ =
    ‖f‖
[PROOFSTEP]
classical
  -- needed for lattice instance on `Finset ι`, for `Filter.atTop_neBot`
have H : 0 < (2 : ℝ≥0∞).toReal := by norm_num
suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
  exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
refine' tendsto_nhds_unique _ (lp.hasSum_norm H f)
convert (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
ext s
exact_mod_cast (hV.norm_sum f s).symm
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
⊢ ‖↑{
            toAddHom :=
              { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                map_add' :=
                  (_ :
                    ∀ (f g : { x // x ∈ lp G 2 }),
                      ∑' (x : ι), ↑(V x) (↑f x + ↑g x) = ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) },
            map_smul' :=
              (_ :
                ∀ (c : 𝕜) (f : { x // x ∈ lp G 2 }),
                  AddHom.toFun
                      { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                        map_add' :=
                          (_ :
                            ∀ (f g : { x // x ∈ lp G 2 }),
                              ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                      (c • f) =
                    ↑(RingHom.id 𝕜) c •
                      AddHom.toFun
                        { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                          map_add' :=
                            (_ :
                              ∀ (f g : { x // x ∈ lp G 2 }),
                                ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                  ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                        f) }
        f‖ =
    ‖f‖
[PROOFSTEP]
have H : 0 < (2 : ℝ≥0∞).toReal := by norm_num
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
⊢ 0 < ENNReal.toReal 2
[PROOFSTEP]
norm_num
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
H : 0 < ENNReal.toReal 2
⊢ ‖↑{
            toAddHom :=
              { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                map_add' :=
                  (_ :
                    ∀ (f g : { x // x ∈ lp G 2 }),
                      ∑' (x : ι), ↑(V x) (↑f x + ↑g x) = ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) },
            map_smul' :=
              (_ :
                ∀ (c : 𝕜) (f : { x // x ∈ lp G 2 }),
                  AddHom.toFun
                      { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                        map_add' :=
                          (_ :
                            ∀ (f g : { x // x ∈ lp G 2 }),
                              ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                      (c • f) =
                    ↑(RingHom.id 𝕜) c •
                      AddHom.toFun
                        { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                          map_add' :=
                            (_ :
                              ∀ (f g : { x // x ∈ lp G 2 }),
                                ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                  ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                        f) }
        f‖ =
    ‖f‖
[PROOFSTEP]
suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
  exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
H : 0 < ENNReal.toReal 2
this : ‖∑' (i : ι), ↑(V i) (↑f i)‖ ^ ENNReal.toReal 2 = ‖f‖ ^ ENNReal.toReal 2
⊢ ‖↑{
            toAddHom :=
              { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                map_add' :=
                  (_ :
                    ∀ (f g : { x // x ∈ lp G 2 }),
                      ∑' (x : ι), ↑(V x) (↑f x + ↑g x) = ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) },
            map_smul' :=
              (_ :
                ∀ (c : 𝕜) (f : { x // x ∈ lp G 2 }),
                  AddHom.toFun
                      { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                        map_add' :=
                          (_ :
                            ∀ (f g : { x // x ∈ lp G 2 }),
                              ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                      (c • f) =
                    ↑(RingHom.id 𝕜) c •
                      AddHom.toFun
                        { toFun := fun f => ∑' (i : ι), ↑(V i) (↑f i),
                          map_add' :=
                            (_ :
                              ∀ (f g : { x // x ∈ lp G 2 }),
                                ∑' (x : ι), ↑(V x) (↑f x + ↑g x) =
                                  ∑' (b : ι), ↑(V b) (↑f b) + ∑' (b : ι), ↑(V b) (↑g b)) }
                        f) }
        f‖ =
    ‖f‖
[PROOFSTEP]
exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
H : 0 < ENNReal.toReal 2
⊢ ‖∑' (i : ι), ↑(V i) (↑f i)‖ ^ ENNReal.toReal 2 = ‖f‖ ^ ENNReal.toReal 2
[PROOFSTEP]
refine' tendsto_nhds_unique _ (lp.hasSum_norm H f)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
H : 0 < ENNReal.toReal 2
⊢ Tendsto (fun s => ∑ b in s, (fun i => ‖↑f i‖ ^ ENNReal.toReal 2) b) atTop
    (𝓝 (‖∑' (i : ι), ↑(V i) (↑f i)‖ ^ ENNReal.toReal 2))
[PROOFSTEP]
convert (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
[GOAL]
case h.e'_3
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
H : 0 < ENNReal.toReal 2
⊢ (fun s => ∑ b in s, (fun i => ‖↑f i‖ ^ ENNReal.toReal 2) b) = fun a =>
    ‖∑ b in a, (fun i => ↑(V i) (↑f i)) b‖ ^ ENNReal.toReal 2
[PROOFSTEP]
ext s
[GOAL]
case h.e'_3.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : { x // x ∈ lp G 2 }
H : 0 < ENNReal.toReal 2
s : Finset ι
⊢ ∑ b in s, (fun i => ‖↑f i‖ ^ ENNReal.toReal 2) b = ‖∑ b in s, (fun i => ↑(V i) (↑f i)) b‖ ^ ENNReal.toReal 2
[PROOFSTEP]
exact_mod_cast (hV.norm_sum f s).symm
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
i : ι
x : G i
⊢ ↑(OrthogonalFamily.linearIsometry hV) (lp.single 2 i x) = ↑(V i) x
[PROOFSTEP]
rw [hV.linearIsometry_apply, ← tsum_ite_eq i (V i x)]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
i : ι
x : G i
⊢ ∑' (i_1 : ι), ↑(V i_1) (↑(lp.single 2 i x) i_1) = ∑' (b' : ι), if b' = i then ↑(V i) x else 0
[PROOFSTEP]
congr
[GOAL]
case e_f
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
i : ι
x : G i
⊢ (fun i_1 => ↑(V i_1) (↑(lp.single 2 i x) i_1)) = fun b' => if b' = i then ↑(V i) x else 0
[PROOFSTEP]
ext j
[GOAL]
case e_f.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
i : ι
x : G i
j : ι
⊢ ↑(V j) (↑(lp.single 2 i x) j) = if j = i then ↑(V i) x else 0
[PROOFSTEP]
rw [lp.single_apply]
[GOAL]
case e_f.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
i : ι
x : G i
j : ι
⊢ ↑(V j) (if h : j = i then (_ : i = j) ▸ x else 0) = if j = i then ↑(V i) x else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
i : ι
x : G i
j : ι
h : j = i
⊢ ↑(V j) (if h : j = i then (_ : i = j) ▸ x else 0) = ↑(V i) x
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
j : ι
x : G j
⊢ ↑(V j) (if h : j = j then (_ : j = j) ▸ x else 0) = ↑(V j) x
[PROOFSTEP]
simp
[GOAL]
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
i : ι
x : G i
j : ι
h : ¬j = i
⊢ ↑(V j) (if h : j = i then (_ : i = j) ▸ x else 0) = 0
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(OrthogonalFamily.linearIsometry hV) (DFinsupp.sum W₀ (lp.single 2)) = DFinsupp.sum W₀ fun i => ↑(V i)
[PROOFSTEP]
have :
  hV.linearIsometry (∑ i in W₀.support, lp.single 2 i (W₀ i)) =
    ∑ i in W₀.support, hV.linearIsometry (lp.single 2 i (W₀ i)) :=
  hV.linearIsometry.toLinearMap.map_sum
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
W₀ : Π₀ (i : ι), G i
this :
  ↑(OrthogonalFamily.linearIsometry hV) (∑ i in DFinsupp.support W₀, lp.single 2 i (↑W₀ i)) =
    ∑ i in DFinsupp.support W₀, ↑(OrthogonalFamily.linearIsometry hV) (lp.single 2 i (↑W₀ i))
⊢ ↑(OrthogonalFamily.linearIsometry hV) (DFinsupp.sum W₀ (lp.single 2)) = DFinsupp.sum W₀ fun i => ↑(V i)
[PROOFSTEP]
simp (config := { contextual := true }) [DFinsupp.sum, this]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap =
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap ≤
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
[PROOFSTEP]
rintro x ⟨f, rfl⟩
[GOAL]
case refine'_1.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
⊢ ↑(OrthogonalFamily.linearIsometry hV).toLinearMap f ∈
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
[PROOFSTEP]
refine' mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (eventually_of_forall _)
[GOAL]
case refine'_1.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
⊢ ∀ (x : Finset ι), ∑ b in x, (fun i => ↑(V i) (↑f i)) b ∈ ↑(⨆ (i : ι), LinearMap.range (V i).toLinearMap)
[PROOFSTEP]
intro s
[GOAL]
case refine'_1.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∑ b in s, (fun i => ↑(V i) (↑f i)) b ∈ ↑(⨆ (i : ι), LinearMap.range (V i).toLinearMap)
[PROOFSTEP]
rw [SetLike.mem_coe]
[GOAL]
case refine'_1.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∑ b in s, (fun i => ↑(V i) (↑f i)) b ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
[PROOFSTEP]
refine' sum_mem _
[GOAL]
case refine'_1.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∀ (c : ι), c ∈ s → (fun i => ↑(V i) (↑f i)) c ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
[PROOFSTEP]
intro i _
[GOAL]
case refine'_1.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
i : ι
a✝ : i ∈ s
⊢ (fun i => ↑(V i) (↑f i)) i ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
[PROOFSTEP]
refine' mem_iSup_of_mem i _
[GOAL]
case refine'_1.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
i : ι
a✝ : i ∈ s
⊢ (fun i => ↑(V i) (↑f i)) i ∈ LinearMap.range (V i).toLinearMap
[PROOFSTEP]
exact LinearMap.mem_range_self _ (f i)
[GOAL]
case refine'_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap) ≤
    LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
[PROOFSTEP]
apply topologicalClosure_minimal
[GOAL]
case refine'_2.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ ⨆ (i : ι), LinearMap.range (V i).toLinearMap ≤ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case refine'_2.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ ∀ (i : ι), LinearMap.range (V i).toLinearMap ≤ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
[PROOFSTEP]
rintro i x ⟨x, rfl⟩
[GOAL]
case refine'_2.h.intro
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
i : ι
x : G i
⊢ ↑(V i).toLinearMap x ∈ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
[PROOFSTEP]
use lp.single 2 i x
[GOAL]
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
i : ι
x : G i
⊢ ↑(OrthogonalFamily.linearIsometry hV).toLinearMap (lp.single 2 i x) = ↑(V i).toLinearMap x
[PROOFSTEP]
exact hV.linearIsometry_apply_single x
[GOAL]
case refine'_2.ht
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ IsClosed ↑(LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap)
[PROOFSTEP]
exact hV.linearIsometry.isometry.uniformInducing.isComplete_range.isClosed
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
⊢ Function.Surjective ↑(OrthogonalFamily.linearIsometry hVortho)
[PROOFSTEP]
rw [← LinearIsometry.coe_toLinearMap]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
⊢ Function.Surjective ↑(OrthogonalFamily.linearIsometry hVortho).toLinearMap
[PROOFSTEP]
exact LinearMap.range_eq_top.mp (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace { x // x ∈ F i }
hFortho : OrthogonalFamily 𝕜 (fun i => { x // x ∈ F i }) fun i => subtypeₗᵢ (F i)
hFtotal : ⊤ ≤ topologicalClosure (⨆ (i : ι), F i)
⊢ ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (subtypeₗᵢ (F i)).toLinearMap)
[PROOFSTEP]
simpa [subtypeₗᵢ_toLinearMap, range_subtype] using hFtotal
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
w : { x // x ∈ lp G 2 }
⊢ ↑(LinearIsometryEquiv.symm (linearIsometryEquiv hV)) w = ∑' (i : ι), ↑(V i) (↑w i)
[PROOFSTEP]
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
w : { x // x ∈ lp G 2 }
⊢ HasSum (fun i => ↑(V i) (↑w i)) (↑(LinearIsometryEquiv.symm (linearIsometryEquiv hV)) w)
[PROOFSTEP]
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.hasSum_linearIsometry]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
i : ι
x : G i
⊢ ↑(LinearIsometryEquiv.symm (linearIsometryEquiv hV)) (lp.single 2 i x) = ↑(V i) x
[PROOFSTEP]
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply_single]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(LinearIsometryEquiv.symm (linearIsometryEquiv hV)) (DFinsupp.sum W₀ (lp.single 2)) = DFinsupp.sum W₀ fun i => ↑(V i)
[PROOFSTEP]
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(↑(linearIsometryEquiv hV) (DFinsupp.sum W₀ fun i => ↑(V i))) = ↑W₀
[PROOFSTEP]
rw [← hV.linearIsometryEquiv_symm_apply_dfinsupp_sum_single]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(↑(linearIsometryEquiv hV) (↑(LinearIsometryEquiv.symm (linearIsometryEquiv hV)) (DFinsupp.sum W₀ (lp.single 2)))) =
    ↑W₀
[PROOFSTEP]
rw [LinearIsometryEquiv.apply_symm_apply]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(DFinsupp.sum W₀ (lp.single 2)) = ↑W₀
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
i : ι
⊢ ↑(DFinsupp.sum W₀ (lp.single 2)) i = ↑W₀ i
[PROOFSTEP]
simp (config := { contextual := true }) [DFinsupp.sum, lp.single_apply]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
⊢ ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E (_ : ‖v i‖ = 1)).toLinearMap)
[PROOFSTEP]
convert hsp
[GOAL]
case h.e'_4.h.e'_9
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
⊢ ⨆ (i : ι), LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E (_ : ‖v i‖ = 1)).toLinearMap = span 𝕜 (Set.range v)
[PROOFSTEP]
simp [← LinearMap.span_singleton_eq_range, ← Submodule.span_iUnion]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ IsHilbertSum 𝕜 (fun b => { x // x ∈ bif b then K else Kᗮ }) fun b => subtypeₗᵢ (bif b then K else Kᗮ)
[PROOFSTEP]
have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
  intro b
  cases b <;>
    first
    | exact instOrthogonalCompleteSpace K
    | assumption
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
[PROOFSTEP]
intro b
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
b : Bool
⊢ CompleteSpace { x // x ∈ bif b then K else Kᗮ }
[PROOFSTEP]
cases b
[GOAL]
case false
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif false then K else Kᗮ }
[PROOFSTEP]
first
| exact instOrthogonalCompleteSpace K
| assumption
[GOAL]
case false
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif false then K else Kᗮ }
[PROOFSTEP]
exact instOrthogonalCompleteSpace K
[GOAL]
case true
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif true then K else Kᗮ }
[PROOFSTEP]
first
| exact instOrthogonalCompleteSpace K
| assumption
[GOAL]
case true
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif true then K else Kᗮ }
[PROOFSTEP]
exact instOrthogonalCompleteSpace K
[GOAL]
case true
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
⊢ CompleteSpace { x // x ∈ bif true then K else Kᗮ }
[PROOFSTEP]
assumption
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ IsHilbertSum 𝕜 (fun b => { x // x ∈ bif b then K else Kᗮ }) fun b => subtypeₗᵢ (bif b then K else Kᗮ)
[PROOFSTEP]
refine' IsHilbertSum.mkInternal _ K.orthogonalFamily_self _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤ topologicalClosure (⨆ (i : Bool), bif i then K else Kᗮ)
[PROOFSTEP]
refine' le_trans _ (Submodule.le_topologicalClosure _)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤ ⨆ (i : Bool), bif i then K else Kᗮ
[PROOFSTEP]
rw [iSup_bool_eq, cond, cond]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ ⊤ ≤
    (match true with
      | true => K
      | false => Kᗮ) ⊔
      match false with
      | true => K
      | false => Kᗮ
[PROOFSTEP]
refine' Codisjoint.top_le _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
K : Submodule 𝕜 E
hK : CompleteSpace { x // x ∈ K }
this : ∀ (b : Bool), CompleteSpace { x // x ∈ bif b then K else Kᗮ }
⊢ Codisjoint
    (match true with
    | true => K
    | false => Kᗮ)
    (match false with
    | true => K
    | false => Kᗮ)
[PROOFSTEP]
exact Submodule.isCompl_orthogonal_of_completeSpace.codisjoint
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
i : ι
⊢ ↑b.repr ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) = lp.single 2 i 1
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ ↑(↑b.repr v) i = inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) v
[PROOFSTEP]
rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ ↑(↑b.repr v) i = inner 1 (↑(↑b.repr v) i)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ Orthonormal 𝕜 fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)
[PROOFSTEP]
rw [orthonormal_iff_ite]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ ∀ (i j : ι),
    inner (↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
        (↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 j 1)) =
      if i = j then 1 else 0
[PROOFSTEP]
intro i j
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner (↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) (↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 j 1)) =
    if i = j then 1 else 0
[PROOFSTEP]
rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left, lp.single_apply]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ inner 1 (if h : i = j then (_ : j = i) ▸ 1 else 0) = if i = j then 1 else 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
⊢ HasSum (fun i => ↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)
    (↑(LinearIsometryEquiv.symm b.repr) f)
[PROOFSTEP]
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
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
H :
  (fun i => ↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) = fun b_1 =>
    ↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
      ((fun i => lp.single 2 i (↑f i)) b_1)
⊢ HasSum (fun i => ↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)
    (↑(LinearIsometryEquiv.symm b.repr) f)
[PROOFSTEP]
rw [H]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
H :
  (fun i => ↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) = fun b_1 =>
    ↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
      ((fun i => lp.single 2 i (↑f i)) b_1)
⊢ HasSum
    (fun b_1 =>
      ↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
        ((fun i => lp.single 2 i (↑f i)) b_1))
    (↑(LinearIsometryEquiv.symm b.repr) f)
[PROOFSTEP]
have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.two_ne_top f
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
H :
  (fun i => ↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) = fun b_1 =>
    ↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
      ((fun i => lp.single 2 i (↑f i)) b_1)
this : HasSum (fun i => lp.single 2 i (↑f i)) f
⊢ HasSum
    (fun b_1 =>
      ↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
        ((fun i => lp.single 2 i (↑f i)) b_1))
    (↑(LinearIsometryEquiv.symm b.repr) f)
[PROOFSTEP]
exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this
[GOAL]
case H
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
⊢ (fun i => ↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) = fun b_1 =>
    ↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
      ((fun i => lp.single 2 i (↑f i)) b_1)
[PROOFSTEP]
ext i
[GOAL]
case H.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
i : ι
⊢ ↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i =
    ↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr)) ((fun i => lp.single 2 i (↑f i)) i)
[PROOFSTEP]
apply b.repr.injective
[GOAL]
case H.h.a
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
i : ι
⊢ ↑b.repr (↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) =
    ↑b.repr
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
        ((fun i => lp.single 2 i (↑f i)) i))
[PROOFSTEP]
letI : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
i : ι
⊢ NormedSpace 𝕜 { x // x ∈ lp (fun _i => 𝕜) 2 }
[PROOFSTEP]
infer_instance
[GOAL]
case H.h.a
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
i : ι
this : NormedSpace 𝕜 { x // x ∈ lp (fun _i => 𝕜) 2 } := inferInstance
⊢ ↑b.repr (↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) =
    ↑b.repr
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
        ((fun i => lp.single 2 i (↑f i)) i))
[PROOFSTEP]
have : lp.single (E := (fun _ : ι => 𝕜)) 2 i (f i * 1) = f i • lp.single 2 i 1 :=
  lp.single_smul (E := (fun _ : ι => 𝕜)) 2 i (1 : 𝕜) (f i)
[GOAL]
case H.h.a
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
i : ι
this✝ : NormedSpace 𝕜 { x // x ∈ lp (fun _i => 𝕜) 2 } := inferInstance
this : lp.single 2 i (↑f i * 1) = ↑f i • lp.single 2 i 1
⊢ ↑b.repr (↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) =
    ↑b.repr
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
        ((fun i => lp.single 2 i (↑f i)) i))
[PROOFSTEP]
rw [mul_one] at this 
[GOAL]
case H.h.a
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
i : ι
this✝ : NormedSpace 𝕜 { x // x ∈ lp (fun _i => 𝕜) 2 } := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ ↑b.repr (↑f i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) =
    ↑b.repr
      (↑(LinearIsometryEquiv.toContinuousLinearEquiv (LinearIsometryEquiv.symm b.repr))
        ((fun i => lp.single 2 i (↑f i)) i))
[PROOFSTEP]
rw [LinearIsometryEquiv.map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
[GOAL]
case H.h.a
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
f : { x // x ∈ lp (fun i => 𝕜) 2 }
i : ι
this✝ : NormedSpace 𝕜 { x // x ∈ lp (fun _i => 𝕜) 2 } := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ lp.single 2 i (↑f i) = ↑b.repr (↑(LinearIsometryEquiv.symm b.repr) ((fun i => lp.single 2 i (↑f i)) i))
[PROOFSTEP]
exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) x
[PROOFSTEP]
simpa using b.hasSum_repr_symm (b.repr x)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))) = ⊤
[PROOFSTEP]
classical
rw [eq_top_iff]
rintro x -
refine' mem_closure_of_tendsto (b.hasSum_repr x) (eventually_of_forall _)
intro s
simp only [SetLike.mem_coe]
refine' sum_mem _
rintro i -
refine' smul_mem _ _ _
exact subset_span ⟨i, rfl⟩
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))) = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ ⊤ ≤ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
[PROOFSTEP]
rintro x -
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ x ∈ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
[PROOFSTEP]
refine' mem_closure_of_tendsto (b.hasSum_repr x) (eventually_of_forall _)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ ∀ (x_1 : Finset ι),
    ∑ b_1 in x_1, (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) b_1 ∈
      ↑(span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
[PROOFSTEP]
intro s
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ b_1 in s, (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) b_1 ∈
    ↑(span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
[PROOFSTEP]
simp only [SetLike.mem_coe]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ x_1 in s, ↑(↑b.repr x) x_1 • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 x_1 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
[PROOFSTEP]
refine' sum_mem _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∀ (c : ι),
    c ∈ s →
      ↑(↑b.repr x) c • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 c 1) ∈
        span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
[PROOFSTEP]
rintro i -
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(↑b.repr x) i • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
[PROOFSTEP]
refine' smul_mem _ _ _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
[PROOFSTEP]
exact subset_span ⟨i, rfl⟩
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
⊢ HasSum
    (fun i =>
      inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
        inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y)
    (inner x y)
[PROOFSTEP]
convert (b.hasSum_repr y).mapL (innerSL _ x) using 1
[GOAL]
case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
⊢ (fun i =>
      inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
        inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y) =
    fun b_1 =>
    ↑(↑(innerSL 𝕜) x) (↑(↑b.repr y) b_1 • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) b_1)
[PROOFSTEP]
ext i
[GOAL]
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ inner x ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) *
      inner ((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) y =
    ↑(↑(innerSL 𝕜) x) (↑(↑b.repr y) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)
[PROOFSTEP]
rw [innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : Fintype ι
b : HilbertBasis ι 𝕜 E
⊢ ⊤ ≤ span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
[PROOFSTEP]
refine' Eq.ge _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : Fintype ι
b : HilbertBasis ι 𝕜 E
⊢ span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) = ⊤
[PROOFSTEP]
have := (span 𝕜 (Finset.univ.image b : Set E)).closed_of_finiteDimensional
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : Fintype ι
b : HilbertBasis ι 𝕜 E
this : IsClosed ↑(span 𝕜 ↑(Finset.image (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) Finset.univ))
⊢ span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) = ⊤
[PROOFSTEP]
simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, HilbertBasis.dense_span] using
  this.submodule_topologicalClosure_eq.symm
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
b : HilbertBasis ι 𝕜 { x // x ∈ U }
x : E
⊢ HasSum
    (fun i =>
      inner (↑((fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)) x •
        (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)
    (↑(orthogonalProjection U) x)
[PROOFSTEP]
simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
  b.hasSum_repr (orthogonalProjection U x)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))) ≤
    topologicalClosure
      (⨆ (J : Finset ι), span 𝕜 ↑(Finset.image (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) J))
[PROOFSTEP]
simp_rw [← Submodule.span_iUnion]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))) ≤
    topologicalClosure
      (span 𝕜 (⋃ (i : Finset ι), ↑(Finset.image (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)))
[PROOFSTEP]
exact
  topologicalClosure_mono
    (span_mono <|
      Set.range_subset_iff.mpr fun i =>
        Set.mem_iUnion_of_mem { i } <| Finset.mem_coe.mpr <| Finset.mem_image_of_mem _ <| Finset.mem_singleton_self i)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
v : ι → E
hv : Orthonormal 𝕜 v
h : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
i : ι
⊢ ↑(LinearIsometryEquiv.symm
          (IsHilbertSum.linearIsometryEquiv
            (_ : IsHilbertSum 𝕜 (fun x => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (_ : ‖v i‖ = 1))))
      (lp.single 2 i 1) =
    v i
[PROOFSTEP]
rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply, one_smul]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
⊢ (fun i => ↑(LinearIsometryEquiv.symm (HilbertBasis.mk hv hsp).repr) (lp.single 2 i 1)) = v
[PROOFSTEP]
apply funext <| Orthonormal.linearIsometryEquiv_symm_apply_single_one hv hsp
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
v : ι → E
hv : Orthonormal 𝕜 v
hsp : (span 𝕜 (Set.range v))ᗮ = ⊥
⊢ ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
[PROOFSTEP]
rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
v : ι → E
hv : Orthonormal 𝕜 v
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ ⊤ ≤ topologicalClosure (span 𝕜 (Set.range ↑b))
[PROOFSTEP]
simpa only [← OrthonormalBasis.coe_toBasis, b.toBasis.span_eq, eq_top_iff] using @subset_closure E _ _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
v : ι → E
hv : Orthonormal 𝕜 v
s : Set E
hs : Orthonormal 𝕜 Subtype.val
w : Set E
hws : w ⊇ s
hw_ortho : Orthonormal 𝕜 Subtype.val
hw_max : ∀ (u : Set E), u ⊇ w → Orthonormal 𝕜 Subtype.val → u = w
⊢ (span 𝕜 (Set.range Subtype.val))ᗮ = ⊥
[PROOFSTEP]
simpa [maximal_orthonormal_iff_orthogonalComplement_eq_bot hw_ortho] using hw_max
