Actual residual tail estimates after the single final factorial split.
The actual finite residual tail inherits the geometric-series word bound.
theorem
EulerPacketCylinderField.PrefixFields.tailSum_bound_of_grades
{P T : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P T (N + 1) a)
(C : CoefficientData P T O)
(hT : 0 < T)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector N ⋯) Ct)
(pressure : Field P T (pressureGradient (a N).highPressure))
(ha : a 0 = 0)
(q : ℕ)
(R κ B : ℝ)
(hR : 0 ≤ R)
(hκ : 0 ≤ κ)
(hB : 0 ≤ B)
(hsmall : κ * B ≤ 1 / 2)
(hgrade :
∀ (n : ℕ) (hn : N + 1 ≤ n),
n ≤ 2 * N + 2 → (F.tailGradeField C hT Ct hCt pressure ha n hn).WordBound q R (B ^ (n + 1)) 0)
:
theorem
EulerPacketCylinderField.ProfileRegularity.tail_grade_coarse_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hN : 1 ≤ N)
(hR : 1 ≤ R)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(ha : a 0 = 0)
(hb : (a 1).mean = 0)
(n : ℕ)
(hn : N + 1 ≤ n)
(hn' : n ≤ 2 * N + 2)
:
(tailGradeField hT G C ha n hn).WordBound 6 (4 * R) (EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ^ (n + 1))
0
theorem
EulerPacketCylinderField.ProfileRegularity.tail_sum_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hN : 1 ≤ N)
(hR : 1 ≤ R)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(ha : a 0 = 0)
(hb : (a 1).mean = 0)
(κ : ℝ)
(hκ : 0 ≤ κ)
(hsmall : κ * EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ 1 / 2)
:
(tailSumField hT G C ha κ).WordBound 6 (4 * R)
(2 * EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N * (κ * EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N) ^ (N + 1))
0
theorem
EulerPacketCylinderField.ProfileRegularity.normalized_tail_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hN : 1 ≤ N)
(hR : 1 ≤ R)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(ha : a 0 = 0)
(hb : (a 1).mean = 0)
(k X : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(hcoef : BC.multiplierCost ≤ k ^ (1 / 100))
(hX : 6 ≤ X)
(hNX : X - 1 ≤ ↑N)
: