Actual derivative words at any lower Sobolev level, with exact representative and norm identities.

noncomputable def EulerSobolevWordLevel.wordAtLevel (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (w : Fin n → Fin 4) (h : n + q ≤ s) : ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

A genuine derivative word followed by restriction to its prescribed target Sobolev level.

Equations

• EulerSobolevWordLevel.wordAtLevel period q n w h = EulerSobolevWordBlocks.wordBlock period q n w ∘SL EulerCylinderSobolevSpace.restrictOperator period ⋯

theorem EulerSobolevWordLevel.wordAtLevel_value (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (w : Fin n → Fin 4) (h : n + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerCylinderSobolevSpace.value period ((wordAtLevel period q n w h) u) = (EulerCylinderSobolevSpace.toJet period u).word w

The underlying L² value is the literal strong derivative coordinate of the original field.

theorem EulerSobolevWordLevel.wordAtLevel_ae (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (w : Fin n → Fin 4) (h : n + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : ↑↑(EulerCylinderSobolevSpace.value period ((wordAtLevel period q n w h) u)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerCylinderSobolev.iteratedFieldDerivative period w f

Every actual smooth representative has the expected classical word after this operation.

theorem EulerSobolevWordLevel.continuous_sumNorm (period : ℝ) [Fact (0 < period)] (q : ℕ) : Continuous (EulerCylinderSobolevSpace.sumNorm period)

The derivative-sum Sobolev norm is continuous on its complete finite-array space.

theorem EulerSobolevWordLevel.sumNorm_wordAtLevel (period : ℝ) [Fact (0 < period)] {s q n : ℕ} (w : Fin n → Fin 4) (h : n + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerCylinderSobolevSpace.sumNorm period ((wordAtLevel period q n w h) u) = (EulerH6Pressure.SpatialJet.derivativeJet (EulerCylinderSobolevSpace.toJet period u) w h).sobolevNorm

The word-at-level norm equals the corresponding genuine derivative-jet norm.