OAI/Geometry/ProjectionBodies/ScalarCalculus.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.Scalar.hasDerivAt_inverse_pow line 9
2. lemma OAI.PettyProjection.Scalar.hasDerivAt_e line 15
3. lemma OAI.PettyProjection.Scalar.hasDerivAt_M line 22
4. lemma OAI.PettyProjection.Scalar.M_one line 29
5. lemma OAI.PettyProjection.Scalar.paste_hasDerivAt line 31
6. lemma OAI.PettyProjection.Scalar.paste_contDiff_one line 62
7. def OAI.PettyProjection.Scalar.Mprime line 86
8. def OAI.PettyProjection.Scalar.Iformula line 89
9. lemma OAI.PettyProjection.Scalar.hasDerivAt_Iformula_four line 95
10. lemma OAI.PettyProjection.Scalar.hasDerivAt_Iformula_other line 108
11. lemma OAI.PettyProjection.Scalar.hasDerivAt_Iformula line 136
12. lemma OAI.PettyProjection.Scalar.Mprime_one line 142
13. lemma OAI.PettyProjection.Scalar.Iformula_one line 143
14. lemma OAI.PettyProjection.Scalar.continuousOn_Mprime line 145
15. lemma OAI.PettyProjection.Scalar.contDiff_G line 150
16. lemma OAI.PettyProjection.Scalar.contDiff_I line 158
17. lemma OAI.PettyProjection.Scalar.deriv_G line 163
18. lemma OAI.PettyProjection.Scalar.deriv_I line 169
19. lemma OAI.PettyProjection.Scalar.derivative_relation line 175
20. lemma OAI.PettyProjection.Scalar.I_nonneg line 180
21. lemma OAI.PettyProjection.Scalar.convex_tangent_bound line 198
22. lemma OAI.PettyProjection.Scalar.inverse_pow_tangent line 210
23. lemma OAI.PettyProjection.Scalar.e_lower line 220
24. lemma OAI.PettyProjection.Scalar.M_nonneg line 225
25. lemma OAI.PettyProjection.Scalar.G_bounds line 230
26. lemma OAI.PettyProjection.Scalar.W_mean_expression line 237