Fixed H⁶ algebra estimates at every external derivative order, for actual nonlinear fields.

theorem EulerH6Nonlinear.fieldDerivative_add (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : EulerLiftedGradientSpace.LiftTangent) (f g : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : EulerTransportDerivatives.fieldDerivative period a (f + g) = EulerTransportDerivatives.fieldDerivative period a f + EulerTransportDerivatives.fieldDerivative period a g

theorem EulerH6Nonlinear.word_add (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (w : Fin n → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : EulerCylinderSobolev.iteratedFieldDerivative period w (f + g) = EulerCylinderSobolev.iteratedFieldDerivative period w f + EulerCylinderSobolev.iteratedFieldDerivative period w g

theorem EulerH6Nonlinear.word_init_last (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (w : Fin (n + 1) → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) : EulerCylinderSobolev.iteratedFieldDerivative period w f = EulerCylinderSobolev.iteratedFieldDerivative period (Fin.init w) (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection (w (Fin.last n))) f)

theorem EulerH6Nonlinear.derivative_all_memLp (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hfL2 : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (i : Fin 4) (j : ℕ) (w : Fin j → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f)) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerH6Nonlinear.word_all_memLp (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hfL2 : ∀ (j : ℕ) (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (j : ℕ) (v : Fin j → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v (EulerCylinderSobolev.iteratedFieldDerivative period w f)) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerH6Nonlinear.sobolev_add_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (q : ℕ) (f g : EulerLiftedGradientSpace.LiftDomain period → F) (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) ≤ EulerCylinderSobolev.liftSobolevNorm period q f + EulerCylinderSobolev.liftSobolevNorm period q g

noncomputable def EulerH6Nonlinear.wordSobolevNorm (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (q n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) : ℝ

Sum of actual Hq norms of all external derivative words of exactly order n.

Equations

• EulerH6Nonlinear.wordSobolevNorm period q n f = ∑ w : Fin n → Fin 4, EulerCylinderSobolev.liftSobolevNorm period q (EulerCylinderSobolev.iteratedFieldDerivative period w f)

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

@[simp]

theorem EulerH6Nonlinear.wordSobolevNorm_zero (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (q : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) : wordSobolevNorm period q 0 f = EulerCylinderSobolev.liftSobolevNorm period q f

theorem EulerH6Nonlinear.wordSobolevNorm_succ (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (q n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) : wordSobolevNorm period q (n + 1) f = ∑ i : Fin 4, wordSobolevNorm period q n (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f)

theorem EulerH6Nonlinear.wordSobolevNorm_add_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (q n : ℕ) (f g : EulerLiftedGradientSpace.LiftDomain period → F) (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 q n (f + g) ≤ wordSobolevNorm period q n f + wordSobolevNorm period q n g

theorem EulerH6Nonlinear.fieldDerivative_smul (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : (EulerTransportDerivatives.fieldDerivative period a fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) = (fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerTransportDerivatives.fieldDerivative period a f x • g x) + fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • EulerTransportDerivatives.fieldDerivative period a g x

theorem EulerH6Nonlinear.product_all_memLp (period : ℝ) [Fact (0 < period)] (q : ℕ) (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)) (j : ℕ) (w : Fin j → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) 2 (EulerLiftedGradientSpace.liftMeasure period)

All actual derivative words of a smooth H-infinity scalar-vector product lie in L².

noncomputable def EulerH6Nonlinear.productConstant (period : ℝ) [Fact (0 < period)] (q : ℕ) : ℝ

The H⁶ algebra constant is fixed, independently of the external derivative order.

Equations

• EulerH6Nonlinear.productConstant period q = ↑q * (5461 * 128 * EulerCylinderAlgebra.lowDerivativeConstant period)

theorem EulerH6Nonlinear.productConstant_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) : 0 ≤ productConstant period q

theorem EulerH6Nonlinear.product_wordSobolevNorm_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 6 n fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) ≤ productConstant period q * EulerJetProductBounds.leibnizConvolution (fun (l : ℕ) => wordSobolevNorm period 6 l f) (fun (l : ℕ) => wordSobolevNorm period 6 l g) n

Exact external-order binomial convolution for actual scalar-vector products in fixed H⁶.