CircleRows.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.EuclideanRamsey.CircleConsequence.QIndex line 8
def OAI.EuclideanRamsey.CircleConsequence.quadraticRow line 9
theorem OAI.EuclideanRamsey.CircleConsequence.normalized_isolators line 13
Source documentation
Normalized coefficients for quadratic interpolation at five circle points.
```
theorem normalized_isolators (a : Fin 5 → Space 2) (ha : Function.Injective a)
    (c : Space 2) (r : ℝ) (hc : ∀ i, dist (a i) c = r) :
    ∃ L : Fin 5 → QIndex → Coeff a,
      ∀ i j, ∑ q, L i q * quadraticRow a j q = if j = i then 1 else 0 := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.CircleConsequence.QIndex, OAI.EuclideanRamsey.Coeff, OAI.EuclideanRamsey.CircleConsequence.quadraticRow
theorem OAI.EuclideanRamsey.CircleConsequence.quadratic_evaluation_surjective line 37
Source documentation
A concrete right inverse to quadratic evaluation.
```
theorem quadratic_evaluation_surjective (a : Fin 5 → Space 2)
    (ha : Function.Injective a) (c : Space 2) (r : ℝ)
    (hc : ∀ i, dist (a i) c = r) :
    ∀ values : Fin 5 → Coeff a, ∃ coeff : QIndex → Coeff a,
      ∀ j, ∑ q, coeff q * quadraticRow a j q = values j := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.Coeff, OAI.EuclideanRamsey.CircleConsequence.QIndex, OAI.EuclideanRamsey.CircleConsequence.quadraticRow
theorem OAI.EuclideanRamsey.CircleConsequence.circle_five_rows_independent line 53
Source documentation
The quadratic evaluation rows are independent because their dual rows isolate them.
```
theorem circle_five_rows_independent (a : Fin 5 → Space 2)
    (ha : Function.Injective a) (c : Space 2) (r : ℝ)
    (hc : ∀ i, dist (a i) c = r) :
    LinearIndependent (Coeff a) (fun i : Fin 5 => fun q : QIndex =>
      augmented a i q.1 * augmented a i q.2) := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.Coeff, OAI.EuclideanRamsey.CircleConsequence.QIndex, OAI.EuclideanRamsey.augmented