Actual cylinder Sobolev multiplication at every fixed integer order q ≥ 6.

noncomputable def EulerGeneralCylinderAlgebra.lowDerivativeConstant (period : ℝ) [Fact (0 < period)] (q : ℕ) : ℝ

An explicit low-derivative tensor embedding constant for fixed Sobolev order q.

Equations

• EulerGeneralCylinderAlgebra.lowDerivativeConstant period q = 4 ^ q * 85 * EulerCylinderSobolev.cylinderEmbeddingConstant period

theorem EulerGeneralCylinderAlgebra.lowDerivativeConstant_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) : 0 ≤ lowDerivativeConstant period q

The low-derivative embedding constant is nonnegative.

theorem EulerGeneralCylinderAlgebra.word_H3_le_Hq (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {q m : ℕ} (hm : m + 3 ≤ q) (w : Fin m → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) : EulerCylinderSobolev.liftSobolevNorm period 3 (EulerCylinderSobolev.iteratedFieldDerivative period w f) ≤ 85 * EulerCylinderSobolev.liftSobolevNorm period q f

Three additional derivatives control the H³ norm of an arbitrary derivative word.

theorem EulerGeneralCylinderAlgebra.word_pointwise_le_Hq (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m + 3 ≤ q) (w : Fin m → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ q, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerCylinderSobolev.iteratedFieldDerivative period w f x‖ ≤ EulerCylinderSobolev.cylinderEmbeddingConstant period * (85 * EulerCylinderSobolev.liftSobolevNorm period q f)

Actual derivative words with three derivatives to spare are uniformly bounded pointwise.

theorem EulerGeneralCylinderAlgebra.tensor_low_le_Hq (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m + 3 ≤ q) (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ q, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖iteratedFDeriv ℝ m (EulerCylinderSobolev.euclideanLift period f x) 0‖ ≤ lowDerivativeConstant period q * EulerCylinderSobolev.liftSobolevNorm period q f

The actual low-order Fréchet tensor is bounded by the fixed-order cylinder Sobolev norm.

theorem EulerGeneralCylinderAlgebra.tensor_le_totalMagnitude (period : ℝ) {q n : ℕ} (hn : n ≤ q) (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖iteratedFDeriv ℝ n (EulerCylinderSobolev.euclideanLift period f x) 0‖ ≤ EulerCylinderSobolev.totalMagnitude period q f x

Every tensor through the fixed Sobolev order is dominated by the actual derivative envelope.

noncomputable def EulerGeneralCylinderAlgebra.productEnvelope (period : ℝ) [Fact (0 < period)] (q : ℕ) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) : EulerLiftedGradientSpace.LiftDomain period → ℝ

The square-integrable envelope obtained by putting one factor in L∞ and the other in L².

Equations

• One or more equations did not get rendered due to their size.

theorem EulerGeneralCylinderAlgebra.productEnvelope_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (x : EulerLiftedGradientSpace.LiftDomain period) : 0 ≤ productEnvelope period q f g x

The product envelope is pointwise nonnegative.

theorem EulerGeneralCylinderAlgebra.product_tensor_term_le (period : ℝ) [Fact (0 < period)] {q n j : ℕ} (hq : 6 ≤ 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‖ ≤ lowDerivativeConstant period q * productEnvelope period q f g x

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

theorem EulerGeneralCylinderAlgebra.product_word_pointwise_le (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 6 ≤ 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 * lowDerivativeConstant period q * productEnvelope period q f g x

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

theorem EulerGeneralCylinderAlgebra.productEnvelope_memLp (period : ℝ) [Fact (0 < period)] (q : ℕ) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (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 (productEnvelope period q f g) 2 (EulerLiftedGradientSpace.liftMeasure period)

The actual low/high envelope is square-integrable.

theorem EulerGeneralCylinderAlgebra.productEnvelope_L2_le (period : ℝ) [Fact (0 < period)] (q : ℕ) (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (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.toLp (productEnvelope period q f g) ⋯‖ ≤ 2 * EulerCylinderSobolev.liftSobolevNorm period q f * EulerCylinderSobolev.liftSobolevNorm period q g

The L² norm of the low/high envelope is bounded by twice the product of Sobolev norms.

theorem EulerGeneralCylinderAlgebra.product_word_memLp (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 6 ≤ 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 EulerGeneralCylinderAlgebra.product_word_L2_le (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 6 ≤ 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 * 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.

noncomputable def EulerGeneralCylinderAlgebra.algebraConstant (period : ℝ) [Fact (0 < period)] (q : ℕ) : ℝ

A finite explicit algebra constant for each fixed Sobolev order.

Equations

• EulerGeneralCylinderAlgebra.algebraConstant period q = (∑ n ∈ Finset.range (q + 1), 4 ^ n) * (2 ^ q * EulerGeneralCylinderAlgebra.lowDerivativeConstant period q * 2)

theorem EulerGeneralCylinderAlgebra.algebraConstant_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) : 0 ≤ algebraConstant period q

The fixed-order algebra constant is nonnegative.

theorem EulerGeneralCylinderAlgebra.cylinder_Hq_algebra (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ 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) ≤ 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≥6.