Gram–Schmidt process for three vectors...

Stream: new members

[Ilmārs Cīrulis]

I can't prove that third vector of basis is nonzero. I tried to do it directly, but, well, got tangled in all these inner products. Maybe there's some simpler way that I simply don't know.

import Mathlib

open InnerProductGeometry

variable (V: Type)
variable [NormedAddCommGroup V]
variable [InnerProductSpace ℝ V]

noncomputable def proj (x y: V): V := (@inner ℝ V _ x y / inner x x) • x
noncomputable def unit (x: V): V := ‖x‖⁻¹ • x
noncomputable def basis (x y z: V) := (x, y - proj _ x y, z - proj _ x z - proj _ (y - proj _ x y) z)
noncomputable def norm_basis (x y z: V) :=
  let (u1, u2, u3) := basis _ x y z
  (unit _ u1, unit _ u2, unit _ u3)

theorem all_ortogonal (x y z: V) (Hx: x ≠ 0) (Hy: y ≠ 0) (Hz: z ≠ 0)
    (Hxy: angle x y ≠ 0 ∧ angle x y ≠ Real.pi):
    let (e1, e2, e3) := norm_basis _ x y z
    inner e1 e2 = (0: ℝ) ∧ inner e1 e3 = (0: ℝ) ∧ inner e2 e3 = (0: ℝ) := by
  done --- proved this

theorem norm_of_unit (x: V) (H: x ≠ 0): ‖unit _ x‖ = 1 := by
  unfold unit; rw [norm_smul]; simp
  have H0: ‖x‖ ≠ 0 := by simp; exact H
  field_simp

theorem e3_normed (x y z: V) (Hx: x ≠ 0) (Hy: y ≠ 0) (Hz: z ≠ 0)
    (Hxy: angle x y ≠ 0 ∧ angle x y ≠ Real.pi)
    (Hxz: angle x z ≠ 0 ∧ angle x y ≠ Real.pi)
    (Hyz: angle y z ≠ 0 ∧ angle y z ≠ Real.pi):
    let (e1, e2, e3) := norm_basis _ x y z
    ‖e3‖ = 1 := by
  have H1: inner x x ≠ (0: ℝ) := by simp; assumption
  have H2: inner y y ≠ (0: ℝ) := by simp; assumption
  have H3: inner z z ≠ (0: ℝ) := by simp; assumption
  apply norm_of_unit; intro H5
  sorry

[Ilmārs Cīrulis]

Hmm, it seems I have missed the case when all x, y and z are linearly dependent (when they belong to one plane?). Hypotheses Hxy, Hxz, Hyz are not enough to prove that ‖e3‖ = 1.

Back to work. :sweat_smile:

[Ilmārs Cīrulis]

Replaced Hxy, Hyz, Hxz with Hxyz: ∀ (a b c: ℝ), a • x + b • y + c • z = 0 ↔ (a = 0 ∧ b = 0 ∧ c = 0).

[Ilmārs Cīrulis]

Ok, that was easier than I thought. I just needed to simplify until i got toz = scary_expression * x + scary_expression * y and then use contradiction with hypothesis of linear independence.

[Ilmārs Cīrulis]

:partying_face:

import Mathlib

open InnerProductGeometry


variable (V: Type)
variable [NormedAddCommGroup V]
variable [InnerProductSpace ℝ V]

noncomputable def proj (x y: V): V := (@inner ℝ V _ x y / inner x x) • x
noncomputable def unit (x: V): V := ‖x‖⁻¹ • x
noncomputable def basis (x y z: V) := (x, y - proj _ x y, z - proj _ x z - proj _ (y - proj _ x y) z)
noncomputable def norm_basis (x y z: V) :=
  let (u1, u2, u3) := basis _ x y z
  (unit _ u1, unit _ u2, unit _ u3)

theorem norm_of_unit (x: V) (H: x ≠ 0): ‖unit _ x‖ = 1 := by
  unfold unit; rw [norm_smul]; simp
  have H0: ‖x‖ ≠ 0 := by simp; exact H
  field_simp

theorem all_normed (x y z: V) (Hx: x ≠ 0) (Hy: y ≠ 0) (Hz: z ≠ 0)
    (Hxyz: ∀ (a b c: ℝ), a • x + b • y + c • z = 0 ↔ (a = 0 ∧ b = 0 ∧ c = 0)):
    let (e1, e2, e3) := norm_basis _ x y z
    ‖e1‖ = 1 ∧ ‖e2‖ = 1 ∧ ‖e3‖ = 1 := by
  have H1: inner x x ≠ (0: ℝ) := by simp; assumption
  have H2: inner y y ≠ (0: ℝ) := by simp; assumption
  have H3: inner z z ≠ (0: ℝ) := by simp; assumption
  have H4: y - (inner x y / @inner ℝ V _ x x) • x ≠ 0 := by
    intro H0; rw [sub_eq_zero] at H0
    obtain H4 | H4 := em (inner x y = (0: ℝ))
    . rw [H4] at H0; simp at H0; contradiction
    . have H5: (inner x y / inner x x) ≠ (0: ℝ) := div_ne_zero H4 H1
      have H6 := Hxyz (- (inner x y / inner x x)) 1 0
      simp at H6; nth_rw 2 [H0] at H6; simp at H6
  simp; refine ⟨?_, ?_, ?_⟩
  . apply norm_of_unit _ _ Hx
  . apply norm_of_unit; unfold proj; exact H4
  . apply norm_of_unit; intro H5
    unfold proj at H5
    have H6 (a b c: ℝ): z - a • x - b • (y - c • x) = (- a + b * c) • x + (- b) • y + (1: ℝ) • z := by module
    rw [H6] at H5
    rw [Hxyz] at H5
    simp at H5