Prove2Me

The strong logarithmic rate has uniformly bounded phase response

Proved
BianchiIX.connectionStrongClockPartials_bounds

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

bianchi-ix-era-statisticsdynamical-systems

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

K(u,v,w)=u2+v2+w2−2(uv+vw+wu),κ=u(v+w−u),K(u,v,w)=u^2+v^2+w^2-2(uv+vw+wu),\qquad \kappa=u(v+w-u), Fm=−v2+w2+u(v−w)−mκ,Fu=12(1−m2−(v−w)2+u2)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, Fv=(m−1−κ)v,Fw=(−m−1−κ)w,F=(Fm,Fu,Fv,Fw),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+v2E(m,v)=(m-1)^2+v^2.

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

Assume μ≥4\mu\geq4, ∣m−μ∣≤1/2|m-\mu|\leq1/2, 0≤u≤1/100000\leq u\leq1/10000, and 0≤v,w≤10\leq v,w\leq1.

For the positive reflected phase variable mm, put

n(a,b)=a2+b2,j(a,b)=1n(a,b)(n(a,b)+a),n(a,b)=\sqrt{a^2+b^2},\quad j(a,b)=\frac1{n(a,b)(n(a,b)+a)}, ϕ=n(m+1,v)+n(m−1,w)−m,h=m+1n(m+1,v)+m−1n(m−1,w)−1,\phi=n(m+1,v)+n(m-1,w)-m,\quad h=\frac{m+1}{n(m+1,v)}+\frac{m-1}{n(m-1,w)}-1, Q=mh+v2n(m+1,v)+w2n(m−1,w),k=j(m+1,v)−j(m−1,w).Q=mh+\frac{v^2}{n(m+1,v)}+\frac{w^2}{n(m-1,w)},\quad k=j(m+1,v)-j(m-1,w).

Write κ=u(v+w−u)\kappa=u(v+w-u), s=m−1−κs=m-1-\kappa, b=(1−m2−(v−w)2+u2)/2b=(1-m^2-(v-w)^2+u^2)/2, and

Mv=−v2n(m+1,v)h,Mw=−w2n(m−1,w)h.M_v=-\frac{v^2}{n(m+1,v)h},\qquad M_w=-\frac{w^2}{n(m-1,w)h}.

The four coordinate differential operators, in the order (ϕ,log⁡u,log⁡v,log⁡w)(\phi,\log u,\log v,\log w), are

L0=h−1∂m,L1=u∂u,L2=Mv∂m+v∂v,L3=Mw∂m+w∂w.L_0=h^{-1}\partial_m,\quad L_1=u\partial_u,\quad L_2=M_v\partial_m+v\partial_v,\quad L_3=M_w\partial_m+w\partial_w.

Subscripts ii below denote the rational expressions obtained by these rules, with total real-field division. On the regular positive-wall region they are the corresponding coordinate partial derivatives. Set

N=h(v−w)+(v+w−u)Q,R=h(v−w)+(v+w−u)(Q−s),N=h(v-w)+(v+w-u)Q,\quad R=h(v-w)+(v+w-u)(Q-s), A=−N/s,B=k/s,G=uA+(vw)2B,α=b/s,β=−1−2(1+κ)/s.A=-N/s,\quad B=k/s,\quad G=uA+(vw)^2B,\quad \alpha=b/s,\quad \beta=-1-2(1+\kappa)/s.

The coefficient matrix CC has rows (Gi)i(G_i)_i, (αi)i(\alpha_i)_i and (βi)i(\beta_i)_i.

∣α0∣≤32,∣α1∣≤32u,|\alpha_0|\leq32,\quad |\alpha_1|\leq32u, ∣α2∣≤32((v2+vw)/μ+uv),∣α3∣≤32((w2+vw)/μ+uw).|\alpha_2|\leq32((v^2+vw)/\mu+uv),\quad |\alpha_3|\leq32((w^2+vw)/\mu+uw).
Preamble
import Definitions.Def_BianchiIX_Algebra_Projective
import Definitions.Def_BianchiIX_Algebra_ConnectionBounds
import Definitions.Def_BianchiIX_Algebra_MatchingPhase
import Definitions.Def_BianchiIX_Analysis_MatchingPhaseWeighted
import Definitions.Def_BianchiIX_Analysis_ConnectionAmplitudeDifferential
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
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.Calculus.ImplicitContDiff
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.Analysis.SpecialFunctions.ExpDeriv

noncomputable section
open BianchiIX
Formal statement
theorem BianchiIX.connectionStrongClockPartials_bounds {μ 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) :
    |connectionStrongClockPartials m u v w 0| ≤ 32 ∧
    |connectionStrongClockPartials m u v w 1| ≤ 32 * u ∧
    |connectionStrongClockPartials m u v w 2| ≤ 32 * ((v ^ 2 + v * w) / μ + u * v) ∧
    |connectionStrongClockPartials m u v w 3| ≤ 32 * ((w ^ 2 + v * w) / μ + u * w) := by sorry
Source
https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/ConnectionAmplitudeBounds.lean#L103-L177

View graph