OAI/Analysis/AllenCahn/Differences.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RegularitySupport.DeGiorgi.laplacian_poisson_at_max line 16
2. lemma OAI.RegularitySupport.DeGiorgi.bounded_poisson_lipschitz line 91
3. def OAI.RegularitySupport.DeGiorgi.difference line 153
4. def OAI.RegularitySupport.DeGiorgi.iterDifference line 156
5. def OAI.RegularitySupport.DeGiorgi.differenceScale line 160
6. def OAI.RegularitySupport.DeGiorgi.DifferenceBound line 162
7. lemma OAI.RegularitySupport.DeGiorgi.differenceScale_nonneg line 165
8. lemma OAI.RegularitySupport.DeGiorgi.difference_comm line 171
9. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_difference line 178
10. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_add line 184
11. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_sub line 193
12. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_const_mul line 202
13. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_translate line 211
14. lemma OAI.RegularitySupport.DeGiorgi.DifferenceBound.mono line 220
15. lemma OAI.RegularitySupport.DeGiorgi.DifferenceBound.translate line 224
16. lemma OAI.RegularitySupport.DeGiorgi.DifferenceBound.normalized_difference line 230
17. lemma OAI.RegularitySupport.DeGiorgi.DifferenceBound.sub line 244
18. lemma OAI.RegularitySupport.DeGiorgi.DifferenceBound.mul line 254
19. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_contDiff line 311
20. lemma OAI.RegularitySupport.DeGiorgi.laplacian_difference line 317
21. lemma OAI.RegularitySupport.DeGiorgi.laplacian_iterDifference line 327
22. lemma OAI.RegularitySupport.DeGiorgi.iterDifference_eq_zero_of_scale_eq_zero line 336