A uniform bound for increments of the growth primitive

Proved

BianchiIX.coreGrowthPrimitive_difference

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

For real $k,z$ , define

\Gamma_k(z)=2\arctan(\sinh z)+\frac{24}{10000k}z, \qquad C_* = \exp\left(2\pi+\frac{48}{10000}\right).

Division at zero has its total real-field meaning. If $k\geq6$ and $|a|,|b|\leq\log(4k)$ , then

\Gamma_k(b)-\Gamma_k(a)\leq2\pi+48/10000.

Preamble

import Definitions.Def_BianchiIX_Analysis_CoreGrowthBudget
import Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

noncomputable section
open BianchiIX

Formal statement

theorem BianchiIX.coreGrowthPrimitive_difference {k a b : ℝ} (hk : 6 ≤ k)
    (ha : |a| ≤ Real.log (4 * k)) (hb : |b| ≤ Real.log (4 * k)) :
    coreGrowthPrimitive k b - coreGrowthPrimitive k a ≤ 2 * Real.pi + 48 / 10000 := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/CoreGrowthBudget.lean#L32-L48

View graph