Actual lower-base Sobolev bounds for the transport pressure, without an external derivative loss.

The additional H⁵ cylinder algebra estimate needed for the base transport commutator.

theorem EulerH5CylinderAlgebra.product_tensor_term_le (period : ℝ) [Fact (0 < period)] {q n j : ℕ} (hq : 5 ≤ q) (hn : n ≤ q) (hj : j ≤ n) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ k ≤ q, ∀ (w : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ q, ∀ (w : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖iteratedFDeriv ℝ j (EulerCylinderSobolev.euclideanLift period f x) 0‖ * ‖iteratedFDeriv ℝ (n - j) (EulerCylinderSobolev.euclideanLift period g x) 0‖ ≤ EulerGeneralCylinderAlgebra.lowDerivativeConstant period q * EulerGeneralCylinderAlgebra.productEnvelope period q f g x

In every Leibniz term through order q≥5, one factor has three spare derivatives.

theorem EulerH5CylinderAlgebra.product_word_pointwise_le (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 5 ≤ q) (hn : n ≤ q) (w : Fin n → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerCylinderSobolev.iteratedFieldDerivative period w (f * g) x‖ ≤ 2 ^ q * EulerGeneralCylinderAlgebra.lowDerivativeConstant period q * EulerGeneralCylinderAlgebra.productEnvelope period q f g x

Every actual product derivative is bounded pointwise by the low/high Sobolev envelope.

theorem EulerH5CylinderAlgebra.product_word_memLp (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 5 ≤ q) (hn : n ≤ q) (w : Fin n → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (f * g)) 2 (EulerLiftedGradientSpace.liftMeasure period)

Every derivative word through order q of the actual product belongs to L².

theorem EulerH5CylinderAlgebra.product_word_L2_le (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 5 ≤ q) (hn : n ≤ q) (w : Fin n → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative period w (f * g)) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ 2 ^ q * EulerGeneralCylinderAlgebra.lowDerivativeConstant period q * 2 * EulerCylinderSobolev.liftSobolevNorm period q f * EulerCylinderSobolev.liftSobolevNorm period q g

Every product derivative has an explicit L² bound by the product of fixed-order Sobolev norms.

theorem EulerH5CylinderAlgebra.cylinder_Hq_algebra (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 5 ≤ q) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ q, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerCylinderSobolev.liftSobolevNorm period q (f * g) ≤ EulerGeneralCylinderAlgebra.algebraConstant period q * EulerCylinderSobolev.liftSobolevNorm period q f * EulerCylinderSobolev.liftSobolevNorm period q g

The genuine complex cylinder Sobolev algebra estimate at every integer order q≥5.

Actual real and scalar-vector cylinder multiplication at every fixed Sobolev order q≥5.

theorem EulerH5CylinderAlgebra.real_cylinder_Hq_algebra (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 5 ≤ q) (f g : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerCylinderSobolev.liftSobolevNorm period q (f * g) ≤ EulerGeneralCylinderAlgebra.algebraConstant period q * EulerCylinderSobolev.liftSobolevNorm period q f * EulerCylinderSobolev.liftSobolevNorm period q g

The actual real cylinder algebra estimate at every fixed order q≥5.

theorem EulerH5CylinderAlgebra.real_product_word_memLp (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 5 ≤ q) (hn : n ≤ q) (w : Fin n → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (f * g)) 2 (EulerLiftedGradientSpace.liftMeasure period)

Every real product derivative through order q is genuinely square-integrable.

theorem EulerH5CylinderAlgebra.scalar_vector_product_word_memLp (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 5 ≤ q) (hn : n ≤ q) (d : ℕ) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain d) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) 2 (EulerLiftedGradientSpace.liftMeasure period)

Every scalar-vector product derivative through order q is genuinely in L².

theorem EulerH5CylinderAlgebra.cylinder_Hq_scalar_vector_product (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 5 ≤ q) (d : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain d) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (EulerCylinderSobolev.liftSobolevNorm period q fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) ≤ ↑d * EulerGeneralCylinderAlgebra.algebraConstant period q * EulerCylinderSobolev.liftSobolevNorm period q f * EulerCylinderSobolev.liftSobolevNorm period q g

Multiplication of an actual vector field by a scalar field is bounded in every Hq, q≥5.

noncomputable def EulerH6Nonlinear.lowerProductConstant (period : ℝ) [Fact (0 < period)] (d : ℕ) : ℝ

The actual H⁵ algebra constant for scalar-vector fields.

Equations

• EulerH6Nonlinear.lowerProductConstant period d = ↑d * EulerGeneralCylinderAlgebra.algebraConstant period 5

theorem EulerH6Nonlinear.lowerProductConstant_nonneg (period : ℝ) [Fact (0 < period)] (d : ℕ) : 0 ≤ lowerProductConstant period d

theorem EulerH6Nonlinear.product_wordH5Norm_bound (period : ℝ) [Fact (0 < period)] (q n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (wordSobolevNorm period 5 n fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) ≤ lowerProductConstant period q * EulerJetProductBounds.leibnizConvolution (fun (l : ℕ) => wordSobolevNorm period 5 l f) (fun (l : ℕ) => wordSobolevNorm period 5 l g) n

External derivatives of the genuine product obey the same binomial rule at base H⁵.

theorem EulerH6Nonlinear.derivative_H5_le_H6 (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (i : Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) : EulerCylinderSobolev.liftSobolevNorm period 5 (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f) ≤ 1365 * EulerCylinderSobolev.liftSobolevNorm period 6 f

One fixed coordinate derivative in H⁵ is controlled by the actual H⁶ norm.

theorem EulerH6Nonlinear.lower_word_shift_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : wordSobolevNorm period 5 (n + 1) f ≤ 5460 * wordSobolevNorm period 6 n f

Raising the external count by one while lowering the fixed base index consumes no higher Sobolev norm.

theorem EulerH6Nonlinear.wordSobolevNorm_mono (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {p q : ℕ} (hpq : p ≤ q) (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) : wordSobolevNorm period p n f ≤ wordSobolevNorm period q n f

Monotonicity in the fixed Sobolev index, at every external word order.

theorem EulerH6Nonlinear.transport_wordH5Norm_bound (period : ℝ) [Fact (0 < period)] (q n : ℕ) (b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4) (e : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x)) (hbL2 : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w b) 2 (EulerLiftedGradientSpace.liftMeasure period)) (heL2 : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w e) 2 (EulerLiftedGradientSpace.liftMeasure period)) : wordSobolevNorm period 5 n (transportField period q b e) ≤ lowerProductConstant period q * EulerJetProductBounds.leibnizConvolution (fun (l : ℕ) => wordSobolevNorm period 5 l b) (fun (l : ℕ) => wordSobolevNorm period 5 (l + 1) e) n

The actual transport source in the lower fixed Sobolev norm.

theorem EulerH6Nonlinear.transport_lower_no_loss (period : ℝ) [Fact (0 < period)] (n : ℕ) (b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x)) (hbL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w b) 2 (EulerLiftedGradientSpace.liftMeasure period)) (heL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w e) 2 (EulerLiftedGradientSpace.liftMeasure period)) : wordSobolevNorm period 5 n (transportField period 3 b e) ≤ 5460 * lowerProductConstant period 3 * EulerJetProductBounds.leibnizConvolution (fun (l : ℕ) => wordSobolevNorm period 6 l b) (fun (l : ℕ) => wordSobolevNorm period 6 l e) n

The pressure's H⁵ source uses only H⁶ velocity at the same external order.