-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_products_summable (hv : Orthonormal 𝕜 v) :
    Summable fun i => ‖⟪v i, x⟫‖ ^ 2

Proof state:
case h.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
s : Finset ι
⊢ (fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2) s ≤ ‖x‖ ^ 2

Tactic:
exact hv.sum_inner_products_le x

Result:
no goals

Proof state:
case h.hf
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ IsLUB (Set.range fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2) (⨆ s, ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)

Tactic:
refine isLUB_ciSup ?_

Result:
case h.hf
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ BddAbove (Set.range fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)

Proof state:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
b : ι
⊢ 0 ≤ ‖inner (v b) x‖ ^ 2

Tactic:
simp only [norm_nonneg, pow_nonneg]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ HasSum (fun i => ‖inner (v i) x‖ ^ 2) (⨆ s, ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)

Tactic:
apply hasSum_of_isLUB_of_nonneg

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (i : ι), 0 ≤ ‖inner (v i) x‖ ^ 2

case h.hf
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ IsLUB (Set.range fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2) (⨆ s, ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ Summable fun i => ‖inner (v i) x‖ ^ 2

Tactic:
use ⨆ s : Finset ι, ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ HasSum (fun i => ‖inner (v i) x‖ ^ 2) (⨆ s, ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ‖x‖ ^ 2 ∈ upperBounds (Set.range fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)

Tactic:
rintro y ⟨s, rfl⟩

Result:
case h.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
s : Finset ι
⊢ (fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2) s ≤ ‖x‖ ^ 2

Proof state:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (i : ι), 0 ≤ ‖inner (v i) x‖ ^ 2

Tactic:
intro b

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
b : ι
⊢ 0 ≤ ‖inner (v b) x‖ ^ 2

Proof state:
case h.hf
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ BddAbove (Set.range fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)

Tactic:
use ‖x‖ ^ 2

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ‖x‖ ^ 2 ∈ upperBounds (Set.range fun s => ∑ i ∈ s, ‖inner (v i) x‖ ^ 2)