OAI/MathematicalPhysics/RapidForcing/FormulaNames.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RapidForcing.EffectiveProfile.Formula.lipBound line 13
2. lemma OAI.RapidForcing.EffectiveProfile.Formula.lipBound_nonneg line 20
3. lemma OAI.RapidForcing.EffectiveProfile.Formula.abs_sub_le_lipBound line 29
4. def OAI.RapidForcing.EffectiveProfile.Formula.RationalName line 60
5. def OAI.RapidForcing.EffectiveProfile.Formula.choosePrecision line 63
6. lemma OAI.RapidForcing.EffectiveProfile.Formula.choosePrecision_spec line 66
7. lemma OAI.RapidForcing.EffectiveProfile.Formula.choosePrecision_dom line 75
8. def OAI.RapidForcing.EffectiveProfile.Formula.evalName line 86
9. lemma OAI.RapidForcing.EffectiveProfile.Formula.rationalName_spec line 95
10. lemma OAI.RapidForcing.EffectiveProfile.Formula.accuracy_le_one line 101
11. lemma OAI.RapidForcing.EffectiveProfile.Formula.name_box line 104
12. lemma OAI.RapidForcing.EffectiveProfile.Formula.evalName_spec line 139
13. lemma OAI.RapidForcing.EffectiveProfile.Formula.evalName_dom line 164