OAI/Geometry/PrescribedRicci/FamilyJetNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Family Jet Norm.

  1. def OAI.TameInterpolation.familyJetNorm line 21
  2. lemma OAI.TameInterpolation.jetNorm_le_family line 24
  3. lemma OAI.TameInterpolation.familyJetNorm_nonneg line 28
  4. lemma OAI.TameInterpolation.familyJetNorm_attained line 32
  5. lemma OAI.TameInterpolation.familyJetNorm_recurrence line 38
  6. lemma OAI.TameInterpolation.exponent_top line 50
  7. theorem OAI.TameInterpolation.family_jet_tame_many line 56