OAI/Geometry/SmoothYau/Estimates/CoefficientPerturbationTendsto.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingLaplacian_mem_realH line 30
2. def OAI.YauCounterexamples.CompactMetricAtlas.varyingRealLaplacian line 40
3. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingRealLaplacian_value line 45
4. def OAI.YauCounterexamples.CompactMetricAtlas.varyingShift line 53
5. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingShift_value line 58
6. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingRealLaplacian_independent line 67
7. lemma OAI.YauCounterexamples.coefficientPerturbation_tendsto_at line 97
8. theorem OAI.YauCounterexamples.CompactMetricAtlas.varyingLaplacianCLM_tendsto line 130
9. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingRealLaplacian_norm_sub_le line 158
10. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingRealLaplacian_tendsto line 167
11. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingShift_tendsto line 180