RationalGridMultiplicity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Multiplicities in a rational circle grid

An integer-periodic predicate samples a rational step a / h on precisely h / gcd h a different points, each with multiplicity gcd h a. The proof reindexes actual finite types using division with remainder and the permutation given by multiplication by a coprime numerator.

def OAI.QuantitativeVanDerWaerden.mulModGridEquiv line 24
Source documentation
Multiplication by a coprime natural number permutes the finite residues.
```
noncomputable def mulModGridEquiv (s b : ℕ) (hs : 0 < s)
    (hcop : Nat.gcd s b = 1) : Equiv.Perm (Fin s) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.mulModGridEquiv_val line 35

theorem OAI.QuantitativeVanDerWaerden.periodic_predicate_div_mod line 41

Source documentation

An integer-periodic predicate is unchanged when a rational numerator is reduced modulo its positive denominator.

theorem periodic_predicate_div_mod (P : ℝ → Prop)
    (hperiod : ∀ x (n : ℤ), P (x + n) ↔ P x)
    (y : ℝ) (n s : ℕ) (hs : 0 < s) :
    P (y + (n : ℝ) / s) ↔ P (y + ((n % s : ℕ) : ℝ) / s) := by
…

theorem OAI.QuantitativeVanDerWaerden.card_coprime_rational_grid_periodic line 59

Source documentation

A full block with a coprime step visits every point of its uniform grid once, for every integer-periodic predicate.

theorem card_coprime_rational_grid_periodic (s b : ℕ) (hs : 0 < s)
    (hcop : Nat.gcd s b = 1) (P : ℝ → Prop) [DecidablePred P]
    (hperiod : ∀ x (n : ℤ), P (x + n) ↔ P x) (y : ℝ) :
    Fintype.card {j : Fin s // P (y + (j.val : ℝ) * b / s)} =
      Fintype.card {j : Fin s // P (y + (j.val : ℝ) / s)} := by
…

theorem OAI.QuantitativeVanDerWaerden.card_repeated_rational_grid_periodic line 72

Source documentation

Repeating the rational step for d full denominator blocks multiplies every periodic-predicate count by d.

theorem card_repeated_rational_grid_periodic (d s b : ℕ) (hs : 0 < s)
    (P : ℝ → Prop) [DecidablePred P]
    (hperiod : ∀ x (n : ℤ), P (x + n) ↔ P x) (y : ℝ) :
    Fintype.card {z : Fin (d * s) // P (y + (z.val : ℝ) * b / s)} =
      d * Fintype.card {j : Fin s // P (y + (j.val : ℝ) * b / s)} := by
…

theorem OAI.QuantitativeVanDerWaerden.card_rational_grid_periodic line 105

Source documentation

Exact multiplicity of the reduced rational grid. This applies to any predicate invariant under integer translation, including circle arcs.

theorem card_rational_grid_periodic (h a : ℕ) (hh : 0 < h)
    (P : ℝ → Prop) [DecidablePred P]
    (hperiod : ∀ x (n : ℤ), P (x + n) ↔ P x) (y : ℝ) :
    Fintype.card {z : Fin h // P (y + (z.val : ℝ) * a / h)} =
      Nat.gcd h a * Fintype.card {j : Fin (h / Nat.gcd h a) //
        P (y + (j.val : ℝ) / (h / Nat.gcd h a : ℕ))} := by
…

theorem OAI.QuantitativeVanDerWaerden.card_filter_rational_grid_periodic line 137

Source documentation

Finset-filter form of the exact rational-grid multiplicity formula.

theorem card_filter_rational_grid_periodic (h a : ℕ) (hh : 0 < h)
    (P : ℝ → Prop) [DecidablePred P]
    (hperiod : ∀ x (n : ℤ), P (x + n) ↔ P x) (y : ℝ) :
    (Finset.univ.filter (fun z : Fin h => P (y + (z.val : ℝ) * a / h))).card =
      Nat.gcd h a * (Finset.univ.filter (fun j : Fin (h / Nat.gcd h a) =>
        P (y + (j.val : ℝ) / (h / Nat.gcd h a : ℕ)))).card := by
…