`ψ - ψ_β ≤ 8β`

Proved

BlockCycleRotation.psi_sub_psiBuf_le_linear

by dbenbenn · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmsblock-cycle-rotationreal-analysis

ψ - ψ_β ≤ 8β.

This is an auxiliary lemma of the formalization rather than a result stated in the paper. It is used in the proof of tendsto_psiBuf.

Preamble

import Definitions.Def_BlockCycleRotation_Buffer
import Definitions.Def_BlockCycleRotation_Theorem10
import Mathlib

open BlockCycleRotation
open Finset Filter Topology Real MeasureTheory BoxIntegral
open scoped ENNReal

Formal statement

theorem BlockCycleRotation.psi_sub_psiBuf_le_linear {β x : ℝ} (hβ : 0 < β) (hx0 : 0 ≤ x) (hx : x ≤ 1 / 2) :
    psi x - psiBuf β x ≤ 8 * β := by sorry

Source

Valentin Blomer and Kai-Uwe Bux, "The cost of cyclic permutations and remainder sums in the Euclidean algorithm", AofA 2026, LIPIcs vol. 381, pp. 14:1-14:17, doi:10.4230/LIPIcs.AofA.2026.14. Numbering follows the full version, arXiv:2601.00979v1. Lean source: https://github.com/dbenbenn/block-cycle-rotation/blob/f69003fd8b00c9b5d6d1a4f6807b4943bce0a92c/BlockCycleRotation/Buffer.lean#L351-L369

View graph