A uniform variational budget on power-height exit intervals

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$.

Write $r(m,v)=\sqrt{(m-1)^2+v^2}$ and define

$$g(R,v)=\sqrt{R^2-v^2},\qquad d(R,u,v,w)=g(R,v)+u(v+w-u),$$ $$f_R=\frac{-u(v+w-u)R-g(R,v)(u-w)^2/R}{d},$$ $$a_s=\frac{2g(R,v)-R^2+2vw-w^2+u^2}{2d},\qquad a_w=\frac{g(R,v)-2-u(v+w-u)}d.$$

The exit clock rate is $\omega(y)=1-m+u(v+w-u)$, and its field is $F_{\log}(y)=F(y)/\omega(y)$. Division and square roots have their total real-valued Lean meanings.

For $Y=(R,u,w)$ define $E_v(Y)=(f_R,a_su,a_ww)$, evaluated at $(R,u,v,w)$. The coordinate maps are $Q(m,u,v,w)=(r(m,v),u,w)$ and $Q_v^{-1}(R,u,w)=(1-g(R,v),u,v,w)$. For a curve $Y(s)$ set

$$M_i(Y,t)=\exp\int_0^t a_i(Y_0(s),Y_1(s),e^{-s},Y_2(s))\,ds \quad(i=s,w).$$

Let $\mathcal R_{\alpha,b,A,D}$ consist of the states satisfying

$$7/4\leq R\leq17/4,\quad |u|,|w|\leq1/100,\quad |u|+|w|\leq Ab,\quad |R-(2+2\alpha)|\leq Db.$$

Put

$$B(\alpha,b,A,D,T)=[10(\alpha+Db)+100(Ab)^2]T+100Ab+5,$$ $$L(\eta,\alpha,J)=\log(1/\eta)+J\log(1/\alpha).$$

For real variables $p,s,a,b,c$, set

$$K=a^2+b^2+c^2-2(ab+bc+ca),\qquad S=p^2+s^2,\qquad C=S+K.$$

The shear components and wall rates are

$$P=Kp-2a^2+b^2+c^2+ab-2bc+ac,$$ $$Q=Ks+\sqrt{3}(-b^2+c^2+ab-ac),$$ $$r_1=-S+2p,\qquad r_2=-S-p+\sqrt{3}s,\qquad r_3=-S-p-\sqrt{3}s.$$

These functions define the normalized vacuum Bianchi IX vector field $(P,Q,r_1a,r_2b,r_3c)$. 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$.

For $x=(p,s,a,b,c)$, put

$$\psi(p,z)=\frac{\sqrt3\,z}{1+p},\qquad \Pi(x)=(\psi(p,s),\psi(p,a),\psi(p,b),\psi(p,c)).$$

For $y=(m,u,v,w)$, set $D(y)=3+m^2+K(u,v,w)$ and

$$\Xi_A(y)=\left(A-1,\frac{Am}{\sqrt3},\frac{Au}{\sqrt3}, \frac{Av}{\sqrt3},\frac{Aw}{\sqrt3}\right),\qquad \Xi(y)=\Xi_{6/D(y)}(y).$$

Write $N(x)=(P,Q,r_1a,r_2b,r_3c)$ for the normalized vector field and $\mathcal C(x)=C(p,s,a,b,c)$ for its constraint.

The normalized and projective state spaces are $\mathbb R^5$ and $\mathbb R^4$ with their finite-product norms. The maps $\Pi,\Xi,D,F$ act on these state spaces.

The projective vector field in normalized time is

$$G(y)=\frac6{D(y)}F(y).$$

Write $X=\mathbb R^5$, $Y=\mathbb R^4$, and let $\alpha_{x,t_0}$ be the maximal solution of $\alpha'=N(\alpha)$ with initial value $x$ at $t_0$ and domain $I_{\max}(x,t_0)$. Put

$$J_{x,t_0}(t)=d_x\alpha_{x,t_0}(t),\qquad \Psi_{t_0}(y,t)=\Pi(\alpha_{\Xi(y),t_0}(t)),$$ $$\mathcal J_{y,t_0}(t)=d\Pi_{\alpha_{\Xi(y),t_0}(t)} \circ J_{\Xi(y),t_0}(t)\circ d\Xi_y.$$

For $Y=(k,u,w)\in\mathbb R^3$, define

$$e_-(Y)=(1-\sqrt{k^2-1},u,1,w),\quad x_Y=\Xi(e_-(Y)),\quad \beta_Y(t)=\Psi_0(e_-(Y),t),\quad g(x)=(\Pi(x))_v.$$

For any real height $\eta$, put

$$H_{\eta,Y}=\{t>0:t\in I_{\max}(x_Y,0),\ g(\alpha_{x_Y,0}(t))=\eta\},$$ $$T_\eta(Y)=\inf H_{\eta,Y},\qquad P_\eta(Y)=\beta_Y(T_\eta(Y)).$$

The infimum uses the total real-order convention. Let $\operatorname{TailValid}_\eta(Y)$ mean that $T_\eta(Y)$ is the least element of $H_{\eta,Y}$, and, writing $T=T_\eta(Y)$, that

$$t\in I_{\max}(x_Y,0),\quad 1+(\alpha_{x_Y,0}(t))_0>0 \quad(0\leq t\leq T),$$ $$g(\alpha_{x_Y,0}(t))>\eta\quad(0\leq t<T),$$ $$dg_{\alpha_{x_Y,0}(t)}N(\alpha_{x_Y,0}(t))<0,\quad |(\Pi(\alpha_{x_Y,0}(t)))_w|<1/2\quad(0\leq t\leq T).$$

