OAI/Analysis/AllenCahn/NormalizedJets.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeGiorgi.defectRoot line 9
  2. lemma OAI.DeGiorgi.defectRoot_pos line 12
  3. lemma OAI.DeGiorgi.defectRoot_sq line 15
  4. lemma OAI.DeGiorgi.defectRoot_eq_sqrt line 20
  5. lemma OAI.DeGiorgi.defectRoot_smooth line 25
  6. lemma OAI.DeGiorgi.defectRoot_gradient line 30
  7. lemma OAI.DeGiorgi.defectRoot_drift line 43
  8. lemma OAI.DeGiorgi.defectRoot_bounds line 67
  9. lemma OAI.DeGiorgi.defectRoot_le_one line 98
  10. lemma OAI.DeGiorgi.normalized_tensor_square_bounds line 102
  11. def OAI.DeGiorgi.normalizedTensorSourceConstant line 115
  12. def OAI.DeGiorgi.normalizedTensorSecondConstant line 119
  13. lemma OAI.DeGiorgi.normalizedTensorSourceConstant_nonneg line 126
  14. lemma OAI.DeGiorgi.normalizedTensorSecondConstant_nonneg line 130
  15. theorem OAI.DeGiorgi.inverseHessian_second_relative line 136
  16. def OAI.DeGiorgi.coordinateJet line 169
  17. lemma OAI.DeGiorgi.coordinateJet_smooth line 173
  18. lemma OAI.DeGiorgi.coordinateJet_laplacian line 179
  19. def OAI.DeGiorgi.jetSplits line 190
  20. lemma OAI.DeGiorgi.jetSplits_length line 195
  21. lemma OAI.DeGiorgi.differentiable_list_sum line 207
  22. lemma OAI.DeGiorgi.coordDeriv_list_sum line 216
  23. lemma OAI.DeGiorgi.coordinateJet_mul line 228
  24. lemma OAI.DeGiorgi.coordinateJet_zero line 251
  25. lemma OAI.DeGiorgi.coordinateJet_const line 261
  26. lemma OAI.DeGiorgi.coordinateJet_add line 275
  27. lemma OAI.DeGiorgi.coordinateJet_const_mul line 287
  28. lemma OAI.DeGiorgi.coordinateJet_sum line 300
  29. lemma OAI.DeGiorgi.coordinateJet_coordDeriv line 311
  30. def OAI.DeGiorgi.jetRestSplits line 321
  31. lemma OAI.DeGiorgi.jetSplits_perm_rest line 326
  32. lemma OAI.DeGiorgi.jetRestSplits_length line 337