OAI/Analysis/AllenCahn/Reach.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeGiorgi.interfaceNormal line 15
  2. def OAI.DeGiorgi.regularZeroSet line 18
  3. def OAI.DeGiorgi.chordDirection line 21
  4. def OAI.DeGiorgi.chordAngle line 23
  5. def OAI.DeGiorgi.reachChordValue line 26
  6. def OAI.DeGiorgi.penalizedReach line 30
  7. def OAI.DeGiorgi.OffDiagonalActive line 33
  8. lemma OAI.DeGiorgi.interfaceNormal_norm line 37
  9. lemma OAI.DeGiorgi.chordDirection_norm line 42
  10. lemma OAI.DeGiorgi.chordAngle_le_one line 47
  11. lemma OAI.DeGiorgi.chord_backwards line 52
  12. lemma OAI.DeGiorgi.active_contact_no_nearer_zero_on_ray line 66
  13. lemma OAI.DeGiorgi.active_bases_on_ray_unique line 95
  14. lemma OAI.DeGiorgi.active_ray_subsingleton line 105
  15. lemma OAI.DeGiorgi.chordAngle_mul_length line 111
  16. lemma OAI.DeGiorgi.reach_chord_inequality line 118
  17. lemma OAI.DeGiorgi.reach_tangent_ball_zero_free line 153
  18. lemma OAI.DeGiorgi.penalized_normal_map_injective line 184
  19. lemma OAI.DeGiorgi.quadratic_residual_of_lipschitz_fderiv line 244
  20. lemma OAI.DeGiorgi.regular_zero_local_chord_bound line 272
  21. lemma OAI.DeGiorgi.penalizedReach_pos line 295
  22. lemma OAI.DeGiorgi.chordAngle_continuousAt line 336