Same-radius estimates for the fifteen actual forcing families, before and after angular projection.

Bounds on the actual masked slow and fast products, with zero terms charged no shifts.

theorem EulerPacketCylinderField.PrefixBound.maskedSlow_bound {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T p a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (BF : PrefixBound F hT S R) {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (l r : KnownPiece) (i j n : ℕ) {raw : EulerPacketProfileRecursion.VectorField} (W : Field P T raw) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = if i + j = n then ((EulerPacketPointJets.slowAdvection (O.inverseFrame (↑t, x, θ))) (l.jet O p a (↑t, x, θ) i)) (r.jet O p a (↑t, x, θ) j) else 0) (b : C(↑(Set.Icc 0 T), ℝ)) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) (hR : 0 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (hprofile : i + j = n → l.active p i → r.active p j → ∀ (t : ↑(Set.Icc 0 T)), (l.profile S i) t * (r.profile S j) t ≤ b t) : (W.normalized hT b hb).WordBound 6 R BC.slowCost (if i + j = n ∧ l.active p i ∧ r.active p j then l.shift i + r.shift j + 1 else 0)

theorem EulerPacketCylinderField.PrefixBound.maskedFast_bound {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T p a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (BF : PrefixBound F hT S R) {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (l r : KnownPiece) (i j n : ℕ) {raw : EulerPacketProfileRecursion.VectorField} (W : Field P T raw) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = if i + j = n then ((EulerPacketPointJets.fastAdvection (O.normal (↑t, x, θ))) (l.jet O p a (↑t, x, θ) i)) (r.jet O p a (↑t, x, θ) j) else 0) (b : C(↑(Set.Icc 0 T), ℝ)) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) (hR : 0 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (hprofile : i + j = n → l.active p i → r.active p j → ∀ (t : ↑(Set.Icc 0 T)), (l.profile S i) t * (r.profile S j) t ≤ b t) : (W.normalized hT b hb).WordBound 6 R BC.fastCost (if i + j = n ∧ l.active p i ∧ r.active p j then l.shift i + r.shift j + 1 else 0)

Every nonzero known summand fits strictly below its target forcing shift.

def EulerPacketCylinderField.KnownTerm.budgetShift (k : KnownTerm) (p i j : ℕ) : ℕ

Budget shift as an element of ℕ.

Equations

• One or more equations did not get rendered due to their size.
• EulerPacketCylinderField.KnownTerm.previousLinear.budgetShift p i j = if i = 0 ∧ j = 0 then EulerPacketShiftArithmetic.highShift (p - 1) else 0
• EulerPacketCylinderField.KnownTerm.previousPressure.budgetShift p i j = if i = 0 ∧ j = 0 then EulerPacketShiftArithmetic.highShift (p - 1) else 0
• (EulerPacketCylinderField.KnownTerm.slow l r).budgetShift p i j = if i + j = p ∧ l.active p i ∧ r.active p j then l.shift i + r.shift j + 1 else 0

theorem EulerPacketCylinderField.KnownTerm.budgetShift_lt_mean (k : KnownTerm) (p i j : ℕ) (hp : 2 ≤ p) (hk : k.zeroMean = false) : k.budgetShift p i j < EulerPacketShiftArithmetic.meanForceShift p

theorem EulerPacketCylinderField.KnownTerm.budgetShift_lt_high (k : KnownTerm) (p i j : ℕ) (hp : 2 ≤ p) : k.budgetShift p i j < EulerPacketShiftArithmetic.highForceShift p

The time-profile inequalities for every surviving term of the mean and high forces.

def EulerPacketCylinderField.KnownTerm.ProfileFits {K : Type u_1} [TopologicalSpace K] (k : KnownTerm) (S : EulerPacketTimeProfile.Scales K) (p i j : ℕ) (b : C(K, ℝ)) : Prop

Profile fits as an element of Prop.

Equations

• One or more equations did not get rendered due to their size.
• EulerPacketCylinderField.KnownTerm.previousLinear.ProfileFits S p i j b = ∀ (t : K), (S.high (p - 1)) t ≤ b t
• EulerPacketCylinderField.KnownTerm.previousPressure.ProfileFits S p i j b = ∀ (t : K), (S.high (p - 1)) t ≤ b t
• (EulerPacketCylinderField.KnownTerm.slow l r).ProfileFits S p i j b = (i + j = p → l.active p i → r.active p j → ∀ (t : K), (l.profile S i) t * (r.profile S j) t ≤ b t)

theorem EulerPacketCylinderField.KnownTerm.mean_profile_fits {K : Type u_1} [TopologicalSpace K] (k : KnownTerm) (S : EulerPacketTimeProfile.Scales K) (p i j : ℕ) (hp : 2 ≤ p) (hk : k.zeroMean = false) : k.ProfileFits S p i j (S.mean p)

theorem EulerPacketCylinderField.KnownTerm.high_profile_fits {K : Type u_1} [TopologicalSpace K] (k : KnownTerm) (S : EulerPacketTimeProfile.Scales K) (p i j : ℕ) (hk : k.meanOnly = false) : k.ProfileFits S p i j (S.high p)

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

Amplitude as an element of ℝ.

Equations

• EulerPacketCylinderField.KnownTerm.previousLinear.amplitude B = B.linearCost
• EulerPacketCylinderField.KnownTerm.previousPressure.amplitude B = B.multiplierCost
• (EulerPacketCylinderField.KnownTerm.slow left right).amplitude B = B.slowCost
• k.amplitude B = B.fastCost

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

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

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

def EulerPacketCylinderField.KnownTerm.meanBudgetShift (k : KnownTerm) (p i j : ℕ) : ℕ

Mean budget shift, with branches according to k.zeroMean.

Equations

• k.meanBudgetShift p i j = if k.zeroMean = true then 0 else k.budgetShift p i j

theorem EulerPacketCylinderField.KnownTerm.meanBudgetShift_lt (k : KnownTerm) (p i j : ℕ) (hp : 2 ≤ p) : k.meanBudgetShift p i j < EulerPacketShiftArithmetic.meanForceShift p

theorem EulerPacketCylinderField.PrefixBound.raw_term_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 : 0 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (k : KnownTerm) (i j : ℕ) (b : C(↑(Set.Icc 0 T), ℝ)) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) (hprofile : k.ProfileFits S p i j b) : ((F.termField C ⋯ hT Ct hCt pressure k i j).normalized ⋯ b hb).WordBound 6 R (k.amplitude BC) (k.budgetShift p i j)

theorem EulerPacketCylinderField.PrefixBound.mean_term_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 : 0 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (k : KnownTerm) (i j : ℕ) : ((F.meanTermField C ⋯ hT Ct hCt pressure k i j).normalized ⋯ (S.mean p) ⋯).WordBound 6 R BC.termCost (k.meanBudgetShift p i j)

theorem EulerPacketCylinderField.PrefixBound.high_term_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 : 0 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (k : KnownTerm) (i j : ℕ) : ((F.highTermField C ⋯ hT Ct hCt pressure k i j).normalized ⋯ (S.high p) ⋯).WordBound 6 R BC.termCost (k.budgetShift p i j)