OAI/Analysis/AllenCahn/HessianControl.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DeGiorgi.diffuseDefect_barrier_lower line 10
2. def OAI.DeGiorgi.sharpDefectConstant line 80
3. theorem OAI.DeGiorgi.diffuseDefect_exponential_comparison line 84
4. lemma OAI.DeGiorgi.positive_defect_log_bounds line 127
5. lemma OAI.DeGiorgi.drift_log_coordinate line 184
6. def OAI.DeGiorgi.logDefectHessianConstant line 215
7. lemma OAI.DeGiorgi.logDefectHessianConstant_pos line 221
8. lemma OAI.DeGiorgi.logDefect_hessian_bound line 227
9. def OAI.DeGiorgi.relativeHessianConstant line 265
10. theorem OAI.DeGiorgi.diffuseDefect_relative_hessian_bound line 268
11. lemma OAI.DeGiorgi.carrier_gradient_estimate line 304