The connection projection denominator has a uniform quadratic upper bound

Proved

BianchiIX.connection_denom_upper

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

bianchi-ix-era-statisticsdynamical-systems

For $y=(m,u,v,w)\in\mathbb R^4$ , define

K(u,v,w)=u^2+v^2+w^2-2(uv+vw+wu),\qquad \kappa=u(v+w-u),

F_m=-v^2+w^2+u(v-w)-m\kappa,\qquad F_u=\tfrac12(1-m^2-(v-w)^2+u^2)u,

F_v=(m-1-\kappa)v,\qquad F_w=(-m-1-\kappa)w,\qquad F=(F_m,F_u,F_v,F_w),

and $E(m,v)=(m-1)^2+v^2$ .

Put $c=u(v+w-u)$ , $s(m,u,v,w)=m-1-c$ , $b(m,u,v,w)=(1-m^2-(v-w)^2+u^2)/2$ , $D(m,u,v,w)=3+m^2+K(u,v,w)$ , and $r(m,v)=\sqrt{(m-1)^2+v^2}$ .

Assume $\mu\geq4$ , $|m-\mu|\leq1/2$ , $0\leq u\leq1/10000$ , and $0\leq v,w\leq1$ . Then $D(-m,u,v,w)\leq2\mu^2$ .

Preamble

import Definitions.Def_BianchiIX_Algebra_Flow
import Definitions.Def_BianchiIX_Algebra_Coordinates
import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Calculus.Deriv.Add
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Analysis.Calculus.Deriv.Inv
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.LinearCombination

noncomputable section
open BianchiIX

Formal statement

theorem BianchiIX.connection_denom_upper {μ m u v w : ℝ} (hμ : 4 ≤ μ)
    (hm : |m - μ| ≤ 1 / 2) (hu : 0 ≤ u ∧ u ≤ 1 / 10000)
    (hv : 0 ≤ v ∧ v ≤ 1) (hw : 0 ≤ w ∧ w ≤ 1) :
    projectiveDenom (-m) u v w ≤ 2 * μ ^ 2 := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Algebra/ConnectionDomain.lean#L7-L22

View graph