CyclicHeavyIntervalWidth.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Drift relative to actual heavy adaptive intervals

The heavy multiplicity is counted over Fin k using the actual literal full label. Its natural-index fiber has the same cardinality. Equal labels place the actual centered representatives in the same half-open interval, providing the width bound required by the general endpoint argument.

theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_second_width line 20
Source documentation
Equal literal labels bound the difference by the actual adaptive interval width, rather than only by the uniform upper bound on mesh widths.
```
theorem literalFullLabel_second_width (mesh : AdaptiveMesh)
    (q D lam Ucount : ℕ) (hU : 0 < Ucount) {a b : CyclicGroup q D}
    (hlabel : literalFullLabel mesh q D lam Ucount hU a =
      literalFullLabel mesh q D lam Ucount hU b) (i : Fin D) :
    |yRep q D lam b i - yRep q D lam a i| ≤
      mesh.width ((literalFullLabel mesh q D lam Ucount hU a).2 i) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.literalFullLabel, OAI.QuantitativeVanDerWaerden.yRep

theorem OAI.QuantitativeVanDerWaerden.cyclic_heavy_label_relative_width line 38

Source documentation

Every heavy literal-label fiber controls the drift relative to the width of its own adaptive interval in every coordinate.

theorem cyclic_heavy_label_relative_width (mesh : AdaptiveMesh)
    {q D lam Ucount k h : ℕ} (hU : 0 < Ucount)
    (a d : CyclicGroup q D) (A v : Fin D → ℝ) (s : Fin D → ℤ) (j : Fin k)
    {M : ℝ} (hM : 0 < M) (hscale : 2 * M ≤ (k : ℝ))
    (hheavy : (k : ℝ) / M <
      (Finset.univ.filter (fun n : Fin k =>
        literalFullLabel mesh q D lam Ucount hU (a + n.val • d) =
        literalFullLabel mesh q D lam Ucount hU (a + j.val • d))).card)
    (hh : 0 < h)
    (hcongr : ∀ m, m < k → ∀ n, n < k →
      literalFullLabel mesh q D lam Ucount hU (a + m • d) =
        literalFullLabel mesh q D lam Ucount hU (a + n • d) →
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.literalFullLabel