OAI/Analysis/HyperbolicCones/DeformationFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper256.intervalPolynomial_expanded line 11
2. theorem OAI.Paper256.quadratic_expansion line 16
3. theorem OAI.Paper256.normalized_quadratic_representation line 24
4. theorem OAI.Paper256.intervalPolynomial_natDegree_le line 49
5. theorem OAI.Paper256.intervalPolynomial_coeff_two line 58
6. theorem OAI.Paper256.intervalPolynomial_natDegree line 64
7. theorem OAI.Paper256.deformedPolynomial_natDegree line 70
8. theorem OAI.Paper256.normalized_negative_quadratics_open line 78

   Source documentation

   In coefficient coordinates on normalized quadratics, negative leading coefficient is open.

   theorem normalized_negative_quadratics_open :
       IsOpen {v : Fin 2 → ℝ | v 1 < 0} := by
   …

9. theorem OAI.Paper256.normalized_negative_quadratics_representation line 83

   Source documentation

   Every point of that open coefficient family is exactly one of the displayed quadratics.

   theorem normalized_negative_quadratics_representation (v : Fin 2 → ℝ) (hv : v 1 < 0) :
       ∃ a b : ℝ, 0 < a ∧ 0 < b ∧
         1 + C (v 0) * X + C (v 1) * X ^ 2 = intervalPolynomial a b := by
   …

   Mentions: OAI.Paper256.intervalPolynomial