Real Euclidean vector wrappers for the actual cylinder Sobolev estimates.

theorem EulerVectorCylinder.postcomp_smooth (period : ℝ) {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : F →L[ℝ] G) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (⇑L ∘ f) x)

theorem EulerVectorCylinder.postcomp_word_memLp (period : ℝ) [Fact (0 < period)] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {s n : ℕ} (hn : n ≤ s) (L : F →L[ℝ] G) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ s, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (w : Fin n → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (⇑L ∘ f)) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerVectorCylinder.postcomp_sobolevNorm_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (s : ℕ) (L : F →L[ℝ] G) (hL : ‖L‖ ≤ 1) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ j ≤ s, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerCylinderSobolev.liftSobolevNorm period s (⇑L ∘ f) ≤ EulerCylinderSobolev.liftSobolevNorm period s f

noncomputable def EulerVectorCylinder.coordinate (q : ℕ) (i : Fin q) : EulerSobolev.Domain q →L[ℝ] ℝ

A coordinate projection on a real Euclidean target, of operator norm at most one.

Equations

• EulerVectorCylinder.coordinate q i = EuclideanSpace.proj i

theorem EulerVectorCylinder.coordinate_norm_le (q : ℕ) (i : Fin q) : ‖coordinate q i‖ ≤ 1

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

H³ controls the pointwise norm of a genuine real Euclidean cylinder field.

theorem EulerVectorCylinder.coordinate_word (period : ℝ) {n : ℕ} (q : ℕ) (i : Fin q) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerCylinderSobolev.iteratedFieldDerivative period w (⇑(coordinate q i) ∘ f) x = (EulerCylinderSobolev.iteratedFieldDerivative period w f x).ofLp i

The coordinate of a classical derivative is the derivative of the coordinate.

theorem EulerVectorCylinder.vector_eLpNorm_le_sum_coordinates (period : ℝ) [Fact (0 < period)] (q : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) (hf : ∀ (i : Fin q), MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => (f x).ofLp i) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period) ≤ ∑ i : Fin q, MeasureTheory.eLpNorm (fun (x : EulerLiftedGradientSpace.LiftDomain period) => (f x).ofLp i) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerVectorCylinder.vector_word_L2_le_sum_coordinates (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (q : ℕ) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ (i : Fin q), ∀ j ≤ s, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v (⇑(coordinate q i) ∘ f)) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ ∑ i : Fin q, (MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative period w (⇑(coordinate q i) ∘ f)) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal

theorem EulerVectorCylinder.vector_sobolevNorm_le_sum_coordinates (period : ℝ) [Fact (0 < period)] (q s : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : ∀ (i : Fin q), ∀ j ≤ s, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v (⇑(coordinate q i) ∘ f)) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerCylinderSobolev.liftSobolevNorm period s f ≤ ∑ i : Fin q, EulerCylinderSobolev.liftSobolevNorm period s (⇑(coordinate q i) ∘ f)

A vector Sobolev norm is controlled by the sum of its scalar coordinate norms.

theorem EulerVectorCylinder.real_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 : ∀ j ≤ 6, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ 6, ∀ (v : Fin j → 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)

theorem EulerVectorCylinder.coordinate_smul (period : ℝ) (q : ℕ) (i : Fin q) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q) : (⇑(coordinate q i) ∘ fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) = f * ⇑(coordinate q i) ∘ g

theorem EulerVectorCylinder.cylinder_H6_scalar_vector_product (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 ≤ 6, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ 6, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (EulerCylinderSobolev.liftSobolevNorm period 6 fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) ≤ ↑q * (5461 * 128 * EulerCylinderAlgebra.lowDerivativeConstant period) * EulerCylinderSobolev.liftSobolevNorm period 6 f * EulerCylinderSobolev.liftSobolevNorm period 6 g

Multiplication of an actual vector field by a scalar field is bounded in H⁶.