OAI/Geometry/Arnold/MidpointGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ArnoldCounterexample.Field.normSquared_add line 15
  2. lemma OAI.ArnoldCounterexample.Field.real_smul_complex line 27
  3. lemma OAI.ArnoldCounterexample.Field.normSquared_real_smul line 30
  4. lemma OAI.ArnoldCounterexample.Field.quadricPolynomial_real_smul line 34
  5. lemma OAI.ArnoldCounterexample.Field.quadratic_skew line 38
  6. lemma OAI.ArnoldCounterexample.Field.normSquared_le_maxNorm line 47
  7. lemma OAI.ArnoldCounterexample.Field.norm_le_one_of_normSquared line 56
  8. lemma OAI.ArnoldCounterexample.Field.center_quadratic line 62
  9. lemma OAI.ArnoldCounterexample.Field.midpoint_preserves line 73
  10. lemma OAI.ArnoldCounterexample.Field.center_norm_le_one line 88
  11. lemma OAI.ArnoldCounterexample.Field.center_norm_gt_half line 95