OAI/Analysis/NodalLength/Conductivity.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Geometry.coordMap_components line 315
  2. lemma OAI.SharpNodal.Geometry.smoothAt_component line 321
  3. lemma OAI.SharpNodal.Geometry.smoothOn_component line 325
  4. lemma OAI.SharpNodal.Geometry.coordPartial_component line 329
  5. lemma OAI.SharpNodal.Geometry.inverse_coordinate_equations line 336
  6. lemma OAI.SharpNodal.Geometry.coordDet_chart_ne_zero line 365
  7. lemma OAI.SharpNodal.Geometry.ChartSmooth.trans line 399
  8. lemma OAI.SharpNodal.Geometry.inverse_jacobian_entries line 409
  9. lemma OAI.SharpNodal.Geometry.conjugate_inverse_metric_numerators line 425
  10. lemma OAI.SharpNodal.Geometry.conformal_inverse_metric line 442
  11. lemma OAI.SharpNodal.Geometry.conjugate_chart_conformal line 479
  12. def OAI.SharpNodal.Geometry.chartConductivity line 547
  13. lemma OAI.SharpNodal.Geometry.ChartSmooth.conductivity_smooth line 552
  14. lemma OAI.SharpNodal.Geometry.conductivity_normalized line 575
  15. lemma OAI.SharpNodal.Geometry.pullMetric_smul line 584
  16. def OAI.SharpNodal.Geometry.scaleChart line 606
  17. lemma OAI.SharpNodal.Geometry.ChartSmooth.scale line 612
  18. lemma OAI.SharpNodal.Geometry.scaleChart_metric line 621
  19. lemma OAI.SharpNodal.Geometry.sqrt_det_smul_sq line 627
  20. lemma OAI.SharpNodal.Geometry.scaleChart_conductivity line 635