OAI/Analysis/NodalLength/MetricFlux.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Geometry.partial_add_at line 304
  2. lemma OAI.SharpNodal.Geometry.partial_sub_at line 309
  3. lemma OAI.SharpNodal.Geometry.partial_mul_at line 314
  4. lemma OAI.SharpNodal.Geometry.smoothAt_partial line 319
  5. lemma OAI.SharpNodal.Geometry.partial_partial_at line 322
  6. lemma OAI.SharpNodal.Geometry.partial_congr_nhds line 333
  7. lemma OAI.SharpNodal.Geometry.differentiableAt_coordMap line 336
  8. lemma OAI.SharpNodal.Geometry.contDiffAt_coordMap line 339
  9. lemma OAI.SharpNodal.Geometry.partial_comp_coordMap line 342
  10. lemma OAI.SharpNodal.Geometry.piola_identity line 354
  11. lemma OAI.SharpNodal.Geometry.conjugate_matrix_conformal line 379
  12. lemma OAI.SharpNodal.Geometry.density_flux_two line 398
  13. lemma OAI.SharpNodal.Geometry.transform_metric_det line 411
  14. lemma OAI.SharpNodal.Geometry.transform_metric_density line 415
  15. lemma OAI.SharpNodal.Geometry.transform_metric_cofactor line 420
  16. lemma OAI.SharpNodal.Geometry.determinant_sign_sq line 428
  17. lemma OAI.SharpNodal.Geometry.transform_metric_flux line 434
  18. def OAI.SharpNodal.Geometry.scalarDensity line 450
  19. def OAI.SharpNodal.Geometry.scalarFlux0 line 452
  20. def OAI.SharpNodal.Geometry.scalarFlux1 line 454
  21. def OAI.SharpNodal.Geometry.scalarLaplace line 456
  22. def OAI.SharpNodal.Geometry.transformA line 460
  23. def OAI.SharpNodal.Geometry.transformB line 464
  24. def OAI.SharpNodal.Geometry.transformC line 468
  25. def OAI.SharpNodal.Geometry.coordDet line 472
  26. lemma OAI.SharpNodal.Geometry.smoothAt_scalarDensity line 475
  27. lemma OAI.SharpNodal.Geometry.smoothAt_scalarFlux line 479
  28. lemma OAI.SharpNodal.Geometry.transform_scalarDensity line 488
  29. lemma OAI.SharpNodal.Geometry.transform_scalarFlux line 494
  30. lemma OAI.SharpNodal.Geometry.continuousAt_abs_sign line 514
  31. lemma OAI.SharpNodal.Geometry.scalarLaplace_covariant line 524