OAI/Geometry/SmoothYau/NodalMeasure/SphericalNodalFinite.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.map_edist_le_pathELength line 25
  2. theorem OAI.YauCounterexamples.map_edist_le_riemannianEDist line 64
  3. lemma OAI.YauCounterexamples.eventually_norm_mfderiv_lt line 78
  4. lemma OAI.YauCounterexamples.exists_global_mfderiv_bound line 110
  5. theorem OAI.YauCounterexamples.compact_map_riemannian_lipschitz line 132
  6. lemma OAI.YauCounterexamples.exists_smooth_chart_extension line 148
  7. theorem OAI.YauCounterexamples.compact_chart_riemannian_lipschitz line 172
  8. theorem OAI.YauCounterexamples.compact_chart_hausdorff_comparison line 182
  9. theorem OAI.YauCounterexamples.nodalMeasure_chart_lower_bound line 213
  10. theorem OAI.YauCounterexamples.nodalMeasure_coordinates_lower_bound line 233
  11. lemma OAI.YauCounterexamples.spherical_nodal_finite line 270
  12. lemma OAI.YauCounterexamples.spherical_signCertificate_bound line 284
  13. lemma OAI.YauCounterexamples.spherical_sign_nodal_real line 336