OAI/NumberTheory/CubicMoment/Estimates/LogarithmicWeightFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A polynomial logarithmic derivative cost can be normalized by any fixed positive power of the outer length. This gives a uniform smooth family without discarding the original, varying test functions.

  1. lemma OAI.CubicFirstMoment.log_power_normalization_bound line 13
  2. structure OAI.CubicFirstMoment.LogarithmicWeightFamily line 41
  3. def OAI.CubicFirstMoment.normalizedLogWeight line 52
  4. def OAI.CubicFirstMoment.LogarithmicWeightFamily.normalize line 55