RationalGridCount.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact short-arc counts for a shifted rational grid. The integer lift below counts the actual points, including closed arc endpoints.

theorem OAI.QuantitativeVanDerWaerden.rho_eq_abs_centered_half_shift line 14
theorem OAI.QuantitativeVanDerWaerden.integer_interval_card_le line 34
def OAI.QuantitativeVanDerWaerden.rationalGridLift line 44
theorem OAI.QuantitativeVanDerWaerden.rationalGridLift_identity line 47
theorem OAI.QuantitativeVanDerWaerden.rationalGridLift_injective line 56
theorem OAI.QuantitativeVanDerWaerden.uniform_grid_centered_count_le line 82
Source documentation
An equally spaced shifted grid has at most 2*e*s+1 points in a closed circle arc of radius e. This remains true for large radii.
```
theorem uniform_grid_centered_count_le (s : ℕ) (hs : 0 < s) (y e : ℝ)
    (he : 0 ≤ e) :
    (((univ : Finset (Fin s)).filter
      (fun j => |centered (y + (j.val : ℝ) / s)| ≤ e)).card : ℝ) ≤
      2 * e * s + 1 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.centered
theorem OAI.QuantitativeVanDerWaerden.uniform_grid_rho_count_le line 115
theorem OAI.QuantitativeVanDerWaerden.rational_grid_rho_closed_count_le line 137

theorem OAI.QuantitativeVanDerWaerden.rational_grid_rho_count_le line 171

Source documentation

Strict cut-neighborhood version used for nonregular positions.

theorem rational_grid_rho_count_le (h a : ℕ) (hh : 0 < h) (y η : ℝ)
    (hη : 0 ≤ η) :
    (((univ : Finset (Fin h)).filter
      (fun z => rho (y + (z.val : ℝ) * a / h) < 2 * η)).card : ℝ) ≤
      (h : ℝ) * (4 * η + 1 / (h / Nat.gcd h a : ℕ)) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.rho