Actual H⁶ multiplication on the three-dimensional cylinder.

noncomputable def EulerCylinderAlgebra.lowDerivativeConstant (period : ℝ) [Fact (0 < period)] : ℝ

The low-order tensor bound furnished by the cylinder embedding.

Equations

• EulerCylinderAlgebra.lowDerivativeConstant period = 64 * 85 * EulerCylinderSobolev.cylinderEmbeddingConstant period

theorem EulerCylinderAlgebra.lowDerivativeConstant_nonneg (period : ℝ) [Fact (0 < period)] : 0 ≤ lowDerivativeConstant period

theorem EulerCylinderAlgebra.tensor_low_le_H6 (period : ℝ) [Fact (0 < period)] {m : ℕ} (hm : m ≤ 3) (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ 6, ∀ (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 * EulerCylinderSobolev.liftSobolevNorm period 6 f

theorem EulerCylinderAlgebra.tensor_le_totalMagnitude (period : ℝ) {n : ℕ} (hn : n ≤ 6) (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 6 f x

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

The real-valued envelope arising from the low/high derivative split.

Equations

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

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

theorem EulerCylinderAlgebra.product_smooth (period : ℝ) (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)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (f * g) x)

theorem EulerCylinderAlgebra.product_tensor_term_le (period : ℝ) [Fact (0 < period)] {n j : ℕ} (hn : n ≤ 6) (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 ≤ 6, ∀ (w : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ 6, ∀ (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 * productEnvelope period f g x

theorem EulerCylinderAlgebra.product_word_pointwise_le (period : ℝ) [Fact (0 < period)] {n : ℕ} (hn : n ≤ 6) (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 ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ 6, ∀ (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‖ ≤ 64 * lowDerivativeConstant period * productEnvelope period f g x

Actual Leibniz derivatives of a product have a square-integrable low/high envelope.

theorem EulerCylinderAlgebra.productEnvelope_memLp (period : ℝ) [Fact (0 < period)] (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hfL2 : ∀ k ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (productEnvelope period f g) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerCylinderAlgebra.productEnvelope_L2_le (period : ℝ) [Fact (0 < period)] (f g : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hfL2 : ∀ k ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : ‖MeasureTheory.MemLp.toLp (productEnvelope period f g) ⋯‖ ≤ 2 * EulerCylinderSobolev.liftSobolevNorm period 6 f * EulerCylinderSobolev.liftSobolevNorm period 6 g

theorem EulerCylinderAlgebra.product_word_memLp (period : ℝ) [Fact (0 < period)] {n : ℕ} (hn : n ≤ 6) (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 ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ 6, ∀ (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 six of the product is genuinely square-integrable.

theorem EulerCylinderAlgebra.product_word_L2_le (period : ℝ) [Fact (0 < period)] {n : ℕ} (hn : n ≤ 6) (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 ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ 6, ∀ (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 ≤ 128 * lowDerivativeConstant period * EulerCylinderSobolev.liftSobolevNorm period 6 f * EulerCylinderSobolev.liftSobolevNorm period 6 g

An explicit bound for each actual product derivative in L².

theorem EulerCylinderAlgebra.cylinder_H6_algebra (period : ℝ) [Fact (0 < period)] (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 ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ k ≤ 6, ∀ (v : Fin k → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerCylinderSobolev.liftSobolevNorm period 6 (f * g) ≤ 5461 * 128 * lowDerivativeConstant period * EulerCylinderSobolev.liftSobolevNorm period 6 f * EulerCylinderSobolev.liftSobolevNorm period 6 g

The H⁶ algebra estimate on the actual cylinder, with a finite explicit constant.