OAI/NumberTheory/JointDickman/Amplification/FiniteWeightedSquare.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite square bound for the smoothed coefficient sum

  1. theorem OAI.JointDickman.finite_weighted_square_bound line 9
  2. theorem OAI.JointDickman.finite_weighted_square_mean line 24
  3. theorem OAI.JointDickman.norm_square_le_twice_difference line 45