OAI/Analysis/NodalLength/NormalizedCharts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Geometry.smoothOn_pullback_metric line 312
  2. lemma OAI.SharpNodal.Geometry.smoothOn_coordinateMetric line 331
  3. lemma OAI.SharpNodal.Geometry.gram_two_positive line 335
  4. lemma OAI.SharpNodal.Geometry.coordinateMetric_symm line 370
  5. lemma OAI.SharpNodal.Geometry.coordinateMetric_positive line 374
  6. def OAI.SharpNodal.Geometry.pullMetric line 384
  7. def OAI.SharpNodal.Geometry.ChartSmooth line 388
  8. lemma OAI.SharpNodal.Geometry.chartSmooth_chartAt line 394
  9. lemma OAI.SharpNodal.Geometry.ChartSmooth.mdiff line 400
  10. lemma OAI.SharpNodal.Geometry.ChartSmooth.metric_smooth line 404
  11. lemma OAI.SharpNodal.Geometry.ChartSmooth.metric_positive line 410
  12. lemma OAI.SharpNodal.Geometry.exists_normalized_chart line 424
  13. lemma OAI.SharpNodal.Geometry.partial_eventuallyEq line 497
  14. lemma OAI.SharpNodal.Geometry.scalarLaplace_congr line 502
  15. lemma OAI.SharpNodal.Geometry.pullMetric_symm line 522
  16. lemma OAI.SharpNodal.Geometry.pullMetric_congr line 527
  17. lemma OAI.SharpNodal.Geometry.pullMetric_transform line 539
  18. lemma OAI.SharpNodal.Geometry.pullMetric_transform_three line 568
  19. lemma OAI.SharpNodal.Geometry.smooth_mul_of_support line 590
  20. lemma OAI.SharpNodal.Geometry.exists_smooth_local_extension line 602