OAI/Geometry/SmoothYau/Spectrum/ProfileFrequencyEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.profileFrequencyEnergy line 11
2. def OAI.YauCounterexamples.profileFrequencyScale line 15
3. lemma OAI.YauCounterexamples.profileFrequencyEnergy_ge_one line 19
4. lemma OAI.YauCounterexamples.profileFrequencyScale_sq line 27
5. lemma OAI.YauCounterexamples.profileFrequencyScale_ge_one line 32
6. lemma OAI.YauCounterexamples.continuous_profileFrequencyEnergy line 41
7. lemma OAI.YauCounterexamples.profileFrequencyEnergy_frame line 53
8. lemma OAI.YauCounterexamples.nearby_characteristic_energy line 60
9. theorem OAI.YauCounterexamples.compact_normal_profile_angular_energy line 114