OAI/Geometry/Riemannian/HarmonicCore/MetricLaplacian.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inverse_derivative line 17
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coeff_symmetric line 51
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coeff_symm line 54
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inverse_symmetric line 57
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_coord_hasDerivAt line 61
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.determinant_coordDeriv line 69
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.density_coordDeriv line 88
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inverse_coordDeriv line 105
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordDeriv_mul line 113
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.divergence_inverse_algebra line 121
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyMatrix_contDiff line 130
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyMatrix_divergence line 135
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordDeriv_contDiff line 151
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordDeriv_sum line 156
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coordDeriv_twice line 163
  16. def OAI.HarmonicCounterexample.Main.SmoothMetric3.metricFlux line 173
  17. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.metricFlux_contDiff line 176
  18. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_divergence line 180
  19. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_green line 204
  20. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.density_laplacian_contDiff line 231
  21. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_eq_zero_of_weak_energy line 241