OAI/MathematicalPhysics/RapidForcing/FieldExpressions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RapidForcing.EffectiveProfile.Expr.approx line 11
2. lemma OAI.RapidForcing.EffectiveProfile.Expr.approx_spec line 14
3. lemma OAI.RapidForcing.EffectiveProfile.Expr.approx_dom line 23
4. inductive OAI.RapidForcing.EffectiveProfile.Formula line 30
5. def OAI.RapidForcing.EffectiveProfile.Formula.value line 40
6. def OAI.RapidForcing.EffectiveProfile.Formula.neg line 47
7. def OAI.RapidForcing.EffectiveProfile.Formula.sub line 49
8. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_neg line 51
9. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_sub line 53
10. def OAI.RapidForcing.EffectiveProfile.Formula.bound line 56
11. lemma OAI.RapidForcing.EffectiveProfile.Formula.bound_nonneg line 63
12. lemma OAI.RapidForcing.EffectiveProfile.Formula.abs_value_le line 71
13. def OAI.RapidForcing.EffectiveProfile.Formula.diff line 83
14. lemma OAI.RapidForcing.EffectiveProfile.Formula.contDiff line 90
15. lemma OAI.RapidForcing.EffectiveProfile.Formula.hasDerivAt_line line 98
16. lemma OAI.RapidForcing.EffectiveProfile.Formula.fderiv_apply_single line 112
17. def OAI.RapidForcing.EffectiveProfile.Formula.evalAt line 122
18. lemma OAI.RapidForcing.EffectiveProfile.Formula.Ball.Covers.center_le line 142
19. lemma OAI.RapidForcing.EffectiveProfile.Formula.numeric_operand_bound line 151
20. lemma OAI.RapidForcing.EffectiveProfile.Formula.evalAt_spec line 162
21. lemma OAI.RapidForcing.EffectiveProfile.Formula.evalAt_dom line 245