OAI/Combinatorics/EuclideanRamsey/CircleInterpolation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EuclideanRamsey.CircleConsequence.secantRow line 9
2. def OAI.EuclideanRamsey.CircleConsequence.secantValue line 15
3. theorem OAI.EuclideanRamsey.CircleConsequence.secantRow_eval line 19
4. def OAI.EuclideanRamsey.CircleConsequence.pairedSecantMatrix line 25
5. theorem OAI.EuclideanRamsey.CircleConsequence.pairedSecantMatrix_eval line 29
6. theorem OAI.EuclideanRamsey.CircleConsequence.pairedSecantMatrix_vanishes line 43
7. theorem OAI.EuclideanRamsey.CircleConsequence.secantValue_ne_zero line 51

   Source documentation

   Nonzero evaluation follows from actual planar circle equations.

   theorem secantValue_ne_zero {s : ℕ} (a : Fin s → Space 2)
       (ha : Function.Injective a) (c : Space 2) (R : ℝ)
       (hc : ∀ m, (a m 0-c 0)^2 + (a m 1-c 1)^2 = R)
       (i j k : Fin s) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) :
       secantValue a i j k ≠ 0 := by
   …

   Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.CircleConsequence.secantValue

8. theorem OAI.EuclideanRamsey.CircleConsequence.five_point_isolator line 74

   Source documentation

   The five-point isolator is a concrete coordinate-field matrix. The permutation is just a labeling, with e 0 the point being isolated.

   theorem five_point_isolator (a : Fin 5 → Space 2)
       (ha : Function.Injective a) (c : Space 2) (R : ℝ)
       (hc : ∀ m, (a m 0-c 0)^2 + (a m 1-c 1)^2 = R)
       (e : Equiv.Perm (Fin 5)) :
       ∃ M : Matrix (Option (Fin 2)) (Option (Fin 2)) (Coeff a),
         (∀ m, m ≠ e 0 →
           (∑ α : Option (Fin 2), ∑ β : Option (Fin 2),
             M α β * augmented a m α * augmented a m β) = 0) ∧
         (∑ α : Option (Fin 2), ∑ β : Option (Fin 2),
             M α β * augmented a (e 0) α * augmented a (e 0) β) ≠ 0 := by
   …

   Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.Coeff, OAI.EuclideanRamsey.augmented