Strong L² derivatives of smooth representatives are their actual classical derivatives.

theorem EulerStrongSmoothJet.lp_derivative_ae {X : Type u_1} {F : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [NormedAddCommGroup F] [NormedSpace ℝ F] (U : ℝ → ↥(MeasureTheory.Lp F 2 μ)) (V : ↥(MeasureTheory.Lp F 2 μ)) (u : ℝ → X → F) (v : X → F) (hrep : ∀ (t : ℝ), ↑↑(U t) =ᵐ[μ] u t) (hU : HasDerivAt U V 0) (hu : ∀ (x : X), HasDerivAt (fun (t : ℝ) => u t x) (v x) 0) : ↑↑V =ᵐ[μ] v

A strong L² derivative agrees almost everywhere with a pointwise derivative. The proof extracts an almost-everywhere convergent subsequence of the difference quotients.

theorem EulerStrongSmoothJet.pointwise_translation_hasDerivAt (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : HasDerivAt (fun (t : ℝ) => f (x + EulerPressureSpatialRegularity.translationPath period a t)) (EulerTransportDerivatives.fieldDerivative period a f x) 0

The pointwise translation orbit of a smooth cylinder field has its actual directional derivative.

theorem EulerStrongSmoothJet.translation_derivative_ae (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (U V : ↥(EulerLiftedGradientSpace.LiftL2 period)) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hD : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) U) V 0) : ↑↑V =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerTransportDerivatives.fieldDerivative period a f

Any strong translation derivative of a smooth representative is its classical derivative, without compactness or a priori integrability of that classical derivative.

theorem EulerStrongSmoothJet.jet_word_ae (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : ↑↑(J.word w) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerCylinderSobolev.iteratedFieldDerivative period w f

Every word of a strong Sobolev jet agrees with the actual classical word of a smooth representative.

theorem EulerStrongSmoothJet.jet_classical_memLp (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)

Strong jets force all actual classical derivatives through the corresponding order to lie in L².

theorem EulerStrongSmoothJet.jet_sobolevNorm_eq (period : ℝ) [Fact (0 < period)] {s : ℕ} (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : J.sobolevNorm = EulerCylinderSobolev.liftSobolevNorm period s f

The strong Sobolev jet norm is exactly the classical derivative Sobolev norm for any smooth representative.