PeriodicResidueCount.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.periodic_count_mul line 9

Source documentation

A periodic predicate has one full period's worth of solutions in each block.

theorem periodic_count_mul {p : ℕ → Prop} [DecidablePred p] {d : ℕ}
    (hp : Function.Periodic p d) (q : ℕ) :
    Nat.count p (q * d) = q * Nat.count p d := by
…

theorem OAI.Problem337.periodic_count_div_mod line 23

Source documentation

Exact quotient-and-remainder formula for a periodic counting function.

theorem periodic_count_div_mod {p : ℕ → Prop} [DecidablePred p] {d : ℕ}
    (hp : Function.Periodic p d) (N : ℕ) :
    Nat.count p N = (N / d) * Nat.count p d + Nat.count p (N % d) := by
…

theorem OAI.Problem337.periodic_count_discrepancy line 37
Source documentation
The count on a prefix differs from its periodic mean by at most the number of allowed residues in one period. This bound is uniform in the prefix length.
```
theorem periodic_count_discrepancy {p : ℕ → Prop} [DecidablePred p] {d : ℕ}
    (hd : 0 < d) (hp : Function.Periodic p d) (N : ℕ) :
    |(Nat.count p N : ℝ) - (N : ℝ) * Nat.count p d / d| ≤ Nat.count p d := by
…
```

theorem OAI.Problem337.periodic_count_shift_period line 63

Source documentation

Shifting a periodic predicate does not change its mass over a full period.

theorem periodic_count_shift_period {p : ℕ → Prop} [DecidablePred p] {d : ℕ}
    (hp : Function.Periodic p d) (a : ℕ) :
    Nat.count (fun n => p (a + n)) d = Nat.count p d := by
…

theorem OAI.Problem337.filter_Ico_card_eq_count_shift line 74

Source documentation

Counting a predicate on a shifted natural interval is the same as counting its translate on a prefix.

theorem filter_Ico_card_eq_count_shift (p : ℕ → Prop) [DecidablePred p]
    (a N : ℕ) :
    ((Finset.Ico a (a + N)).filter p).card =
      Nat.count (fun n => p (a + n)) N := by
…

theorem OAI.Problem337.periodic_Ico_count_discrepancy line 86

Source documentation

Sharp periodic discrepancy on any shifted interval: the error is bounded by one period's mass, independent of both endpoints.

theorem periodic_Ico_count_discrepancy {p : ℕ → Prop} [DecidablePred p] {d : ℕ}
    (hd : 0 < d) (hp : Function.Periodic p d) (a N : ℕ) :
    |(((Finset.Ico a (a + N)).filter p).card : ℝ) -
      (N : ℝ) * Nat.count p d / d| ≤ Nat.count p d := by
…

theorem OAI.Problem337.zmod_predicate_period_count line 98

Source documentation

The periodic mass of a predicate on residue classes is its finite cardinality.

theorem zmod_predicate_period_count (d : ℕ) [NeZero d]
    (P : ZMod d → Prop) [DecidablePred P] :
    Nat.count (fun n : ℕ => P (n : ZMod d)) d =
      (Finset.univ.filter P).card := by
…

theorem OAI.Problem337.zmod_predicate_Ico_discrepancy line 108

Source documentation

Residue classes are equidistributed up to one copy of the allowed set on any natural interval, without a primality or coprimality assumption.

theorem zmod_predicate_Ico_discrepancy (d : ℕ) [NeZero d]
    (P : ZMod d → Prop) [DecidablePred P] (a N : ℕ) :
    |(((Finset.Ico a (a + N)).filter (fun n : ℕ => P (n : ZMod d))).card : ℝ) -
      (N : ℝ) * (Finset.univ.filter P).card / d| ≤ (Finset.univ.filter P).card := by
…