OAI/Combinatorics/SphericalRamsey/AffineCopy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GrahamSpherical.dist_vertex_sq line 9
2. lemma OAI.GrahamSpherical.inner_sub_self_eq_dist_sq line 15
3. theorem OAI.GrahamSpherical.affine_copy line 22

   Source documentation

   Every literal distance-preserving placement of the twelve points has one common affine expression with an orthonormal pair. No affine hypothesis or ambient-dimension lower bound is assumed.

   theorem affine_copy {n : ℕ} (y : Label → Point n)
       (hy : ∀ i j, dist (y i) (y j) = dist (vertex i) (vertex j)) :
       ∃ c A B : Point n, (inner ℝ (A) (A)) = 1 ∧ (inner ℝ (B) (B)) = 1 ∧
         (inner ℝ (A) (B)) = 0 ∧ ∀ i, y i = c + coordinates i 0 • A + coordinates i 1 • B := by
   …

   Mentions: OAI.GrahamSpherical.Label, OAI.GrahamSpherical.Point, OAI.GrahamSpherical.vertex, OAI.GrahamSpherical.coordinates

4. lemma OAI.GrahamSpherical.sum_sq_eq_inner line 73

   Source documentation

   Coordinate-square normalization for the derivative-energy calculation.

   lemma sum_sq_eq_inner {n : ℕ} (A : Point n) :
       (∑ j : Fin n, A j ^ 2) = (inner ℝ (A) (A)) := by
   …

   Mentions: OAI.GrahamSpherical.Point