OAI/Analysis/AllenCahn/NormalMass.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.SmallDefectConverges.mass_positive line 14
  2. theorem OAI.DeGiorgi.small_defect_mean_window_normalized line 30
  3. lemma OAI.DeGiorgi.fderiv_affine_isometry line 100
  4. lemma OAI.DeGiorgi.gradient_affine_isometry line 108
  5. lemma OAI.DeGiorgi.diffuseDefect_affine_isometry line 116
  6. lemma OAI.DeGiorgi.positiveDefectClass_affine_isometry line 124
  7. lemma OAI.DeGiorgi.diffuseNormal_affine_isometry line 139
  8. lemma OAI.DeGiorgi.diffuseMeanCurvature_affine_isometry_zero line 147
  9. lemma OAI.DeGiorgi.gradient_eq_normal line 163
  10. def OAI.DeGiorgi.normalDefectMass line 171
  11. lemma OAI.DeGiorgi.normal_mass_affine_isometry line 174
  12. theorem OAI.DeGiorgi.diffuse_mean_window_positive line 194
  13. lemma OAI.DeGiorgi.normalDefectMass_mono line 238