OAI/Geometry/SmoothYau/NodalMeasure/CompactRegularLevelIntrinsicFinite.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.YauCounterexamples.exists_supported_nodal_quasimodes line 18
  2. theorem OAI.YauCounterexamples.exists_supported_box_nodal_quasimodes line 114
  3. def OAI.YauCounterexamples.normalCoordinateVolume line 213
  4. instance OAI.YauCounterexamples.normalCoordinateVolume_finiteOnCompacts line 215
  5. lemma OAI.YauCounterexamples.box_Ioo_closure line 229
  6. lemma OAI.YauCounterexamples.normal_box_closure line 238
  7. lemma OAI.YauCounterexamples.normal_box_open line 244
  8. lemma OAI.YauCounterexamples.normal_box_measure_ne_zero line 247
  9. lemma OAI.YauCounterexamples.profileSpeed_le_frequencyScale line 258
  10. lemma OAI.YauCounterexamples.actual_profile_mass_le_box_frequency_integral line 266
  11. theorem OAI.YauCounterexamples.exists_box_amplified_profile line 283
  12. theorem OAI.YauCounterexamples.regular_level_local_finite line 317
  13. lemma OAI.YauCounterexamples.compact_coordinate_regular_level_finite line 384
  14. lemma OAI.YauCounterexamples.realWaveJet_pos_regular line 401
  15. lemma OAI.YauCounterexamples.noncancelling_coordinate_nodal_finite line 410
  16. theorem OAI.YauCounterexamples.exists_arbitrarily_large_nodal_quasimodes line 428
  17. theorem OAI.YauCounterexamples.compact_regular_level_intrinsic_finite line 533