AffineCopyCore.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GrahamSpherical.inner_sub_self line 12
Source documentation
Polarization in the actual real Euclidean inner product.
```
lemma inner_sub_self (n : ℕ) (x y : Point n) :
    (inner ℝ (x-y) (x-y)) = (inner ℝ (x) (x)) - 2*(inner ℝ (x) (y)) + (inner ℝ (y) (y)) := by
…
```
Mentions: OAI.GrahamSpherical.Point

lemma OAI.GrahamSpherical.vector_eq_of_orthonormal_coordinates line 19

Source documentation

An orthonormal pair reconstructs a vector once its two coordinates account for its full squared norm. No dimension assumption is imposed on the codomain.

lemma vector_eq_of_orthonormal_coordinates {n : ℕ} (A B z : Point n) (a b : ℝ)
    (hAA : (inner ℝ (A) (A)) = 1) (hBB : (inner ℝ (B) (B)) = 1) (hAB : (inner ℝ (A) (B)) = 0)
    (hzA : (inner ℝ (z) (A)) = a) (hzB : (inner ℝ (z) (B)) = b)
    (hzz : (inner ℝ (z) (z)) = a^2+b^2) : z = a • A + b • B := by
…

Mentions: OAI.GrahamSpherical.Point

lemma OAI.GrahamSpherical.affine_frame_of_anchor_gram line 34

Source documentation

The three-anchor Gram data determine a common affine Euclidean frame.

lemma affine_frame_of_anchor_gram {ι : Type*} {n : ℕ}
    (y : ι → Point n) (a b : ι → ℝ) (p : Point n) (d e : Point n)
    (hdd : (inner ℝ (d) (d)) = 4) (hee : (inner ℝ (e) (e)) = 2) (hde : (inner ℝ (d) (e)) = 2)
    (hzz : ∀ i, (inner ℝ (y i-p) (y i-p)) = (a i-1)^2+(b i)^2)
    (hzd : ∀ i, (inner ℝ (y i-p) (d)) = 2*(1-a i))
    (hze : ∀ i, (inner ℝ (y i-p) (e)) = 1-a i+b i) :
    ∃ c A B : Point n, (inner ℝ (A) (A)) = 1 ∧ (inner ℝ (B) (B)) = 1 ∧
      (inner ℝ (A) (B)) = 0 ∧ ∀ i, y i = c + a i • A + b i • B := by
…

Mentions: OAI.GrahamSpherical.Point