Prove2Me

The derivative of the angular growth primitive

Proved
BianchiIX.hasDerivAt_coreGrowthPrimitive

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

bianchi-ix-era-statisticsdynamical-systems

For real k,zk,z, define

Γk(z)=2arctan⁡(sinh⁡z)+2410000kz,C∗=exp⁡(2π+4810000).\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. For all real k,zk,z,

Γk′(z)=2cosh⁡z+2410000k.\Gamma_k'(z)=\frac2{\cosh z}+\frac{24}{10000k}.
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.hasDerivAt_coreGrowthPrimitive (k z : ℝ) :
    HasDerivAt (coreGrowthPrimitive k) (2 / Real.cosh z + 24 * ((1 / 10000) / k)) z := by sorry
Source
https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/CoreGrowthBudget.lean#L18-L24

View graph