OAI/Geometry/SmoothYau/SphereMetric/ThreeExceptional.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.threePacketA line 16
  2. def OAI.YauCounterexamples.threePacketB line 18
  3. def OAI.YauCounterexamples.threePacketWeight line 20
  4. def OAI.YauCounterexamples.threeExceptionalInChart line 22
  5. lemma OAI.YauCounterexamples.threePacketA_smooth line 25
  6. lemma OAI.YauCounterexamples.threePacketB_smooth line 27
  7. lemma OAI.YauCounterexamples.threePacketA_norm line 29
  8. lemma OAI.YauCounterexamples.threePacketB_norm line 33
  9. lemma OAI.YauCounterexamples.threePacketWeight_lower line 38
  10. lemma OAI.YauCounterexamples.threePacketWeight_upper line 42
  11. lemma OAI.YauCounterexamples.threePacket_radius_bound line 49
  12. lemma OAI.YauCounterexamples.threePacket_back_eq line 60
  13. lemma OAI.YauCounterexamples.threePacket_background_input_bounds line 65
  14. lemma OAI.YauCounterexamples.threeCoupled_abs_le_radius line 80
  15. lemma OAI.YauCounterexamples.three_background_sign_small line 98
  16. lemma OAI.YauCounterexamples.three_exceptional_eventually_coverage line 123
  17. lemma OAI.YauCounterexamples.threeNormalInv_injective line 164
  18. theorem OAI.YauCounterexamples.exists_three_chart_quasimodes line 172
  19. theorem OAI.YauCounterexamples.exists_three_chart_quasimodes_with_gaps line 262
  20. def OAI.YauCounterexamples.threeExceptional line 351
  21. lemma OAI.YauCounterexamples.three_global_radius_weight_bound line 353
  22. lemma OAI.YauCounterexamples.threeWeight_le_packet line 366
  23. lemma OAI.YauCounterexamples.three_packet_productWeight line 370
  24. lemma OAI.YauCounterexamples.three_exceptional_chart_iff line 373
  25. lemma OAI.YauCounterexamples.three_exceptional_global_coverage line 377
  26. lemma OAI.YauCounterexamples.three_core_exceptional line 409