Quantitative bounds for the literal finite approximate velocity and its time derivative.
theorem
EulerPacketCylinderField.ProfileRegularity.velocity_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 : ℝ}
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(hN : 1 ≤ N)
(C : ℝ)
(hC : 1 ≤ C)
(κ : ℝ)
(hκ : 0 ≤ κ)
(hsmall : κ * EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ 1 / 2)
:
(velocityField hT G κ).WordBound 6 (4 * R)
(κ * fixedVelocityGradeCost R S.H0 1 + κ ^ 2 * fixedVelocityGradeCost R S.H0 2 + 2 * EulerPacketCoarseMajorant.tailBase R S.H0 C N * (κ * EulerPacketCoarseMajorant.tailBase R S.H0 C N) ^ 3)
0
theorem
EulerPacketCylinderField.ProfileRegularity.velocityDerivative_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 : ℝ}
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(hN : 1 ≤ N)
(C : ℝ)
(hC : 1 ≤ C)
(κ : ℝ)
(hκ : 0 ≤ κ)
(hsmall : κ * EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ 1 / 2)
:
(velocityDerivativeField hT G κ).WordBound 6 (4 * R)
(κ * fixedVelocityGradeCost R S.H0 1 + κ ^ 2 * fixedVelocityGradeCost R S.H0 2 + 2 * EulerPacketCoarseMajorant.tailBase R S.H0 C N * (κ * EulerPacketCoarseMajorant.tailBase R S.H0 C N) ^ 3)
0