OAI/Geometry/SmoothYau/SphereMetric/ThreeCutoffControlBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.threeNormalInv_isOpenMap line 12
  2. lemma OAI.YauCounterexamples.threeNormalInv_closedBall_closed line 18
  3. lemma OAI.YauCounterexamples.threeNormalInv_mem_closedBall_iff line 20
  4. lemma OAI.YauCounterexamples.threeNormalInv_mem_ball_iff line 23
  5. lemma OAI.YauCounterexamples.exists_three_radial_cutoff line 26
  6. lemma OAI.YauCounterexamples.three_wave_exterior_germ line 37
  7. lemma OAI.YauCounterexamples.three_wave_residual_support line 44
  8. lemma OAI.YauCounterexamples.three_clean_conjugating_margin line 69
  9. lemma OAI.YauCounterexamples.three_coordinateGradientPair_pos_derivative_ne line 94
  10. lemma OAI.YauCounterexamples.three_regular_quotient_at_zero line 100
  11. def OAI.YauCounterexamples.ThreeAnnulus line 127
  12. lemma OAI.YauCounterexamples.threeAnnulus_closed line 129
  13. lemma OAI.YauCounterexamples.threeAnnulus_not_inner line 131
  14. lemma OAI.YauCounterexamples.threeAnnulus_clean line 136
  15. theorem OAI.YauCounterexamples.three_annular_projection_uniform line 141
  16. lemma OAI.YauCounterexamples.three_cutoff_control_bounds line 209
  17. lemma OAI.YauCounterexamples.three_cutoff_raw_bounded_by_near_one line 248
  18. theorem OAI.YauCounterexamples.exists_three_exact_stage line 269