Actual derivative-word Sobolev norms on R³ × T and compact localizations.

noncomputable def EulerCylinderSobolev.standardDirection (i : Fin 4) : EulerLiftedGradientSpace.LiftTangent

The four coordinate directions, with angle first and the spatial coordinates following.

Equations

• EulerCylinderSobolev.standardDirection i = EulerCylinderCoordinates.coordinateEquiv (EuclideanSpace.single i 1)

@[simp]

theorem EulerCylinderSobolev.standardDirection_zero : standardDirection 0 = (0, 1)

@[simp]

theorem EulerCylinderSobolev.standardDirection_succ (i : Fin 3) : standardDirection i.succ = (EuclideanSpace.single i 1, 0)

noncomputable def EulerCylinderSobolev.iteratedFieldDerivative (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} : (Fin n → Fin 4) → (EulerLiftedGradientSpace.LiftDomain period → F) → EulerLiftedGradientSpace.LiftDomain period → F

Ordered actual derivatives on the cylinder; the head is differentiated last.

Equations

• One or more equations did not get rendered due to their size.
• EulerCylinderSobolev.iteratedFieldDerivative period x_3 x✝ = x✝

@[simp]

theorem EulerCylinderSobolev.iteratedFieldDerivative_zero (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (w : Fin 0 → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) : iteratedFieldDerivative period w f = f

@[simp]

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

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

A concrete norm: the sum of L² norms of all ordered coordinate derivatives up to order s.

Equations

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

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

noncomputable def EulerCylinderSobolev.euclideanLift (period : ℝ) {F : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerSobolev.Domain 4 → F

The actual field lifted to Euclidean coordinates centered at a cylinder point.

Equations

• EulerCylinderSobolev.euclideanLift period f x = EulerMetricTransport.localFieldLift period f x ∘ ⇑EulerCylinderCoordinates.coordinateEquiv

theorem EulerCylinderSobolev.euclideanLift_smooth (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (euclideanLift period f x)

theorem EulerCylinderSobolev.euclideanLift_zero (period : ℝ) {F : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : euclideanLift period f x 0 = f x

theorem EulerCylinderSobolev.euclideanLift_fieldDerivative (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (v z : EulerSobolev.Domain 4) (x : EulerLiftedGradientSpace.LiftDomain period) : euclideanLift period (EulerTransportDerivatives.fieldDerivative period (EulerCylinderCoordinates.coordinateEquiv v) f) x z = (fderiv ℝ (euclideanLift period f x) z) v

theorem EulerCylinderSobolev.euclideanLift_iteratedFieldDerivative (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) (z : EulerSobolev.Domain 4) : euclideanLift period (iteratedFieldDerivative period w f) x z = (iteratedFDeriv ℝ n (euclideanLift period f x) z) fun (j : Fin n) => EuclideanSpace.single (w j) 1

The word derivative is exactly the corresponding coordinate entry of the Fréchet tensor.

theorem EulerCylinderSobolev.euclideanLift_tensor_norm_le (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)) (x : EulerLiftedGradientSpace.LiftDomain period) (z : EulerSobolev.Domain 4) : ‖iteratedFDeriv ℝ n (euclideanLift period f x) z‖ ≤ ∑ w : Fin n → Fin 4, ‖euclideanLift period (iteratedFieldDerivative period w f) x z‖

Tensor operator norms are controlled by the actual coordinate-word derivatives.

noncomputable def EulerCylinderSobolev.wordMagnitude (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : ℝ

Sum of the norms of all coordinate words of one fixed order.

Equations

• EulerCylinderSobolev.wordMagnitude period n f x = ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative period w f x‖

theorem EulerCylinderSobolev.wordMagnitude_nonneg (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : 0 ≤ wordMagnitude period n f x

noncomputable def EulerCylinderSobolev.totalMagnitude (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (s : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : ℝ

The sum of all coordinate derivative magnitudes through a given order.

Equations

• EulerCylinderSobolev.totalMagnitude period s f x = ∑ n ∈ Finset.range (s + 1), EulerCylinderSobolev.wordMagnitude period n f x

theorem EulerCylinderSobolev.totalMagnitude_nonneg (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (s : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : 0 ≤ totalMagnitude period s f x

theorem EulerCylinderSobolev.wordMagnitude_le_total (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (s n : ℕ) (hn : n ≤ s) (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : wordMagnitude period n f x ≤ totalMagnitude period s f x

noncomputable def EulerCylinderSobolev.translated (period : ℝ) {F : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.LiftDomain period → F

Translation of an actual cylinder function.

Equations

• EulerCylinderSobolev.translated period f x y = f (y + x)

theorem EulerCylinderSobolev.eLpNorm_translated (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.AEStronglyMeasurable f (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : MeasureTheory.eLpNorm (translated period f x) 2 (EulerLiftedGradientSpace.liftMeasure period) = MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerCylinderSobolev.memLp_translated (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : MeasureTheory.MemLp (translated period f x) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerCylinderSobolev.euclideanLift_eq_translated_cover (period : ℝ) {F : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) (z : EulerSobolev.Domain 4) : euclideanLift period f x z = translated period f x (EulerCylinderCoordinates.euclideanCover period z)

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

theorem EulerCylinderSobolev.eLpNorm_wordMagnitude_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (w : Fin n → Fin 4), MeasureTheory.MemLp (iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.eLpNorm (wordMagnitude period n f) 2 (EulerLiftedGradientSpace.liftMeasure period) ≤ ∑ w : Fin n → Fin 4, MeasureTheory.eLpNorm (iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerCylinderSobolev.totalMagnitude_memLp (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (s : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ n ≤ s, ∀ (w : Fin n → Fin 4), MeasureTheory.MemLp (iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (totalMagnitude period s f) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerCylinderSobolev.totalMagnitude_L2_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (s : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ n ≤ s, ∀ (w : Fin n → Fin 4), MeasureTheory.MemLp (iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : ‖MeasureTheory.MemLp.toLp (totalMagnitude period s f) ⋯‖ ≤ liftSobolevNorm period s f

noncomputable def EulerCylinderSobolev.localBump (period : ℝ) [Fact (0 < period)] : ContDiffBump 0

A fixed compact smooth localizer, supported in the chart neighborhood and equal to one at zero.

Equations

• EulerCylinderSobolev.localBump period = { rIn := period, rOut := 2 * period, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem EulerCylinderSobolev.localBump_smooth (period : ℝ) [Fact (0 < period)] : ContDiff ℝ ↑⊤ ↑(localBump period)

theorem EulerCylinderSobolev.localBump_zero (period : ℝ) [Fact (0 < period)] : ↑(localBump period) 0 = 1

theorem EulerCylinderSobolev.localBump_support (period : ℝ) [Fact (0 < period)] : tsupport ↑(localBump period) ⊆ {z : EulerSobolev.Domain 4 | |z.ofLp 0| ≤ 2 * period}

noncomputable def EulerCylinderSobolev.bumpSchwartz (period : ℝ) [Fact (0 < period)] : SchwartzMap (EulerSobolev.Domain 4) ℝ

The local bump regarded as a real Schwartz function.

Equations

• EulerCylinderSobolev.bumpSchwartz period = ⋯.toSchwartzMap ⋯

noncomputable def EulerCylinderSobolev.bumpBound (period : ℝ) [Fact (0 < period)] (j : ℕ) : NNReal

A finite, explicitly defined bound for each derivative of the fixed local bump.

Equations

• EulerCylinderSobolev.bumpBound period j = ⟨(SchwartzMap.seminorm ℝ 0 j) (EulerCylinderSobolev.bumpSchwartz period), ⋯⟩

theorem EulerCylinderSobolev.localBump_derivative_bound (period : ℝ) [Fact (0 < period)] (j : ℕ) (z : EulerSobolev.Domain 4) : ‖iteratedFDeriv ℝ j (↑(localBump period)) z‖ ≤ ↑(bumpBound period j)

noncomputable def EulerCylinderSobolev.bumpCoefficient (period : ℝ) [Fact (0 < period)] (n : ℕ) : NNReal

Finite Leibniz coefficient controlling localization at derivative order n.

Equations

• EulerCylinderSobolev.bumpCoefficient period n = ∑ j ∈ Finset.range (n + 1), ↑(n.choose j) * EulerCylinderSobolev.bumpBound period j

noncomputable def EulerCylinderSobolev.localized (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : SchwartzMap (EulerSobolev.Domain 4) ℂ

An actual compactly supported localization of an arbitrary smooth cylinder field.

Equations

• EulerCylinderSobolev.localized period f hf x = ⋯.toSchwartzMap ⋯

@[simp]

theorem EulerCylinderSobolev.localized_apply (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) (z : EulerSobolev.Domain 4) : (localized period f hf x) z = ↑(localBump period) z • euclideanLift period f x z

theorem EulerCylinderSobolev.localized_zero (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : (localized period f hf x) 0 = f x

theorem EulerCylinderSobolev.localized_tsupport (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : tsupport ⇑(localized period f hf x) ⊆ {z : EulerSobolev.Domain 4 | |z.ofLp 0| ≤ 2 * period}

theorem EulerCylinderSobolev.localized_tensor_norm_le (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) (z : EulerSobolev.Domain 4) : ‖iteratedFDeriv ℝ n (⇑(localized period f hf x)) z‖ ≤ ↑(bumpCoefficient period n) * translated period (totalMagnitude period n f) x (EulerCylinderCoordinates.euclideanCover period z)

The actual Leibniz rule controls every localized derivative by cylinder derivative words.

theorem EulerCylinderSobolev.directional_localized_support (period : ℝ) [Fact (0 < period)] (n : ℕ) (i : Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : Function.support ⇑(EulerSobolevProducts.directional 4 n (EuclideanSpace.single i 1) (localized period f hf x)) ⊆ {z : EulerSobolev.Domain 4 | |z.ofLp 0| ≤ 2 * period}

Each pure directional derivative of the localization has the same chart support.

theorem EulerCylinderSobolev.localized_directional_L2_le (period : ℝ) [Fact (0 < period)] (n : ℕ) (i : Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ n, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖(EulerSobolevProducts.directional 4 n (EuclideanSpace.single i 1) (localized period f hf x)).toLp 2 MeasureTheory.volume‖ ≤ ↑(bumpCoefficient period n) * 6 ^ (1 / 2) * liftSobolevNorm period n f

Every localized pure derivative is controlled by the actual cylinder derivative L² sum.

theorem EulerCylinderSobolev.liftSobolevNorm_nonneg (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (s : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) : 0 ≤ liftSobolevNorm period s f

theorem EulerCylinderSobolev.liftSobolevNorm_mono (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {s t : ℕ} (hst : s ≤ t) (f : EulerLiftedGradientSpace.LiftDomain period → F) : liftSobolevNorm period s f ≤ liftSobolevNorm period t f

noncomputable def EulerCylinderSobolev.cylinderEmbeddingConstant (period : ℝ) [Fact (0 < period)] : ℝ

A concrete finite embedding constant depending only on the circle period.

Equations

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

theorem EulerCylinderSobolev.cylinderEmbeddingConstant_nonneg (period : ℝ) [Fact (0 < period)] : 0 ≤ cylinderEmbeddingConstant period

theorem EulerCylinderSobolev.cylinder_pointwise_le_H3 (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → ℂ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ 3, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖f x‖ ≤ cylinderEmbeddingConstant period * liftSobolevNorm period 3 f

Genuine H³ to L∞ embedding on R³ × T for arbitrary smooth fields with square-integrable derivatives.

theorem EulerCylinderSobolev.iteratedFieldDerivative_comp_exists (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {m n : ℕ} (v : Fin n → Fin 4) (w : Fin m → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) : ∃ (u : Fin (m + n) → Fin 4), iteratedFieldDerivative period v (iteratedFieldDerivative period w f) = iteratedFieldDerivative period u f

Composing two actual derivative words gives a word of the combined length.

theorem EulerCylinderSobolev.word_L2_le_liftSobolevNorm (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {s n : ℕ} (hn : n ≤ s) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → F) : (MeasureTheory.eLpNorm (iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ liftSobolevNorm period s f

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

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

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

Uniform control of any derivative word of order at most three by the H⁶ norm.