Uniform finite-order product and pressure constants from bounds on the actual coefficient derivative tree. At each fixed Sobolev order these costs are finite polynomials in the coefficient bound and inverse coercivity.

def EulerCoefficientJetPressureBounds.productCost (B : ℝ) : ℕ → ℝ

Product cost as an element of ℕ → ℝ | 0 => B | q+1 => B+8*productCost B q.

Equations

• EulerCoefficientJetPressureBounds.productCost B 0 = B
• EulerCoefficientJetPressureBounds.productCost B q.succ = B + 8 * EulerCoefficientJetPressureBounds.productCost B q

def EulerCoefficientJetPressureBounds.pressureCost (c B : ℝ) : ℕ → ℝ

Pressure cost as an element of ℕ → ℝ | 0 => c⁻¹ | q+1 => c⁻¹+4*(pressureCost c B q*(1+productCost B q*pressureCost c B q)).

Equations

• One or more equations did not get rendered due to their size.
• EulerCoefficientJetPressureBounds.pressureCost c B 0 = c⁻¹

theorem EulerCoefficientJetPressureBounds.productCost_nonneg (B : ℝ) (hB : 0 ≤ B) (q : ℕ) : 0 ≤ productCost B q

theorem EulerCoefficientJetPressureBounds.pressureCost_nonneg (c B : ℝ) (hc : 0 < c) (hB : 0 ≤ B) (q : ℕ) : 0 ≤ pressureCost c B q

def EulerCoefficientJetPressureBounds.TreeBound {P : ℝ} {dirs : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} (K : EulerSpatialSobolevInverse.CoefficientJet P dirs s A) (B : ℝ) : Prop

Tree bound as an element of Prop.

Equations

• One or more equations did not get rendered due to their size.
• EulerCoefficientJetPressureBounds.TreeBound (EulerSpatialSobolevInverse.CoefficientJet.zero A) B = (↑A.bound ≤ B)

theorem EulerCoefficientJetPressureBounds.TreeBound.root {P : ℝ} {dirs : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} {K : EulerSpatialSobolevInverse.CoefficientJet P dirs s A} {B : ℝ} (hK : TreeBound K B) : ↑A.bound ≤ B

theorem EulerCoefficientJetPressureBounds.treeBound_of_levels {P : ℝ} {dirs : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} (K : EulerSpatialSobolevInverse.CoefficientJet P dirs s A) (B : ℝ) (hb : ∀ n ≤ s, EulerJetProductBounds.boundLevel P K n ≤ B) : TreeBound K B

theorem EulerCoefficientJetPressureBounds.TreeBound.truncate {P : ℝ} {dirs : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} {K : EulerSpatialSobolevInverse.CoefficientJet P dirs (s + 1) A} {B : ℝ} (hK : TreeBound K B) : TreeBound K.truncate B

theorem EulerCoefficientJetPressureBounds.TreeBound.restrict {P : ℝ} {dirs : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} {K : EulerSpatialSobolevInverse.CoefficientJet P dirs s A} {B : ℝ} (hK : TreeBound K B) (q : ℕ) (hq : q ≤ s) : TreeBound (EulerH6Pressure.CoefficientJet.restrict K q hq) B

theorem EulerCoefficientJetPressureBounds.TreeBound.productConstant_le {P : ℝ} {dirs : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} {K : EulerSpatialSobolevInverse.CoefficientJet P dirs s A} {B : ℝ} (hK : TreeBound K B) : K.productConstant ≤ productCost B s

theorem EulerCoefficientJetPressureBounds.TreeBound.pressureConstant_le {P : ℝ} {dirs : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient P} {K : EulerSpatialSobolevInverse.CoefficientJet P dirs s A} {B : ℝ} (hK : TreeBound K B) (c : ℝ) (hc : 0 < c) (hB : 0 ≤ B) : K.pressureConstant c ≤ pressureCost c B s