OAI/Geometry/Riemannian/HarmonicCore/Energy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficient_memLp line 10
  2. def OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientLinear line 19
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientLinear_norm line 38
  4. def OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientCLM line 48
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientCLM_coercive line 53
  6. def OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevEnergy line 69
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevEnergy_coercive line 75
  8. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.variational_dirichlet_unique line 91
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coeff_contDiff line 112
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.determinant_contDiff line 115
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.inverse_contDiff line 125
  12. def OAI.HarmonicCounterexample.Main.SmoothMetric3.energyMatrix line 139
  13. def OAI.HarmonicCounterexample.Main.SmoothMetric3.matrixOperator line 142
  14. def OAI.HarmonicCounterexample.Main.SmoothMetric3.energyOperator line 145
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyMatrix_continuous line 148
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyOperator_continuous line 152
  17. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyMatrix_positive line 155
  18. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyOperator_pos line 158
  19. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.energyOperator_uniform line 169
  20. def OAI.HarmonicCounterexample.Main.SmoothMetric3.clippedEnergyOperator line 207
  21. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.clippedEnergyOperator_measurable line 210
  22. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.clippedEnergyOperator_uniform line 216
  23. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevEnergy_eq_integral line 235
  24. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_variational_dirichlet_unique line 246
  25. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_affine_dirichlet_unique line 256