The literal packet differs from its primary wave by a quadratic-frequency remainder.
theorem
EulerPacketCylinderField.ProfileRegularity.assembledVelocity_one
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hN : 1 ≤ N)
(ha : a 0 = 0)
(hb : (a 1).mean = 0)
:
noncomputable def
EulerPacketCylinderField.ProfileRegularity.primaryRemainderField
{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))
(hN : 1 ≤ N)
(ha : a 0 = 0)
(hb : (a 1).mean = 0)
(κ : ℝ)
:
Field P T (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N a) - κ • (a 1).high)
Primary remainder field as an element of Field P T (fieldSum (N+1) κ (assembledVelocity N a)-κ • (a 1).high).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.ProfileRegularity.primaryRemainder_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)
(hb : (a 1).mean = 0)
(hN : 1 ≤ N)
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
(primaryRemainderField hT G hN ha hb k⁻¹).WordBound 6 (4 * R) ((fixedVelocityGradeCost R S.H0 2 + 2) / k ^ 2) 0
theorem
EulerPacketCylinderField.ProfileRegularity.normalizedRemainder_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)
(hb : (a 1).mean = 0)
(hN : 1 ≤ N)
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
((C.inverse.multiply (primaryRemainderField hT G hN ha hb k⁻¹)).smul k).WordBound 6 (4 * R)
(BC.multiplierCost * (fixedVelocityGradeCost R S.H0 2 + 2) / k) 0