Actual mean and high forcing estimates at one fixed radius, uniform in the packet grade.
theorem
EulerPacketCylinderField.PrefixBound.meanForce_bound
{P T : ℝ}
[Fact (0 < P)]
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{F : PrefixFields P T p a}
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(hp : 2 ≤ p)
(hT : 0 < T)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct)
(pressure : Field P T (pressureGradient (a (p - 1)).highPressure))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(BF : PrefixBound F ⋯ S R)
(BC : CoefficientBudget C)
(hCtBound : (Ct.normalized ⋯ (S.high (p - 1)) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift (p - 1)))
(hPressureBound :
(pressure.normalized ⋯ (S.high (p - 1)) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift (p - 1)))
(hR : 1 ≤ R)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(hcost : BC.termCost ≤ R)
(hc : (a 0).corrector = 0)
(hB₁ : (a 1).mean = 0)
(hA :
∀ i < p,
∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0)
(hB :
∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0))
:
((F.meanForce C ⋯ hT Ct hCt pressure).normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1
(EulerPacketShiftArithmetic.meanForceShift p)
theorem
EulerPacketCylinderField.PrefixBound.highForce_bound
{P T : ℝ}
[Fact (0 < P)]
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{F : PrefixFields P T p a}
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(hp : 2 ≤ p)
(hT : 0 < T)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct)
(pressure : Field P T (pressureGradient (a (p - 1)).highPressure))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(BF : PrefixBound F ⋯ S R)
(BC : CoefficientBudget C)
(hCtBound : (Ct.normalized ⋯ (S.high (p - 1)) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift (p - 1)))
(hPressureBound :
(pressure.normalized ⋯ (S.high (p - 1)) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift (p - 1)))
(hR : 1 ≤ R)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(hcost : BC.termCost ≤ R)
(hc : (a 0).corrector = 0)
(hB₁ : (a 1).mean = 0)
(hA :
∀ i < p,
∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0)
(hB :
∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0))
(newMean : Field P T (EulerPacketProfileRecursion.meanResult O p a).1)
(hnew : (newMean.normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p))
:
((F.highForce C hp hT Ct hCt pressure newMean).normalized ⋯ (S.high p) ⋯).WordBound 6 R 1
(EulerPacketShiftArithmetic.highForceShift p)