LongPeriodBlocks.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Full blocks in the long-period alternative

All displacements are actual real representatives modulo an explicitly integral error. In particular, the heavy anchor in the stationary-coordinate argument need not be a regular position.

theorem OAI.QuantitativeVanDerWaerden.rational_full_block_reanchor line 24

Source documentation

Re-anchor an actual rational path at the beginning of a full block.

theorem rational_full_block_reanchor {k h j₀ : ℕ} {a : ℤ} {y v : ℝ}
    (Y : ℕ → ℝ) (hh : 0 < h) (hfull : j₀ + h ≤ k)
    (hpath : ∀ j, j < k → ∃ e : ℤ,
      Y j - y - (j : ℝ) / h * ((a : ℝ) + v) = e) :
    ∀ z : Fin h, ∃ e : ℤ,
      Y (j₀ + z.val) - Y j₀ - (z.val : ℝ) / h * ((a : ℝ) + v) = e := by
…

theorem OAI.QuantitativeVanDerWaerden.full_block_drift_le line 41
Source documentation
A block displacement accumulates at most one unit of its drift vector.
```
theorem full_block_drift_le {h : ℕ} (hh : 0 < h) (z w : Fin h) (v : ℝ) :
    |((z.val : ℝ) - w.val) / h * v| ≤ |v| := by
…
```

theorem OAI.QuantitativeVanDerWaerden.stationary_full_block_distance line 50

Source documentation

If the rational step is integral, every pair of block positions is within one drift amplitude modulo integers, including centered cut crossings.

theorem stationary_full_block_distance {h : ℕ} {a : ℤ} {y v : ℝ}
    (Y : Fin h → ℝ) (hh : 0 < h) (hstationary : (h : ℤ) ∣ a)
    (hpath : ∀ z, ∃ e : ℤ,
      Y z - y - (z.val : ℝ) / h * ((a : ℝ) + v) = e)
    (z w : Fin h) :
    ∃ e : ℤ, |centered (Y z) - centered (Y w) - e| ≤ |v| := by
…

Mentions: OAI.QuantitativeVanDerWaerden.centered

theorem OAI.QuantitativeVanDerWaerden.stationary_full_block_width line 88

Source documentation

Actual stationary-coordinate interval widths satisfy eligibility at every position, using any heavy anchor, without regularity of that anchor.

theorem stationary_full_block_width (A : AdaptiveMesh)
    {h : ℕ} {a : ℤ} {y v : ℝ} (Y : Fin h → ℝ)
    (hh : 0 < h) (hstationary : (h : ℤ) ∣ a)
    (hpath : ∀ z, ∃ e : ℤ,
      Y z - y - (z.val : ℝ) / h * ((a : ℝ) + v) = e)
    (anchor : Fin h)
    (hrelative : |v| ≤ A.width (A.meshLabel (Y anchor)) / 16) :
    ∀ z, |v| ≤ A.width (A.meshLabel (Y z)) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh

theorem OAI.QuantitativeVanDerWaerden.stationary_relative_width_threshold line 106

theorem OAI.QuantitativeVanDerWaerden.nonregular_implies_grid_near line 114

Source documentation

A truly nonregular sample must be near the cut in its undrifted grid. The error is explicitly integral; this includes every representative cut.

theorem nonregular_implies_grid_near {h : ℕ} (hh : 0 < h)
    (z : Fin h) {a : ℝ} {y v actual η : ℝ}
    (hpath : ∃ e : ℤ,
      actual - y - (z.val : ℝ) / h * (a + v) = e)
    (hdrift : |v| < η) (hbad : rho actual < η) :
    rho (y + (z.val : ℝ) * a / h) < 2 * η := by
…

Mentions: OAI.QuantitativeVanDerWaerden.rho