OAI/Geometry/SmoothYau/Estimates/RescaledDifferentialPerturbation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.scaledLowerCoefficient line 22
  2. lemma OAI.YauCounterexamples.scaledLowerCoefficient_tendsto line 29
  3. lemma OAI.YauCounterexamples.scaledLowerCoefficient_sobolev_tendsto line 42
  4. def OAI.YauCounterexamples.sobolevCoefficientOperator line 49
  5. lemma OAI.YauCounterexamples.norm_sobolevCoefficientOperator_le line 56
  6. lemma OAI.YauCounterexamples.sobolevCoefficientOperator_tendsto line 73
  7. lemma OAI.YauCounterexamples.sobolevCoefficientOperator_representative line 87
  8. def OAI.YauCounterexamples.sobolevFirstLower line 117
  9. lemma OAI.YauCounterexamples.sobolevFirstLower_representative line 121
  10. def OAI.YauCounterexamples.coefficientPerturbation line 131
  11. lemma OAI.YauCounterexamples.coefficientPerturbation_tendsto line 138
  12. lemma OAI.YauCounterexamples.coefficientPerturbation_representative line 157
  13. def OAI.YauCounterexamples.rescaledDifferentialPerturbation line 214
  14. lemma OAI.YauCounterexamples.rescaledDifferentialPerturbation_tendsto line 222
  15. lemma OAI.YauCounterexamples.rescaledDifferentialPerturbation_representative line 230
  16. theorem OAI.YauCounterexamples.exists_rescaled_local_inverse line 246