One-step contraction of the scale-invariant quantity #
The one-step contraction of the scale-invariant quantity in the iteration of the CKN manuscript's iteration proposition (with its convention for κ, η, ε_* and the force coefficient C₂₉), stated for abstract real numbers.
theorem
CIV.theta_contraction_of_beta_small
{C₂₇ C₂₈ T Tnext b L : ℝ}
(hC₂₇ : 0 < C₂₇)
(hC₂₈ : 0 < C₂₈)
(hT : 0 ≤ T)
(hL : 0 ≤ L)
(hb : 0 ≤ b)
(hbsmall : b ≤ CKN.iterationEpsilonStar C₂₇)
(hdec :
Tnext ≤ C₂₇ * CKN.iterationKappa C₂₇ ^ (2 / 3) * T + C₂₇ * CKN.iterationKappa C₂₇ ^ (-5) * (b ^ (1 / 2) + b) * T + C₂₈ * CKN.iterationKappa C₂₇ ^ (-1 / 2) * T ^ (1 / 2) * L ^ (1 / 2) + C₂₈ * CKN.iterationKappa C₂₇ ^ (-3) * L)
: