Related estimates used together by the same construction modules.

Exact triangle inequalities for the actual finite Hilbert forcing families.

theorem EulerWeightedForcingAlgebra.familyNorm_add_le {β : Type u_2} {H : Type u_3} [Fintype β] [NormedAddCommGroup H] (v w : β → H) : EulerFiniteMetricEnergy.familyNorm (v + w) ≤ EulerFiniteMetricEnergy.familyNorm v + EulerFiniteMetricEnergy.familyNorm w

Triangle inequality for the root-of-sum-of-squares norm of actual finite Hilbert families.

theorem EulerWeightedForcingAlgebra.familyNorm_neg {β : Type u_2} {H : Type u_3} [Fintype β] [NormedAddCommGroup H] (v : β → H) : EulerFiniteMetricEnergy.familyNorm (-v) = EulerFiniteMetricEnergy.familyNorm v

Signs do not change the genuine Hilbert family norm.

theorem EulerWeightedForcingAlgebra.weightedForcingSum_add_le {α : Type u_1} {β : Type u_2} {H : Type u_3} [Fintype α] [Fintype β] [NormedAddCommGroup H] (ρ : ℝ) (hρ : 0 < ρ) (order : α → ℕ) (f g : α → β → H) : EulerWeightedCylinderEnergy.weightedForcingSum ρ order (f + g) ≤ EulerWeightedCylinderEnergy.weightedForcingSum ρ order f + EulerWeightedCylinderEnergy.weightedForcingSum ρ order g

Weighted forcing is subadditive without any cardinality factor.

theorem EulerWeightedForcingAlgebra.weightedForcingSum_neg {α : Type u_1} {β : Type u_2} {H : Type u_3} [Fintype α] [Fintype β] [NormedAddCommGroup H] (ρ : ℝ) (order : α → ℕ) (f : α → β → H) : EulerWeightedCylinderEnergy.weightedForcingSum ρ order (-f) = EulerWeightedCylinderEnergy.weightedForcingSum ρ order f

Weighted forcing is invariant under the overall sign.

theorem EulerWeightedForcingAlgebra.weightedForcingSum_sum_le {α : Type u_1} {β : Type u_2} {H : Type u_3} [Fintype α] [Fintype β] [NormedAddCommGroup H] {ι : Type u_4} (ρ : ℝ) (hρ : 0 < ρ) (order : α → ℕ) (S : Finset ι) (f : ι → α → β → H) : EulerWeightedCylinderEnergy.weightedForcingSum ρ order (∑ i ∈ S, f i) ≤ ∑ i ∈ S, EulerWeightedCylinderEnergy.weightedForcingSum ρ order (f i)

The forcing norm of a sum is controlled by the sum of the norms of its actual terms.

Complete finite-cutoff pressure commutator bounds for both actual source components.

theorem EulerGevreyPressureEnergy.coefficientBlock_mono (period : ℝ) {s p q : ℕ} (hpq : p ≤ q) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (n : ℕ) : EulerH6Pressure.coefficientBlock period K p n ≤ EulerH6Pressure.coefficientBlock period K q n

Monotonicity of the actual coefficient derivative blocks in their fixed Sobolev index.

theorem EulerGevreyPressureEnergy.nonlinear_externalPressure_bound_all (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (N : ℕ) (hN : N + 6 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (EulerH6Pressure.CoefficientJet.restrict K 6 hs).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : externalPressureNorm period K N ρ (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v) ≤ 32 * Rc * M * EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

The actual nonlinear external pressure commutator bound includes the zero-cutoff case.

theorem EulerGevreyPressureEnergy.nonlinear_basePressure_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (N : ℕ) (hN : N + 6 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (EulerH6Pressure.CoefficientJet.restrict K 5 ⋯).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : basePressureNorm period K0 N hN ρ (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v) ≤ 448 * EulerBasePressureCommutator.baseCoefficientSum period K0 * (8 * M * (5460 * EulerH6Nonlinear.lowerProductConstant period 3)) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v

Actual base transport-pressure commutators are bounded by the product of the two velocity energies at the same cutoff.

theorem EulerGevreyPressureEnergy.source_pressure_commutators (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (N : ℕ) (hN : N + 6 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (EulerH6Pressure.CoefficientJet.restrict K 6 ⋯).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (f : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : externalPressureNorm period K N ρ ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) f) + basePressureNorm period K0 N hN ρ ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) f) ≤ 2 * M * (EulerSobolevGevreyOperators.weightedCoefficient period K 6 N ρ + 448 * EulerBasePressureCommutator.baseCoefficientSum period K0) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f

Both actual commutators of the order-zero pressure are controlled by the unshifted source norm.