OAI/Geometry/PrescribedPotential/QuasilinearJetBasics.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Quasilinear Jet Basics.

  1. def OAI.HigherJet.firstJet line 20
  2. lemma OAI.HigherJet.firstJet_smoothOn line 21
  3. lemma OAI.HigherJet.firstJet_smoothAt line 24
  4. lemma OAI.HigherJet.norm_firstJet_deriv line 26
  5. lemma OAI.HigherJet.composition_first_jet_bound line 33
  6. lemma OAI.HigherJet.compact_coefficient_jets line 43
  7. lemma OAI.HigherJet.norm_hessian_deriv line 62
  8. lemma OAI.HigherJet.frozen_first_bound line 69
  9. lemma OAI.HigherJet.frozen_second_bound line 79