A single coefficient cost bounds every elementary nonlinear packet term.

structure EulerPacketCylinderField.CoefficientBudget {P T : ℝ} {O : EulerPacketProfileRecursion.Operators} (C : CoefficientData P T O) : Type

Coefficient budget data, collecting Rc, amplitude, Rc_nonneg, amplitude_nonneg, inverse_bound, strain_bound and their compatibility conditions.

• Rc : ℝ

  Rc of CoefficientBudget, of type ℝ.

• amplitude : ℝ

  Amplitude of CoefficientBudget, of type ℝ.

• Rc_nonneg : 0 ≤ self.Rc
• amplitude_nonneg : 0 ≤ self.amplitude
• inverse_bound (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath C.inverse.path) a‖ ≤ self.amplitude * EulerGevrey.majorant self.Rc 0 n
• strain_bound (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath C.strain.path) a‖ ≤ self.amplitude * EulerGevrey.majorant self.Rc 0 n
• normal_bound (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath C.normal.path) a‖ ≤ self.amplitude * EulerGevrey.majorant self.Rc 0 n

def EulerPacketCylinderField.CoefficientBudget.multiplierCost {P T : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : ℝ

Multiplier cost, given by 3*sobolevCoefficientAmplitude (Fin 4) 6 B.Rc B.amplitude.

Equations

• B.multiplierCost = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 B.Rc B.amplitude

noncomputable def EulerPacketCylinderField.CoefficientBudget.slowCost {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : ℝ

Slow cost, given by 9*productBlockConstant P*B.multiplierCost.

Equations

• B.slowCost = 9 * EulerCylinderPathProduct.productBlockConstant P * B.multiplierCost

noncomputable def EulerPacketCylinderField.CoefficientBudget.fastCost {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : ℝ

Fast cost, given by 3*productBlockConstant P*B.multiplierCost.

Equations

• B.fastCost = 3 * EulerCylinderPathProduct.productBlockConstant P * B.multiplierCost

def EulerPacketCylinderField.CoefficientBudget.linearCost {P T : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : ℝ

Linear cost, given by 1+B.multiplierCost.

Equations

• B.linearCost = 1 + B.multiplierCost

noncomputable def EulerPacketCylinderField.CoefficientBudget.termCost {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : ℝ

Term cost, given by 2*(1+B.multiplierCost+B.slowCost).

Equations

• B.termCost = 2 * (1 + B.multiplierCost + B.slowCost)

theorem EulerPacketCylinderField.CoefficientBudget.multiplierCost_nonneg {P T : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 0 ≤ B.multiplierCost

theorem EulerPacketCylinderField.CoefficientBudget.slowCost_nonneg {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 0 ≤ B.slowCost

theorem EulerPacketCylinderField.CoefficientBudget.fastCost_nonneg {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 0 ≤ B.fastCost

theorem EulerPacketCylinderField.CoefficientBudget.fastCost_le_slowCost {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : B.fastCost ≤ B.slowCost

theorem EulerPacketCylinderField.CoefficientBudget.linearCost_nonneg {P T : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 0 ≤ B.linearCost

theorem EulerPacketCylinderField.CoefficientBudget.termCost_nonneg {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 0 ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.one_le_termCost {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 1 ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.twice_slowCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 2 * B.slowCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.twice_fastCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 2 * B.fastCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.twice_linearCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 2 * B.linearCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.twice_multiplierCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : 2 * B.multiplierCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.slow_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (H : SpatialJetField P T K) (hT : 0 ≤ T) (g h b : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {R : ℝ} {d e : ℕ} (hG : (G.field.normalized hT g hg).WordBound 6 R 1 d) (hH : (H.field.normalized hT h hh).WordBound 6 R 1 e) (hR : 0 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) B.Rc ≤ R) (hp : ∀ (t : ↑(Set.Icc 0 T)), g t * h t ≤ b t) : ((SpatialJetField.slowAdvection C.inverse G H).normalized hT b hb).WordBound 6 R B.slowCost (d + e + 1)

theorem EulerPacketCylinderField.CoefficientBudget.fast_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (H : SpatialJetField P T K) (hT : 0 ≤ T) (g h b : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {R : ℝ} {d e : ℕ} (hG : (G.field.normalized hT g hg).WordBound 6 R 1 d) (hH : (H.field.normalized hT h hh).WordBound 6 R 1 e) (hR : 0 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) B.Rc ≤ R) (hp : ∀ (t : ↑(Set.Icc 0 T)), g t * h t ≤ b t) : ((SpatialJetField.fastAdvection C.normal G H).normalized hT b hb).WordBound 6 R B.fastCost (d + e + 1)