OAI/Geometry/NodalSets/Elliptic/BasisLaplacian.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Geometry.basisMetricMatrix line 15
  2. def OAI.Yau.Geometry.basisMetricFlux line 18
  3. def OAI.Yau.Geometry.basisMetricLaplacian line 23
  4. lemma OAI.Yau.Geometry.basis_change_det_ne_zero line 28
  5. lemma OAI.Yau.Geometry.basis_change_inverse line 33
  6. lemma OAI.Yau.Geometry.basisMetricMatrix_change line 36
  7. lemma OAI.Yau.Geometry.basisMetricMatrix_volume_change line 40
  8. lemma OAI.Yau.Geometry.basis_derivative_vector line 49
  9. lemma OAI.Yau.Geometry.basis_inverse_derivative_vector line 55
  10. lemma OAI.Yau.Geometry.basisMetricFlux_change line 67
  11. lemma OAI.Yau.Geometry.basisMetricLaplacian_change line 81