OAI/Analysis/AllenCahn/JetProducts.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.coordinateJet_mul_rest line 9
  2. lemma OAI.DeGiorgi.list_relative_sum_bound line 18
  3. def OAI.DeGiorgi.JetControl line 35
  4. lemma OAI.DeGiorgi.JetControl.mono_order line 39
  5. lemma OAI.DeGiorgi.JetControl.mono_weight line 43
  6. lemma OAI.DeGiorgi.JetControl.const line 50
  7. lemma OAI.DeGiorgi.JetControl.add line 58
  8. lemma OAI.DeGiorgi.JetControl.const_mul line 71
  9. lemma OAI.DeGiorgi.JetControl.sub line 81
  10. lemma OAI.DeGiorgi.JetControl.mul line 88
  11. lemma OAI.DeGiorgi.JetControl.sum line 111
  12. lemma OAI.DeGiorgi.JetControl.deriv line 129
  13. lemma OAI.DeGiorgi.JetControl.of_zero line 139
  14. lemma OAI.DeGiorgi.finset_relative_sum_bound line 147
  15. lemma OAI.DeGiorgi.coordinateJet_drift_system line 163
  16. lemma OAI.DeGiorgi.JetControl.bootstrap line 191
  17. lemma OAI.DeGiorgi.JetControl.congr line 243
  18. lemma OAI.DeGiorgi.JetControl.of_derivs line 249
  19. lemma OAI.DeGiorgi.JetControl.mul_bounded line 262
  20. def OAI.DeGiorgi.positiveDefectClass line 268
  21. lemma OAI.DeGiorgi.positiveDefectClass_smooth line 272
  22. lemma OAI.DeGiorgi.positiveDefectClass_interior line 275
  23. lemma OAI.DeGiorgi.positiveDefectClass_pde line 278
  24. lemma OAI.DeGiorgi.positiveDefectClass_positive line 281
  25. lemma OAI.DeGiorgi.defect_le_root line 284
  26. lemma OAI.DeGiorgi.positiveAC_jet_base line 288
  27. lemma OAI.DeGiorgi.positiveAC_root_product line 312