OAI/Analysis/AllenCahn/DyadicDerivatives.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RegularitySupport.DeGiorgi.allenCahn_difference_bounds line 16
2. lemma OAI.RegularitySupport.DeGiorgi.allenCahn_difference_bounds_uniform line 85
3. def OAI.RegularitySupport.DeGiorgi.dyadicSlope line 170
4. lemma OAI.RegularitySupport.DeGiorgi.dyadicSlope_step line 173
5. lemma OAI.RegularitySupport.DeGiorgi.dyadicSlope_converges line 203
6. lemma OAI.RegularitySupport.DeGiorgi.dyadicSlope_remainder line 208
7. lemma OAI.RegularitySupport.DeGiorgi.dyadicSlope_bound line 215
8. def OAI.RegularitySupport.DeGiorgi.dyadicDerivative line 228
9. lemma OAI.RegularitySupport.DeGiorgi.tendsto_dyadicDerivative line 231
10. lemma OAI.RegularitySupport.DeGiorgi.dyadicDerivative_bound line 236
11. lemma OAI.RegularitySupport.DeGiorgi.dyadicDerivative_remainder line 242
12. lemma OAI.RegularitySupport.DeGiorgi.dyadicSlope_add_error line 247
13. lemma OAI.RegularitySupport.DeGiorgi.dyadicDerivative_add line 267
14. def OAI.RegularitySupport.DeGiorgi.dyadicDerivativeHom line 281
15. lemma OAI.RegularitySupport.DeGiorgi.dyadicDerivative_continuous line 289
16. def OAI.RegularitySupport.DeGiorgi.dyadicDerivativeCLM line 296
17. lemma OAI.RegularitySupport.DeGiorgi.hasFDerivAt_dyadicDerivative line 300
18. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_tendsto line 318
19. lemma OAI.RegularitySupport.DeGiorgi.differenceBound_fderiv_apply line 326
20. lemma OAI.RegularitySupport.DeGiorgi.contDiff_infty_of_difference_bounds line 352