OAI/Geometry/SmoothYau/ProductMetric/ThreeInteriorMeridianNormedSpace.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.threeInteriorMeridianAmbient line 15
  2. lemma OAI.YauCounterexamples.threeInteriorMeridianAmbient_norm line 16
  3. def OAI.YauCounterexamples.threeInteriorMeridian line 23
  4. lemma OAI.YauCounterexamples.threeInteriorMeridian_smooth line 25
  5. lemma OAI.YauCounterexamples.threeInteriorMeridian_A line 32
  6. lemma OAI.YauCounterexamples.threeInteriorMeridian_B line 34
  7. lemma OAI.YauCounterexamples.threeInteriorMeridian_circle line 36
  8. lemma OAI.YauCounterexamples.interior_complex_I_pow_four_add_one line 37
  9. lemma OAI.YauCounterexamples.interior_complex_I_pow_four line 40
  10. lemma OAI.YauCounterexamples.interior_complex_neg_one_pow_four_add_one line 41
  11. lemma OAI.YauCounterexamples.threeInteriorMeridian_complex line 44
  12. lemma OAI.YauCounterexamples.threeInteriorMeridian_zero line 51
  13. lemma OAI.YauCounterexamples.threeInteriorMeridian_gradient_value line 54
  14. def OAI.YauCounterexamples.threeInteriorMeridianEnergy line 66
  15. lemma OAI.YauCounterexamples.threeInteriorMeridianEnergy_smooth line 69
  16. lemma OAI.YauCounterexamples.threeInteriorMeridianEnergy_zero line 72
  17. lemma OAI.YauCounterexamples.threeInteriorMeridianEnergy_right line 77
  18. lemma OAI.YauCounterexamples.exists_threeInteriorMeridianEnergy_deriv line 82
  19. lemma OAI.YauCounterexamples.threeInteriorMeridian_circle_deriv_ne line 97
  20. lemma OAI.YauCounterexamples.exists_threeCoupled_interior_gradient_rank line 108