OAI/NumberTheory/CubicMoment/Estimates/DyadicWeightIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A supported height weight is controlled by the actual two-sided dyadic mean. The normalization includes both height intervals.

  1. def OAI.CubicFirstMoment.dyadicHeightSupport line 11
  2. lemma OAI.CubicFirstMoment.dyadicWeightIntegral_bound line 13
  3. lemma OAI.CubicFirstMoment.normalized_dyadicWeightIntegral_bound line 44