OAI/Geometry/SmoothYau/Smoothness/LocalIntegrationParts.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.contDiffAt_chartTransition line 44
  2. lemma OAI.YauCounterexamples.contDiffAt_inChart line 52
  3. lemma OAI.YauCounterexamples.chart_overlap_nhds line 59
  4. lemma OAI.YauCounterexamples.fderiv_inChart_change line 68
  5. def OAI.YauCounterexamples.metricFlux line 89
  6. def OAI.YauCounterexamples.localLaplacian line 94
  7. lemma OAI.YauCounterexamples.metricInverse_change_left line 98
  8. lemma OAI.YauCounterexamples.metricFlux_change line 108
  9. def OAI.YauCounterexamples.metricFirstCoefficient line 169
  10. lemma OAI.YauCounterexamples.contDiffAt_metricFirstCoefficient line 174
  11. lemma OAI.YauCounterexamples.localLaplacian_expansion line 186
  12. def OAI.YauCounterexamples.roundPlanarChart line 281
  13. lemma OAI.YauCounterexamples.roundPlanarChart_smooth line 284
  14. lemma OAI.YauCounterexamples.sphere_wave_weight_C1 line 293
  15. theorem OAI.YauCounterexamples.sphere_wave_weight_control line 306
  16. theorem OAI.YauCounterexamples.exists_smooth_metric_coefficients_at line 343
  17. theorem OAI.YauCounterexamples.exists_smooth_metric_coefficients_on_compact line 381
  18. lemma OAI.YauCounterexamples.local_integration_by_parts line 420
  19. def OAI.YauCounterexamples.realChartLocalize line 456
  20. lemma OAI.YauCounterexamples.realChartLocalize_eq line 461
  21. lemma OAI.YauCounterexamples.support_realChartLocalize line 465
  22. lemma OAI.YauCounterexamples.isCompact_realChartSupport line 477
  23. lemma OAI.YauCounterexamples.tsupport_realChartLocalize line 483
  24. lemma OAI.YauCounterexamples.hasCompactSupport_realChartLocalize line 489
  25. lemma OAI.YauCounterexamples.tsupport_realChartLocalize_subset line 496
  26. lemma OAI.YauCounterexamples.contDiff_realChartLocalize line 503
  27. lemma OAI.YauCounterexamples.realChartLocalize_fderiv line 518