OAI/Analysis/NodalLength/Regularization.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.truncBelow line 51
  2. lemma OAI.SharpNodal.Profiles.coe_truncBelow line 55
  3. lemma OAI.SharpNodal.Profiles.truncBelow_nonpos line 63
  4. lemma OAI.SharpNodal.Profiles.truncBelow_lower line 70
  5. lemma OAI.SharpNodal.Profiles.truncBelow_antitone line 77
  6. def OAI.SharpNodal.Profiles.supRegularize line 84
  7. lemma OAI.SharpNodal.Profiles.regularize_bdd line 87
  8. lemma OAI.SharpNodal.Profiles.supRegularize_nonpos line 93
  9. lemma OAI.SharpNodal.Profiles.supRegularize_majorant line 99
  10. lemma OAI.SharpNodal.Profiles.supRegularize_antitone line 107
  11. lemma OAI.SharpNodal.Profiles.supRegularize_lipschitz line 117
  12. lemma OAI.SharpNodal.Profiles.supRegularize_eventually_below line 138
  13. lemma OAI.SharpNodal.Profiles.iInf_supRegularize line 161
  14. lemma OAI.SharpNodal.Profiles.tendsto_supRegularize line 172
  15. def OAI.SharpNodal.Profiles.circleParameterMeasure line 187
  16. lemma OAI.SharpNodal.Profiles.circleAverage_eq_integral_parameter line 190
  17. lemma OAI.SharpNodal.Profiles.circleParameter_integrable line 196
  18. lemma OAI.SharpNodal.Profiles.toENNReal_coe_real line 201
  19. theorem OAI.SharpNodal.Profiles.circle_submean line 204
  20. def OAI.SharpNodal.Profiles.polarParameterMeasure line 260
  21. lemma OAI.SharpNodal.Profiles.circleAverage_eq_integral_polar line 263
  22. lemma OAI.SharpNodal.Profiles.polarParameter_integrable line 271
  23. theorem OAI.SharpNodal.Profiles.circle_submean_polar line 278
  24. lemma OAI.SharpNodal.Profiles.polarCoord_eq_circleMap line 334
  25. lemma OAI.SharpNodal.Profiles.lintegral_radius line 339
  26. lemma OAI.SharpNodal.Profiles.lintegral_ball_le_of_angular line 349
  27. lemma OAI.SharpNodal.Profiles.lintegral_ball_center_le_of_angular line 387
  28. lemma OAI.SharpNodal.Profiles.lintegral_plane_ball_complex line 412
  29. theorem OAI.SharpNodal.Profiles.disk_submean line 431
  30. theorem OAI.SharpNodal.Profiles.disk_lintegral_le_of_anchor line 457
  31. theorem OAI.SharpNodal.Profiles.profile_lintegral_D8 line 468
  32. lemma OAI.SharpNodal.Profiles.usc_neg_toENNReal_aemeasurable line 498
  33. lemma OAI.SharpNodal.Profiles.profile_integrable_of_lintegral_ne_top line 505
  34. lemma OAI.SharpNodal.Profiles.profile_norm_integral_le line 520