The actual external transport commutator and its cutoff-independent Gevrey radius-loss estimate.

The actual base Sobolev transport commutator with no uncontrolled extra derivative.

Mixed derivative product estimates with only five total derivatives, for the base transport commutator.

noncomputable def EulerMixedH5Product.mixedConstant (period : ℝ) [Fact (0 < period)] : ℝ

An explicit uniform constant for mixed scalar-vector derivative products through total order five.

Equations

• EulerMixedH5Product.mixedConstant period = 3 * 85 * EulerCylinderSobolev.cylinderEmbeddingConstant period

theorem EulerMixedH5Product.mixedConstant_nonneg (period : ℝ) [Fact (0 < period)] : 0 ≤ mixedConstant period

theorem EulerMixedH5Product.scalar_word_pointwise (period : ℝ) [Fact (0 < period)] {k : ℕ} (hk : k ≤ 2) (w : Fin k → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL : ∀ j ≤ 5, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerCylinderSobolev.iteratedFieldDerivative period w f x‖ ≤ mixedConstant period * EulerCylinderSobolev.liftSobolevNorm period 5 f

Low scalar derivatives are bounded by the original H⁵ norm.

theorem EulerMixedH5Product.vector_word_pointwise (period : ℝ) [Fact (0 < period)] {k : ℕ} (hk : k ≤ 2) (w : Fin k → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL : ∀ j ≤ 5, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerCylinderSobolev.iteratedFieldDerivative period w f x‖ ≤ mixedConstant period * EulerCylinderSobolev.liftSobolevNorm period 5 f

Low vector derivatives are bounded by the original H⁵ norm.

theorem EulerMixedH5Product.memLp_norm_of_domination (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → E) (g : EulerLiftedGradientSpace.LiftDomain period → F) (c : ℝ) (hc : 0 ≤ c) (hf : MeasureTheory.AEStronglyMeasurable f (EulerLiftedGradientSpace.liftMeasure period)) (hg : MeasureTheory.MemLp g 2 (EulerLiftedGradientSpace.liftMeasure period)) (h : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖f x‖ ≤ c * ‖g x‖) : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period) ∧ (MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ c * (MeasureTheory.eLpNorm g 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal

An actual pointwise L² domination gives both integrability and the corresponding norm estimate.

theorem EulerMixedH5Product.mixed_product_bound (period : ℝ) [Fact (0 < period)] {k l : ℕ} (hkl : k + l ≤ 5) (w : Fin k → Fin 4) (v : Fin l → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ j ≤ 5, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ j ≤ 5, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerCylinderSobolev.iteratedFieldDerivative period w f x • EulerCylinderSobolev.iteratedFieldDerivative period v g x) 2 (EulerLiftedGradientSpace.liftMeasure period) ∧ (MeasureTheory.eLpNorm (fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerCylinderSobolev.iteratedFieldDerivative period w f x • EulerCylinderSobolev.iteratedFieldDerivative period v g x) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ mixedConstant period * EulerCylinderSobolev.liftSobolevNorm period 5 f * EulerCylinderSobolev.liftSobolevNorm period 5 g

The literal product of two derivative words with at most five total derivatives is in L² with a fixed H⁵ bound.

theorem EulerMixedH5Product.fieldL2_add_le (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] (f g : EulerLiftedGradientSpace.LiftDomain period → E) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) (hg : MeasureTheory.MemLp g 2 (EulerLiftedGradientSpace.liftMeasure period)) : (MeasureTheory.eLpNorm (f + g) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ (MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal + (MeasureTheory.eLpNorm g 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal

The real L² norm obeys the triangle inequality whenever both actual fields are square-integrable.

Actual outer derivatives of mixed products, with a fixed total derivative budget.

theorem EulerMixedH5Product.mixed_outer_product_bound (period : ℝ) [Fact (0 < period)] {n k l : ℕ} (hnkl : n + k + l ≤ 5) (a : Fin n → Fin 4) (w : Fin k → Fin 4) (v : Fin l → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ j ≤ 5, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ j ≤ 5, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period a fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerCylinderSobolev.iteratedFieldDerivative period w f x • EulerCylinderSobolev.iteratedFieldDerivative period v g x) 2 (EulerLiftedGradientSpace.liftMeasure period) ∧ (MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative period a fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerCylinderSobolev.iteratedFieldDerivative period w f x • EulerCylinderSobolev.iteratedFieldDerivative period v g x) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ 2 ^ n * mixedConstant period * EulerCylinderSobolev.liftSobolevNorm period 5 f * EulerCylinderSobolev.liftSobolevNorm period 5 g

Outer product differentiation preserves the total derivative budget and costs only the finite Leibniz factor.

noncomputable def EulerBaseTransportCommutator.gradientFiveNorm (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) : ℝ

The sum of H⁵ norms of the four actual first derivatives.

Equations

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

theorem EulerBaseTransportCommutator.gradientFiveNorm_nonneg (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) : 0 ≤ gradientFiveNorm period f

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

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

Six actual derivatives of a field give five derivatives of each first derivative.

noncomputable def EulerBaseTransportCommutator.scalarCommutator (period : ℝ) {n : ℕ} (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3

The literal differential commutator D^w(fg)−f D^w g.

Equations

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

theorem EulerBaseTransportCommutator.scalarCommutator_recurrence (period : ℝ) {n : ℕ} (w : Fin (n + 1) → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : scalarCommutator period w f g = (EulerCylinderSobolev.iteratedFieldDerivative period (Fin.init w) fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection (w (Fin.last n))) f x • g x) + scalarCommutator period (Fin.init w) f (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection (w (Fin.last n))) g)

Exact commutator recurrence isolates one actual derivative of the scalar coefficient.

theorem EulerBaseTransportCommutator.mixed_scalarCommutator_bound (period : ℝ) [Fact (0 < period)] {n l : ℕ} (hnl : n + l ≤ 6) (w : Fin n → Fin 4) (v : Fin l → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ j ≤ 6, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ j ≤ 5, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (scalarCommutator period w f (EulerCylinderSobolev.iteratedFieldDerivative period v g)) 2 (EulerLiftedGradientSpace.liftMeasure period) ∧ (MeasureTheory.eLpNorm (scalarCommutator period w f (EulerCylinderSobolev.iteratedFieldDerivative period v g)) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ (2 ^ n - 1) * EulerMixedH5Product.mixedConstant period * gradientFiveNorm period f * EulerCylinderSobolev.liftSobolevNorm period 5 g

The commutator cancels its apparent highest derivative before the L² estimate is applied.

theorem EulerBaseTransportCommutator.scalarCommutator_bound (period : ℝ) [Fact (0 < period)] {n : ℕ} (hn : n ≤ 6) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ j ≤ 6, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ j ≤ 5, ∀ (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (scalarCommutator period w f g) 2 (EulerLiftedGradientSpace.liftMeasure period) ∧ (MeasureTheory.eLpNorm (scalarCommutator period w f g) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ (2 ^ n - 1) * EulerMixedH5Product.mixedConstant period * gradientFiveNorm period f * EulerCylinderSobolev.liftSobolevNorm period 5 g

The actual base commutator through six derivatives has the source's H⁵×H⁵ bound.

Actual fixed-H⁶ external scalar multiplication commutators with positive-order binomial bounds.

theorem EulerExternalScalarCommutator.fieldDerivative_sub (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 EulerExternalScalarCommutator.word_sub (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 EulerExternalScalarCommutator.scalarCommutator_smooth (period : ℝ) {n : ℕ} (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (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 (EulerBaseTransportCommutator.scalarCommutator period w f g) x)

theorem EulerExternalScalarCommutator.scalarCommutator_all_memLp (period : ℝ) [Fact (0 < period)] {n : ℕ} (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u g) 2 (EulerLiftedGradientSpace.liftMeasure period)) (j : ℕ) (u : Fin j → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u (EulerBaseTransportCommutator.scalarCommutator period w f g)) 2 (EulerLiftedGradientSpace.liftMeasure period)

noncomputable def EulerExternalScalarCommutator.commutatorH6Norm (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : ℝ

Sum of actual H⁶ norms of external commutators at one order.

Equations

• EulerExternalScalarCommutator.commutatorH6Norm period n f g = ∑ w : Fin n → Fin 4, EulerCylinderSobolev.liftSobolevNorm period 6 (EulerBaseTransportCommutator.scalarCommutator period w f g)

theorem EulerExternalScalarCommutator.commutatorH6Norm_nonneg (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : 0 ≤ commutatorH6Norm period n f g

@[simp]

theorem EulerExternalScalarCommutator.commutatorH6Norm_zero (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : commutatorH6Norm period 0 f g = 0

theorem EulerExternalScalarCommutator.commutatorH6Norm_succ_le (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : commutatorH6Norm period (n + 1) f g ≤ ∑ i : Fin 4, ((EulerH6Nonlinear.wordSobolevNorm period 6 n fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) f x • g x) + commutatorH6Norm period n f (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) g))

The exact differential recurrence gives a recurrence of the actual fixed-base Sobolev norms.

theorem EulerExternalScalarCommutator.commutatorH6Norm_bound (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : commutatorH6Norm period n f g ≤ EulerH6Nonlinear.productConstant period 3 * EulerJetProductBounds.commutatorConvolution (fun (l : ℕ) => EulerH6Nonlinear.wordSobolevNorm period 6 l f) (fun (l : ℕ) => EulerH6Nonlinear.wordSobolevNorm period 6 l g) n

The actual external commutator has exactly the positive-coefficient-order binomial convolution.

theorem EulerExternalTransportCommutator.word_derivative_comm (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (w : Fin n → Fin 4) (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : EulerCylinderSobolev.iteratedFieldDerivative period w (EulerTransportDerivatives.fieldDerivative period a f) = EulerTransportDerivatives.fieldDerivative period a (EulerCylinderSobolev.iteratedFieldDerivative period w f)

Actual coordinate words commute with each constant-direction derivative of a smooth field.

noncomputable def EulerExternalTransportCommutator.transportCommutator (period : ℝ) {n : ℕ} (w : Fin n → Fin 4) (b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3

The literal external transport commutator D^w(b·∇e)−b·∇D^w e.

Equations

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

theorem EulerExternalTransportCommutator.transportCommutator_eq_sum (period : ℝ) {n : ℕ} (w : Fin n → Fin 4) (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)) : transportCommutator period w b e = ∑ i : Fin 4, EulerBaseTransportCommutator.scalarCommutator period w (⇑(EulerVectorCylinder.coordinate 4 i) ∘ b) (EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) e)

The actual transport commutator is exactly the sum of the scalar multiplication commutators.

noncomputable def EulerExternalTransportCommutator.transportCommutatorNorm (period : ℝ) [Fact (0 < period)] (n : ℕ) (b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : ℝ

Sum of the actual H⁶ norms of all external transport commutators at one order.

Equations

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

theorem EulerExternalTransportCommutator.commutatorConvolution_mono_left (n : ℕ) (A A' B : ℕ → ℝ) (hA : ∀ (l : ℕ), A l ≤ A' l) (hB : ∀ (l : ℕ), 0 ≤ B l) : EulerJetProductBounds.commutatorConvolution A B n ≤ EulerJetProductBounds.commutatorConvolution A' B n

Positivity allows monotonicity of the coefficient sequence in the genuine commutator convolution.

theorem EulerExternalTransportCommutator.transportCommutatorNorm_bound (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 : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u b) 2 (EulerLiftedGradientSpace.liftMeasure period)) (heL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u e) 2 (EulerLiftedGradientSpace.liftMeasure period)) : transportCommutatorNorm period n b e ≤ EulerH6Nonlinear.productConstant period 3 * EulerJetProductBounds.commutatorConvolution (fun (l : ℕ) => EulerH6Nonlinear.wordSobolevNorm period 6 l b) (fun (l : ℕ) => EulerH6Nonlinear.wordSobolevNorm period 6 (l + 1) e) n

The actual external transport commutator has no undifferentiated-velocity term.

theorem EulerExternalTransportCommutator.transportCommutator_weighted_bound (period : ℝ) [Fact (0 < period)] (N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (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 : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u b) 2 (EulerLiftedGradientSpace.liftMeasure period)) (heL : ∀ (j : ℕ) (u : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period u e) 2 (EulerLiftedGradientSpace.liftMeasure period)) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * transportCommutatorNorm period n b e ≤ (EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ * ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * EulerH6Nonlinear.wordSobolevNorm period 6 l b) * ∑ j ∈ Finset.range (N + 1), ↑j * EulerPacketWeights.weight ρ j * EulerH6Nonlinear.wordSobolevNorm period 6 j e

The actual external transport commutator obeys the radius-loss bound with no cutoff-dependent constant or cutoff-plus-one velocity.