Uniform control of every classical derivative word by actual strong Sobolev jets.

theorem EulerMollifierUniform.word_H3_le_higher (period : ℝ) [Fact (0 < period)] {m : ℕ} (w : Fin m → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) : EulerCylinderSobolev.liftSobolevNorm period 3 (EulerCylinderSobolev.iteratedFieldDerivative period w f) ≤ 85 * EulerCylinderSobolev.liftSobolevNorm period (m + 3) f

An arbitrary derivative word has H³ norm controlled by the full norm three orders higher.

theorem EulerMollifierUniform.jet_word_pointwise_bound (period : ℝ) [Fact (0 < period)] {m : ℕ} (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection (m + 3) U) (w : Fin m → 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)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerCylinderSobolev.iteratedFieldDerivative period w f x‖ ≤ 3 * EulerCylinderSobolev.cylinderEmbeddingConstant period * (85 * J.sobolevNorm)

Every actual smooth derivative word is uniformly controlled by its genuine strong jet.

theorem EulerMollifierUniform.fieldDerivative_sub (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerTransportDerivatives.fieldDerivative period a (fun (y : EulerLiftedGradientSpace.LiftDomain period) => f y - g y) x = EulerTransportDerivatives.fieldDerivative period a f x - EulerTransportDerivatives.fieldDerivative period a g x

theorem EulerMollifierUniform.word_sub (period : ℝ) {m : ℕ} (w : Fin m → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : (EulerCylinderSobolev.iteratedFieldDerivative period w fun (y : EulerLiftedGradientSpace.LiftDomain period) => f y - g y) = fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerCylinderSobolev.iteratedFieldDerivative period w f x - EulerCylinderSobolev.iteratedFieldDerivative period w g x

theorem EulerMollifierUniform.jet_word_difference_bound (period : ℝ) [Fact (0 < period)] {m : ℕ} (U V : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection (m + 3) U) (K : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection (m + 3) V) (w : Fin m → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hrepG : ↑↑V =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerCylinderSobolev.iteratedFieldDerivative period w f x - EulerCylinderSobolev.iteratedFieldDerivative period w g x‖ ≤ 3 * EulerCylinderSobolev.cylinderEmbeddingConstant period * (85 * (J.sub K).sobolevNorm)

Uniform derivative differences are controlled by the actual L² Sobolev difference jet.

theorem EulerMollifierUniform.jet_sub_triangle (period : ℝ) [Fact (0 < period)] {s : ℕ} {U V W : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (K : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s V) (L : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s W) : (J.sub K).sobolevNorm ≤ (J.sub L).sobolevNorm + (K.sub L).sobolevNorm

A genuine Sobolev difference is bounded through any third jet at the same order.

theorem EulerMollifierUniform.smoothMollifier_word_uniformCauchy (period : ℝ) [Fact (0 < period)] {m : ℕ} (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection (m + 3) U) (w : Fin m → Fin 4) : UniformCauchySeqOn (fun (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) => EulerCylinderSobolev.iteratedFieldDerivative period w (EulerMollifierRepresentative.smoothMollifier period n U) x) Filter.atTop Set.univ

Every actual classical derivative word of the mollifiers is uniformly Cauchy.

theorem EulerMollifierUniform.exists_smoothMollifier_word_uniform_limit (period : ℝ) [Fact (0 < period)] {m : ℕ} (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection (m + 3) U) (w : Fin m → Fin 4) : ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), TendstoUniformly (fun (n : ℕ) => EulerCylinderSobolev.iteratedFieldDerivative period w (EulerMollifierRepresentative.smoothMollifier period n U)) g Filter.atTop

Completeness produces a uniform limit for every actual derivative word.

theorem EulerMollifierUniform.smoothMollifier_word_limit_ae (period : ℝ) [Fact (0 < period)] {m : ℕ} (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection (m + 3) U) (w : Fin m → Fin 4) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hlim : TendstoUniformly (fun (n : ℕ) => EulerCylinderSobolev.iteratedFieldDerivative period w (EulerMollifierRepresentative.smoothMollifier period n U)) g Filter.atTop) : ↑↑(J.word w) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g

The uniform classical word limit represents the actual strong L² derivative word.

theorem EulerMollifierUniform.exists_continuous_representative (period : ℝ) [Fact (0 < period)] (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 3 U) : ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), Continuous g ∧ ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g

Strong H³ cylinder jets have genuine continuous representatives.