OAI/Geometry/SmoothYau/Smoothness/SourceSignBox.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.sourceSignBox line 25
  2. lemma OAI.YauCounterexamples.sourceSignBox_band line 27
  3. def OAI.YauCounterexamples.sourceSignRegion line 35
  4. lemma OAI.YauCounterexamples.sourceSignRegion_band line 38
  5. def OAI.YauCounterexamples.sourceProfileCoverage line 44
  6. lemma OAI.YauCounterexamples.sourceProfileCoverage_compact line 47
  7. lemma OAI.YauCounterexamples.sourceSignBox_subset_coverage line 51
  8. def OAI.YauCounterexamples.sphericalProfileMetricNeighborhood line 59
  9. lemma OAI.YauCounterexamples.sphericalProfileMetricNeighborhood_isNeighborhood line 66
  10. lemma OAI.YauCounterexamples.coordinateMetricGradient_ne_zero_of_fderiv line 71
  11. lemma OAI.YauCounterexamples.source_baseProfile_sign_gradient line 82
  12. theorem OAI.YauCounterexamples.exists_global_spherical_wave_profile line 102