OAI/Analysis/LpDimension/StableIntensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SubpolynomialLp.powerIntensity line 12
  2. lemma OAI.SubpolynomialLp.powerIntensity_integral line 15
  3. lemma OAI.SubpolynomialLp.powerIntensity_restrict_integral line 24
  4. lemma OAI.SubpolynomialLp.powerIntensity_tail line 37
  5. lemma OAI.SubpolynomialLp.powerIntensity_large_moment line 55
  6. lemma OAI.SubpolynomialLp.powerIntensity_critical_moment line 72
  7. def OAI.SubpolynomialLp.stableKernel line 86
  8. lemma OAI.SubpolynomialLp.stableKernel_abs_le_quadratic line 88
  9. lemma OAI.SubpolynomialLp.stableKernel_abs_le_large line 108
  10. lemma OAI.SubpolynomialLp.stableKernel_integrable line 116
  11. lemma OAI.SubpolynomialLp.stableKernel_scaling_pos line 143
  12. lemma OAI.SubpolynomialLp.stableKernel_scaling line 159