Actual four-dimensional velocity fields assembled from bounded vector functionals.

noncomputable def EulerFunctionalVelocity.velocityMap (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4

Assemble the four actual cylinder-velocity components as a bounded linear map.

Equations

• EulerFunctionalVelocity.velocityMap L = ↑(EuclideanSpace.equiv (Fin 4) ℝ).symm ∘SL ContinuousLinearMap.pi L

@[simp]

theorem EulerFunctionalVelocity.velocityMap_apply (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (z : EulerLiftedGradientSpace.Vector3) (i : Fin 4) : ((velocityMap L) z).ofLp i = (L i) z

theorem EulerFunctionalVelocity.wordSobolevNorm_coordinates (period : ℝ) [Fact (0 < period)] (q n d : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain d) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerH6Nonlinear.wordSobolevNorm period q n f ≤ ∑ i : Fin d, EulerH6Nonlinear.wordSobolevNorm period q n (⇑(EulerVectorCylinder.coordinate d i) ∘ f)

Coordinate decomposition of the actual external-word Sobolev norm.

theorem EulerFunctionalVelocity.velocityMap_word_bound (period : ℝ) [Fact (0 < period)] (q n : ℕ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerH6Nonlinear.wordSobolevNorm period q n (⇑(velocityMap L) ∘ f) ≤ 4 * EulerH6Nonlinear.wordSobolevNorm period q n f

Passing from a three-vector to its four lifted velocity coefficients costs only the fixed dimension factor.