OAI/Geometry/SmoothYau/Smoothness/ChartGradientProjectionSmooth.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.chartGradientField line 28
  2. lemma OAI.YauCounterexamples.chartGradientField_smooth line 33
  3. lemma OAI.YauCounterexamples.coordinateDivergence_chartGradient line 46
  4. lemma OAI.YauCounterexamples.scalarCorrectionDenominator_inChart line 51
  5. lemma OAI.YauCounterexamples.scalarCorrectionRatio_inChart line 62
  6. lemma OAI.YauCounterexamples.weightedLaplacian_chartGradient line 74
  7. lemma OAI.YauCounterexamples.scalarCorrectionB_inChart line 99
  8. lemma OAI.YauCounterexamples.scalarCorrectionS_inChart line 110
  9. lemma OAI.YauCounterexamples.coordinateGradientPair_nonneg line 133
  10. lemma OAI.YauCounterexamples.intrinsicCorrectionD_lower line 147
  11. lemma OAI.YauCounterexamples.intrinsicCorrectionD_pos line 153
  12. lemma OAI.YauCounterexamples.compact_derivative_bound_on line 160
  13. lemma OAI.YauCounterexamples.geometric_product_jet_bound_on line 171
  14. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_scalar_direction_on line 186
  15. lemma OAI.YauCounterexamples.chartGradientField_jet_bound line 196
  16. lemma OAI.YauCounterexamples.compact_metric_scalar_coefficient_bounds line 248
  17. theorem OAI.YauCounterexamples.quantitative_intrinsic_correction_on_compact_chart line 283
  18. def OAI.YauCounterexamples.CompactMetricAtlas.scalarChartSupport line 401
  19. lemma OAI.YauCounterexamples.CompactMetricAtlas.scalarChartSupport_compact line 405
  20. lemma OAI.YauCounterexamples.CompactMetricAtlas.scalarChartSupport_target line 409
  21. theorem OAI.YauCounterexamples.CompactMetricAtlas.quantitative_intrinsic_correction_jets line 414
  22. lemma OAI.YauCounterexamples.weighted_quotient_jet_bound_on line 536
  23. theorem OAI.YauCounterexamples.rankOne_projection_jet_bound_on line 557
  24. def OAI.YauCounterexamples.chartGradientProjection line 606
  25. lemma OAI.YauCounterexamples.chartGradientField_sharp_jet_bound line 612
  26. theorem OAI.YauCounterexamples.chartGradientProjection_jet_bound line 630
  27. lemma OAI.YauCounterexamples.sharp_conjugate_jet_bound_on line 714
  28. lemma OAI.YauCounterexamples.chartGradientProjection_smooth_on line 784