OAI/NumberTheory/EgyptianFractions/ResidueIntervalCount.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.card_range_zmod_eq line 10

   Source documentation

   The exact number of natural numbers below N in one residue class.

   theorem card_range_zmod_eq {d : ℕ} [NeZero d] (N : ℕ) (r : ZMod d) :
       ((Finset.range N).filter (fun n : ℕ => (n : ZMod d) = r)).card =
         N / d + if r.val < N % d then 1 else 0 := by
   …

2. theorem OAI.Problem337.card_range_zmod_mem line 24

   Source documentation

   Exact quotient/remainder decomposition for any collection of residues.

   theorem card_range_zmod_mem {d : ℕ} [NeZero d] (N : ℕ) (S : Finset (ZMod d)) :
       ((Finset.range N).filter (fun n : ℕ => (n : ZMod d) ∈ S)).card =
         (N / d) * S.card + (S.filter (fun r => r.val < N % d)).card := by
   …

3. theorem OAI.Problem337.abs_card_range_zmod_mem_sub line 36

   Source documentation

   The elementary progression-counting error is at most the number of residue classes, uniformly in the interval length and modulus.

   theorem abs_card_range_zmod_mem_sub {d : ℕ} [NeZero d]
       (N : ℕ) (S : Finset (ZMod d)) :
       |(((Finset.range N).filter (fun n : ℕ => (n : ZMod d) ∈ S)).card : ℝ) -
         (N : ℝ) * S.card / d| ≤ (S.card : ℝ) := by
   …