LongPeriodRegularity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Counting regular positions in a long-period block

The finite union bound is expressed on literal subsets of the block indices. The coordinate bounds are supplied by the actual rational-grid count.

theorem OAI.QuantitativeVanDerWaerden.regular_count_of_coordinate_bounds line 17

theorem OAI.QuantitativeVanDerWaerden.regular_positions_eq_complement line 53

Source documentation

The finite complement in the union bound is exactly the regular-position predicate, with equality at the cut-distance threshold retained as regular.

theorem regular_positions_eq_complement {D h : ℕ}
    (rotating : Finset (Fin D)) (Y : Fin h → Fin D → ℝ) (η : ℝ) :
    (Finset.univ.filter fun z => ∀ i ∈ rotating, η ≤ rho (Y z i)) =
      Finset.univ \ rotating.biUnion
        (fun i => Finset.univ.filter fun z => rho (Y z i) < η) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.rho

theorem OAI.QuantitativeVanDerWaerden.regular_fraction_constant line 63