OAI/NumberTheory/CubicMoment/Estimates/WeightedSquarefreeMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A weighted norm-fiber mean. The divisor weight is retained explicitly so coprimality rows can later be summed without a uniform-fiber loss.

  1. lemma OAI.CubicFirstMoment.normCollectedCoeff_squarefree_weighted_energy line 13
  2. lemma OAI.CubicFirstMoment.squarefree_weighted_meanSquare line 35
  3. lemma OAI.CubicFirstMoment.squarefree_weighted_dyadic_mean line 46
  4. lemma OAI.CubicFirstMoment.squarefree_weighted_character_height line 56