OAI/Geometry/SmoothYau/Limits/CutoffFactorCompactRaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.inverse_gram_differential_norm line 39
2. lemma OAI.YauCounterexamples.round_centered_gradient_norm line 58
3. def OAI.YauCounterexamples.chartInverseDifferentialBound line 73
4. lemma OAI.YauCounterexamples.chart_inverse_differential_bound line 77
5. lemma OAI.YauCounterexamples.chartInverseDifferentialBound_continuous line 101
6. theorem OAI.YauCounterexamples.compact_chart_intrinsic_gradient_bound line 109
7. theorem OAI.YauCounterexamples.cutoffFactor_compact_raw line 152
8. def OAI.YauCounterexamples.CompactMetricAtlas.coveringRawTest line 177
9. def OAI.YauCounterexamples.CompactMetricAtlas.coveringRawTests line 186
10. lemma OAI.YauCounterexamples.CompactMetricAtlas.coveringRawTest_mem line 190
11. lemma OAI.YauCounterexamples.CompactMetricAtlas.coveringRawTests_cover line 196
12. theorem OAI.YauCounterexamples.CompactMetricAtlas.global_cutoff_raw_controls line 212