OAI/Geometry/PrescribedPotential/JetEnergyUniform.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Jet Energy Uniform.

  1. lemma OAI.HigherJet.jetEnergy_le_norm line 22
  2. lemma OAI.HigherJet.jetEnergy_gradient_bound line 33
  3. lemma OAI.HigherJet.familyDissipation_nonneg line 40
  4. lemma OAI.HigherJet.jetEnergy_frame_upper line 44
  5. lemma OAI.BernsteinEstimate.first_energy_scaled line 75
  6. lemma OAI.BernsteinEstimate.cubic_energy_scaled line 87
  7. lemma OAI.BernsteinEstimate.linear_energy_scaled line 103