OAI/Geometry/SmoothYau/Smoothness/NormIteratedFDerivScalarDirection.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.coordinateDivergence line 24
  2. theorem OAI.YauCounterexamples.coordinateDivergence_mul line 27
  3. theorem OAI.YauCounterexamples.coordinateDivergence_sub line 48
  4. theorem OAI.YauCounterexamples.coordinate_scalar_correction line 57
  5. theorem OAI.YauCounterexamples.contDiff_coordinateDivergence line 85
  6. def OAI.YauCounterexamples.scalarCorrectionDenominator line 93
  7. def OAI.YauCounterexamples.scalarCorrectionRatio line 97
  8. def OAI.YauCounterexamples.scalarCorrectionB line 101
  9. def OAI.YauCounterexamples.scalarCorrectionS line 105
  10. theorem OAI.YauCounterexamples.contDiff_scalarCorrectionDenominator line 110
  11. theorem OAI.YauCounterexamples.contDiff_scalarCorrectionRatio line 118
  12. theorem OAI.YauCounterexamples.scalar_correction line 127
  13. def OAI.YauCounterexamples.coordinateFlux line 148
  14. theorem OAI.YauCounterexamples.fderiv_quotient_apply line 152
  15. theorem OAI.YauCounterexamples.coordinateFlux_quotient line 166
  16. theorem OAI.YauCounterexamples.coordinateFlux_pair_comm line 177
  17. theorem OAI.YauCounterexamples.contDiff_coordinateFlux line 190
  18. theorem OAI.YauCounterexamples.coordinate_conjugation_flux line 197
  19. def OAI.YauCounterexamples.conjugatedDensity line 229
  20. theorem OAI.YauCounterexamples.coordinate_conjugated_equation line 233
  21. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_scalar_direction line 271
  22. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_scalar_sum line 280
  23. theorem OAI.YauCounterexamples.scalar_denominator_jet_bound line 288
  24. lemma OAI.YauCounterexamples.constant_product_jet_bound line 357
  25. theorem OAI.YauCounterexamples.coordinate_divergence_jet_bound line 373
  26. theorem OAI.YauCounterexamples.scalar_denominator_lower line 408
  27. theorem OAI.YauCounterexamples.scalar_correction_error_from_quotients line 429
  28. theorem OAI.YauCounterexamples.quantitative_scalar_correction_jets line 504