case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ gramSchmidt 𝕜 f i = f i
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
⊢ gramSchmidt 𝕜 f = f
ext i
case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = f i
case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ gramSchmidt 𝕜 f i = f i
rw [gramSchmidt_def]
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = f i - 0

𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - 0 = f i
case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = f i
trans f i - 0
case e_a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = 0
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = f i - 0
congr
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∀ (x : ι), x ∈ Finset.Iio i → ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x})) (f i)) = 0
case e_a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = 0
apply Finset.sum_eq_zero
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i)) = 0
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∀ (x : ι), x ∈ Finset.Iio i → ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x})) (f i)) = 0
intro j hj
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i) = 0
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i)) = 0
rw [coe_eq_zero]
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i) = 0
suffices span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i by
  apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
  rw [mem_orthogonal_singleton_iff_inner_left]
  rw [← mem_orthogonal_singleton_iff_inner_right]
  exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ∀ ⦃u : E⦄, u ∈ f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {f i} → inner u v = 0
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
rw [isOrtho_span]
case e_a.h.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ inner (f k) (f i) = 0
case e_a.h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ∀ ⦃u : E⦄, u ∈ f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {f i} → inner u v = 0
rintro u ⟨k, hk, rfl⟩ v (rfl : v = f i)
case e_a.h.intro.intro.a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ k ≠ i
case e_a.h.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ inner (f k) (f i) = 0
apply hf
no goals
case e_a.h.intro.intro.a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ k ≠ i
exact (lt_of_le_of_lt hk (Finset.mem_Iio.mp hj)).ne
case hv
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ f i ∈ (span 𝕜 {gramSchmidt 𝕜 f j})ᗮ
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ ↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i) = 0
apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
case hv
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ inner (f i) (gramSchmidt 𝕜 f j) = 0
case hv
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ f i ∈ (span 𝕜 {gramSchmidt 𝕜 f j})ᗮ
rw [mem_orthogonal_singleton_iff_inner_left]
case hv
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ gramSchmidt 𝕜 f j ∈ (span 𝕜 {f i})ᗮ
case hv
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ inner (f i) (gramSchmidt 𝕜 f j) = 0
rw [← mem_orthogonal_singleton_iff_inner_right]
no goals
case hv
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ gramSchmidt 𝕜 f j ∈ (span 𝕜 {f i})ᗮ
exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))
no goals
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - 0 = f i
simp