LongPeriodRegularGrid.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The regular-position bound instantiated with the actual shifted rational grids and their actual integer periods.

theorem OAI.QuantitativeVanDerWaerden.long_block_regular_card line 14

Source documentation

At least half the positions in a full long-period block are regular. The coordinate count is proved by the rational-grid theorem, including grid multiplicity; it is not an assumption of this statement.

theorem long_block_regular_card {D h : ℕ} (hh : 0 < h) (hD : 0 < D)
    (rotating : Finset (Fin D)) (Y : Fin h → Fin D → ℝ)
    (y v : Fin D → ℝ) (a : Fin D → ℕ) (η : ℝ) (hη : 0 ≤ η)
    (hpath : ∀ i ∈ rotating, ∀ z, ∃ e : ℤ,
      Y z i - y i - (z.val : ℝ) / h * ((a i : ℝ) + v i) = e)
    (hdrift : ∀ i ∈ rotating, |v i| < η)
    (hperiod : ∀ i ∈ rotating, D ^ 2 < h / Nat.gcd h (a i))
    (hsmall : (D : ℝ) * (4 * η + 1 / (D : ℝ) ^ 2) ≤ 1 / 2) :
    (h : ℝ) / 2 ≤
      ((Finset.univ.filter fun z => ∀ i ∈ rotating, η ≤ rho (Y z i)).card : ℝ) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.rho

theorem OAI.QuantitativeVanDerWaerden.long_block_regular_card_at_scale line 53