OAI/NumberTheory/JointDickman/Counting/BlockSquareHits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing all site squares in a block, after taking digit averages

  1. def OAI.JointDickman.BlockSquareHit line 12
  2. theorem OAI.JointDickman.residue_block_squareHit_bound line 15
  3. theorem OAI.JointDickman.block_squareHit_polynomial_bound line 47

    Source documentation

    Polynomially bounded graph tests pay a vanishing total cost when all site squares are removed.

    theorem block_squareHit_polynomial_bound {B M : ℕ} (hB : 1 < B) (hM : M ≤ B^2) :
    (B : ℝ)^10 * ((∑ u : ZMod (auxiliarySquarePeriod B),
      if BlockSquareHit B M u.val then (1 : ℝ) else 0)/(auxiliarySquarePeriod B : ℝ)) ≤
        1/(B : ℝ) := by
…

    Mentions: OAI.JointDickman.auxiliarySquarePeriod, OAI.JointDickman.BlockSquareHit