OAI/Geometry/SmoothYau/Estimates/AnisotropicCompositionSmall.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.neumannCorrectedInverse line 26
2. lemma OAI.YauCounterexamples.neumannCorrectedInverse_fixed line 32
3. lemma OAI.YauCounterexamples.neumannCorrectedInverse_bound line 43
4. lemma OAI.YauCounterexamples.neumannCorrectedInverse_lower_bound line 57
5. lemma OAI.YauCounterexamples.rescaledCoefficient_sobolev_tendsto line 81
6. lemma OAI.YauCounterexamples.rescaledCoefficient_sobolev_small line 88
7. lemma OAI.YauCounterexamples.anisotropic_composition_small line 110
8. def OAI.YauCounterexamples.localEllipticInverse line 119
9. lemma OAI.YauCounterexamples.localEllipticInverse_equation line 126
10. lemma OAI.YauCounterexamples.norm_localEllipticInverse_le line 141
11. lemma OAI.YauCounterexamples.localEllipticInverse_half_bound line 151
12. lemma OAI.YauCounterexamples.eventually_localEllipticInverse_small line 164