HeavyIntervalWidth.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Drift relative to every heavy label interval

All occurrences of a label are in one residue class modulo the primitive return denominator. Packing these actual occurrence indices gives at least card - 1 periods between the extreme visits. Their representatives alone then determine the real accumulated drift: the integral discrepancy is too small to be nonzero. No assertion about the path between the visits is used.

theorem OAI.QuantitativeVanDerWaerden.rational_path_period_difference line 25

Source documentation

At indices differing by c denominator periods, the rational numerator disappears modulo integers and only c times the drift remains.

theorem rational_path_period_difference {ι : Type uIndex} {h a b c : ℕ}
    (Y : ℕ → ι → ℝ) (A v : ι → ℝ) (s : ι → ℤ)
    (hh : 0 < h) (hab : a ≤ b) (hspan : b - a = c * h)
    (hpath : ∀ n i, ∃ z : ℤ,
      Y n i - A i - (n : ℝ) / h * ((s i : ℝ) + v i) = z) (i : ι) :
    ∃ z : ℤ, (Y b i - Y a i) - (c : ℝ) * v i = z := by
…

theorem OAI.QuantitativeVanDerWaerden.heavy_fiber_relative_width line 48

Source documentation

A heavy set of occurrences in one residue class controls the common drift by the actual width of every one of its coordinate intervals.

theorem heavy_fiber_relative_width {ι : Type uIndex} {J : Finset ℕ} {k h : ℕ}
    {M H : ℝ} (Y : ℕ → ι → ℝ) (A v L : ι → ℝ) (s : ι → ℤ)
    (hM : 0 < M) (hscale : 2 * M ≤ (k : ℝ))
    (hheavy : (k : ℝ) / M < J.card) (hh : 0 < h)
    (hbound : ∀ j ∈ J, j < k)
    (hcongr : ∀ a ∈ J, ∀ b ∈ J, (h : ℤ) ∣ (b : ℤ) - a)
    (hpath : ∀ n i, ∃ z : ℤ,
      Y n i - A i - (n : ℝ) / h * ((s i : ℝ) + v i) = z)
    (hbox : ∀ a ∈ J, ∀ b ∈ J, ∀ i, |Y b i - Y a i| ≤ L i)
    (hwidth : ∀ i, L i ≤ 2 * H)
    (hdrift : ∀ i, |v i| ≤ 4 * M * H / (k : ℝ))
    (hsmall : 2 * H + 4 * M * H / (h : ℝ) < 1) :
…

theorem OAI.QuantitativeVanDerWaerden.heavy_label_relative_width line 94

Source documentation

Apply the endpoint argument to the actual occurrence fiber of any heavy label, including labels different from the one that supplied the return.

theorem heavy_label_relative_width {ι : Type uIndex} {B : Type uB} {k h j : ℕ}
    {M H : ℝ} (Y : ℕ → ι → ℝ) (A v : ι → ℝ) (s : ι → ℤ)
    (label : ℕ → B) (width : B → ι → ℝ)
    (hM : 0 < M) (hscale : 2 * M ≤ (k : ℝ))
    (hheavy : (k : ℝ) / M < (labelFiber k label (label j)).card) (hh : 0 < h)
    (hcongr : ∀ a, a < k → ∀ b, b < k → label a = label b →
      (h : ℤ) ∣ (b : ℤ) - a)
    (hpath : ∀ n i, ∃ z : ℤ,
      Y n i - A i - (n : ℝ) / h * ((s i : ℝ) + v i) = z)
    (hbox : ∀ a, a < k → ∀ b, b < k → label a = label b →
      ∀ i, |Y b i - Y a i| ≤ width (label a) i)
    (hwidth : ∀ i, width (label j) i ≤ 2 * H)
…

Mentions: OAI.QuantitativeVanDerWaerden.labelFiber