OAI/Geometry/SmoothYau/Spectrum/InverseFrequencyWeightedZero.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.inverseFrequency_weighted_zero line 12
2. lemma OAI.YauCounterexamples.spherical_exterior_conjugating_margin line 28
3. lemma OAI.YauCounterexamples.spherical_cutoff_control_bounds line 59
4. lemma OAI.YauCounterexamples.cutoff_raw_bounded_by_near_one line 102
5. theorem OAI.YauCounterexamples.exists_spherical_exact_stage line 123