OAI/Analysis/AllenCahn/PositiveWindows.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.conePotential_positive_window line 15
  2. lemma OAI.DeGiorgi.conePotential_positive_window_unnormalized line 56
  3. lemma OAI.DeGiorgi.even_normal_derivative_zero line 78
  4. theorem OAI.DeGiorgi.SmallDefectConverges.positive_window line 97
  5. def OAI.DeGiorgi.diffuseNormal line 141
  6. def OAI.DeGiorgi.diffuseMeanCurvature line 144
  7. lemma OAI.DeGiorgi.diffuseNormal_component line 148
  8. lemma OAI.DeGiorgi.diffuseNormal_unit line 155
  9. lemma OAI.DeGiorgi.inverseNormalScale_derivative line 162
  10. lemma OAI.DeGiorgi.diffuseMeanCurvature_zero line 181
  11. lemma OAI.DeGiorgi.fderiv_eq_basis_sum line 227
  12. lemma OAI.DeGiorgi.SmallDefectConverges.directional_D line 237
  13. lemma OAI.DeGiorgi.conjugated_derivative_zero line 245
  14. theorem OAI.DeGiorgi.SmallDefectConverges.mean_limit line 255
  15. lemma OAI.DeGiorgi.profile_uniformContinuous line 282
  16. lemma OAI.DeGiorgi.SmallDefectConverges.v_locallyUniform line 292
  17. lemma OAI.DeGiorgi.SmallDefectConverges.normalized_mass_locallyUniform line 307
  18. def OAI.DeGiorgi.reducedNormalMass line 327
  19. lemma OAI.DeGiorgi.SmallDefectConverges.normal_mass_limit line 330
  20. lemma OAI.DeGiorgi.profileWeight_normal line 353