OAI/Analysis/AllenCahn/Curvature.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DeGiorgi.finite_chord_bounds line 16
2. def OAI.DeGiorgi.DiagonalActive line 42
3. lemma OAI.DeGiorgi.exists_reach_minimizing_sequence line 49
4. theorem OAI.DeGiorgi.reach_active_contact line 95
5. theorem OAI.DeGiorgi.diagonal_contact_tangent_realization line 137
6. lemma OAI.DeGiorgi.second_order_remainder line 184
7. theorem OAI.DeGiorgi.diagonal_active_curvature line 228