All vector and operator norms use the finite-product supremum norms.

For $y\in\mathbb R^4$, put $x_y=\Xi(y)$,

$$T_+(y)=\inf\{t>0:t\in I_{\max}(x_y,0),\ (\Psi_0(y,t))_v=1\}, \qquad P_+(y)=\Psi_0(y,T_+(y)).$$

Let $V_+(y)$ mean that this infimum is a least element, the full interval $[0,T_+(y)]$ lies in the maximal domain with $1+(\alpha_{x_y,0}(t))_0>0$, the active wall is below one before the endpoint, and its normalized-time derivative is strictly positive throughout the interval. The infimum has its total real-order meaning.

For $y=(m,u,v,w)$ define the cyclic chart by

$$H(y)=(m+1)^2+K(u,v,w),\qquad \mathcal A(y)=(1-4(m+1)/H,4v/H,4w/H,4u/H).$$

Its normalized symmetry is

$$A(p,s,a,b,c)=((-p+\sqrt3s)/2,(-\sqrt3p-s)/2,b,c,a).$$

Put $z_h(Y)=\mathcal A(P_h(Y))$ and

$$\mathcal T(h,Y)=T_h(Y)+T_+(z_h(Y)),\qquad \mathcal P(h,Y)=P_+(z_h(Y)),\qquad x_Y^c=A\Xi(e_-(Y)).$$

Write $r(m,v)=\sqrt{(m-1)^2+v^2}$ and $g_*(x)=(\Pi(x))_v$.

Let $\beta(Y,t)=\Psi_0(e_-(Y),t)$ and $c(Y,t)=-\log\beta(Y,t)_2$. Call $(Y,t)$ regular when $Y_0>1$, $D(e_-(Y))>0$, the normalized flow exists at $t$ with positive chart clock, and $\beta_2>0$, $\beta_0<1$, $\omega(\beta)>0$. For an interval $I$, let $\tau_I(Y,s)$ be a solution in $I$ of $c(Y,t)=s$, selected by choice, or zero if there is none. Define

$$X_I(Y,s)=Q(\beta(Y,\tau_I(Y,s))),\qquad \ell_i(Y,s)=\int_0^s a_i(X_I(Y,r)_0,X_I(Y,r)_1,e^{-r},X_I(Y,r)_2)\,dr.$$

Here $i=0,1$ denotes $a_s,a_w$ respectively. Write

$$V(\alpha,b,A,D,T)=2B(\alpha,b,A,D,T)+2048(1+AbT).$$

The tail box is $7/4\leq R\leq17/4$, $|u|,|w|\leq1/100$, $0\leq v\leq1$. Write $G_R=\nabla_{R,u,w}f_R$, $G_s=\nabla_{R,u,w}a_s$, $G_w=\nabla_{R,u,w}a_w$ for their explicit algebraic gradients there. For $0<\eta\leq1$ and $J\geq1$ there exist $A\geq2$, $B_*\geq0$, $\varepsilon>0$ such that the following holds. Let $0<\alpha\leq1$, $0<b\leq\varepsilon\alpha^J$, $0\leq T\leq L(\eta,\alpha,J)$. A solution $Y'=E_{e^{-s}}(Y)$ on $[0,T]$ with $Y(0)_0=2+2\alpha$ and $|Y(0)_1|+|Y(0)_2|\leq b$ remains in $\mathcal R_{\alpha,b,A,80A}$, and $V(\alpha,b,A,80A,T)\leq B_*$.

import Definitions.Def_BianchiIX_TerminalConnectionData
import Definitions.Def_BianchiIX_TerminalConeData
import Mathlib.Analysis.ODE.Gronwall
import Mathlib.Data.Matrix.Mul
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.FunProp
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Topology.Order.ProjIcc
import Mathlib.LinearAlgebra.Matrix.ToLin
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.SpecialFunctions.Arsinh
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic.FinCases
import Mathlib.Analysis.Calculus.Deriv.Inv
import Mathlib.Tactic.LinearCombination
import Mathlib.Analysis.SpecialFunctions.Arcosh
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
import Mathlib.Analysis.Calculus.Deriv.MeanValue
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.Analysis.ODE.ExistUnique
import Mathlib.Analysis.Calculus.FDeriv.Partial
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Mathlib.Topology.Order.Compact
import Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
import Mathlib.Topology.Order.IntermediateValue
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic.Positivity

noncomputable section
open BianchiIX
open Set

theorem BianchiIX.exists_exitTail_uniform_variation_budget {η : ℝ} (hη : 0 < η ∧ η ≤ 1)
    {J : ℕ} (hJ : 1 ≤ J) :
    ∃ A ≥ (2 : ℝ), ∃ B ≥ (0 : ℝ), ∃ ε > (0 : ℝ),
      ∀ (α b T : ℝ) (Y : ℝ → ExitTailState),
      (0 < α ∧ α ≤ 1) → 0 < b → b ≤ ε * α ^ J →
      (0 ≤ T ∧ T ≤ exitTailLength η α J) → Y 0 0 = 2 + 2 * α →
      |Y 0 1| + |Y 0 2| ≤ b →
      (∀ s ∈ Icc 0 T, HasDerivAt Y (exitTailField (Real.exp (-s)) (Y s)) s) →
      (∀ s ∈ Icc 0 T, exitTailRegion α b A (80 * A) (Y s)) ∧
        exitTailVariationBudget α b A (80 * A) T ≤ B := by sorry