OAI/Geometry/SmoothYau/Spectrum/SmoothExtension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.smooth_extension_at line 26
  2. lemma OAI.YauCounterexamples.positive_smooth_extension_at line 34
  3. lemma OAI.YauCounterexamples.coordinateDivergence_eventuallyEq line 47
  4. lemma OAI.YauCounterexamples.scalarCorrectionDenominator_eventuallyEq line 60
  5. lemma OAI.YauCounterexamples.scalarCorrectionRatio_eventuallyEq line 68
  6. lemma OAI.YauCounterexamples.contDiffOn_coordinateDivergence line 75
  7. lemma OAI.YauCounterexamples.contDiffOn_scalarCorrectionDenominator line 85
  8. lemma OAI.YauCounterexamples.contDiffOn_scalarCorrectionRatio line 95
  9. theorem OAI.YauCounterexamples.frequency_weighted_quotient_uniform_on line 104
  10. theorem OAI.YauCounterexamples.frequency_weighted_product_bound_on line 127
  11. theorem OAI.YauCounterexamples.scalar_denominator_jet_bound_on line 146
  12. theorem OAI.YauCounterexamples.coordinate_divergence_jet_bound_on line 163
  13. theorem OAI.YauCounterexamples.scalar_correction_error_from_quotients_on line 183
  14. theorem OAI.YauCounterexamples.quantitative_scalar_correction_jets_on line 259