OAI/Analysis/LpDimension/DyadicRamps.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SubpolynomialLp.tailPart line 12
  2. def OAI.SubpolynomialLp.cutPart line 14
  3. def OAI.SubpolynomialLp.bandPart line 16
  4. def OAI.SubpolynomialLp.dyadicRamp line 18
  5. lemma OAI.SubpolynomialLp.tailPart_measurable line 21
  6. lemma OAI.SubpolynomialLp.cutPart_measurable line 24
  7. lemma OAI.SubpolynomialLp.bandPart_measurable line 27
  8. lemma OAI.SubpolynomialLp.dyadicRamp_measurable line 31
  9. lemma OAI.SubpolynomialLp.tailPart_add_cutPart line 34
  10. lemma OAI.SubpolynomialLp.bandPart_eq_cutPart line 38
  11. lemma OAI.SubpolynomialLp.abs_cutPart_le line 45
  12. lemma OAI.SubpolynomialLp.bandPart_neg line 49
  13. lemma OAI.SubpolynomialLp.dyadicRamp_neg line 53
  14. lemma OAI.SubpolynomialLp.dyadicRamp_zero_small line 56
  15. lemma OAI.SubpolynomialLp.abs_bandPart_le line 62
  16. lemma OAI.SubpolynomialLp.abs_bandPart_le_tail line 68
  17. lemma OAI.SubpolynomialLp.abs_dyadicRamp_le line 72
  18. lemma OAI.SubpolynomialLp.dyadicRamp_plateau line 83
  19. lemma OAI.SubpolynomialLp.pareto_integrable_moment line 103
  20. lemma OAI.SubpolynomialLp.pareto_tailPart_moment line 121
  21. lemma OAI.SubpolynomialLp.tailPart_abs_le line 135
  22. lemma OAI.SubpolynomialLp.tailPart_neg line 139
  23. lemma OAI.SubpolynomialLp.pareto_tail_sq_integrable line 143
  24. lemma OAI.SubpolynomialLp.pareto_tail_sq_moment line 156
  25. lemma OAI.SubpolynomialLp.dyadicRamp_moment_integrable line 166
  26. lemma OAI.SubpolynomialLp.pareto_dyadicRamp_energy_lower line 175
  27. lemma OAI.SubpolynomialLp.dyadic_variance_weight line 210
  28. lemma OAI.SubpolynomialLp.pareto_dyadicRamp_variance line 219