OAI/Geometry/PrescribedPotential/RealJetEnergy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Real Jet Energy.

  1. lemma OAI.HigherJet.dir_add line 18
  2. lemma OAI.HigherJet.dir_smul line 23
  3. lemma OAI.HigherJet.dir_inner line 27
  4. lemma OAI.HigherJet.dir_norm_sq line 33
  5. lemma OAI.HigherJet.dir_dir_norm_sq line 38
  6. def OAI.HigherJet.frameLaplace line 56
  7. def OAI.HigherJet.frameGradientSq line 58
  8. lemma OAI.HigherJet.frameLaplace_norm_sq line 60
  9. lemma OAI.HigherJet.dir_sum line 67
  10. lemma OAI.HigherJet.frameLaplace_sum line 73
  11. def OAI.HigherJet.familyEnergy line 84
  12. def OAI.HigherJet.familyDissipation line 86
  13. lemma OAI.HigherJet.familyEnergy_smoothOn line 89
  14. lemma OAI.HigherJet.familyEnergy_laplace line 93
  15. lemma OAI.HigherJet.familyEnergy_gradient_bound line 102