OAI/Geometry/SmoothYau/Smoothness/CutoffExactificationSmoothNeighborhood.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.chartGradientField_sub_const line 42
2. theorem OAI.YauCounterexamples.weightedLaplacian_small_jets_on_compact line 47
3. lemma OAI.YauCounterexamples.constant_product_jet_bound_on line 148
4. lemma OAI.YauCounterexamples.raw_jets_of_near_one line 165
5. theorem OAI.YauCounterexamples.cutoff_density_small_jets line 188
6. lemma OAI.YauCounterexamples.list_positive_common_lower_bound line 332
7. theorem OAI.YauCounterexamples.cutoff_density_small_jets_finite line 348
8. theorem OAI.YauCounterexamples.cutoff_exactification_in_smooth_neighborhood line 421