OAI/MathematicalPhysics/RapidForcing/JetBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RapidForcing.finite_order line 9
2. lemma OAI.RapidForcing.jet_sum_le line 15
3. lemma OAI.RapidForcing.jet_postcomp_le line 21
4. lemma OAI.RapidForcing.jet_smul_const_le line 26
5. lemma OAI.RapidForcing.EffectiveProfile.Formula.fderiv_eq_sum line 35
6. lemma OAI.RapidForcing.EffectiveProfile.Formula.jet_succ_le line 50
7. def OAI.RapidForcing.EffectiveProfile.Formula.allDiff line 65
8. def OAI.RapidForcing.EffectiveProfile.Formula.jetBound line 68
9. lemma OAI.RapidForcing.EffectiveProfile.Formula.jetBound_nonneg line 71
10. lemma OAI.RapidForcing.EffectiveProfile.Formula.jet_list_le line 77
11. lemma OAI.RapidForcing.EffectiveProfile.Formula.norm_jet_le line 98