Actual C∞ representatives obtained from all-order strong cylinder jets.

Smoothness of uniform limits of complete Fréchet derivative towers.

Full Fréchet tensor convergence from the genuine cylinder derivative words.

theorem EulerMollifierTensors.tensor_difference_le_word_sum (period : ℝ) (m : ℕ) (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) (z : EulerSobolev.Domain 4) : ‖iteratedFDeriv ℝ m (EulerCylinderSobolev.euclideanLift period f x) z - iteratedFDeriv ℝ m (EulerCylinderSobolev.euclideanLift period g x) z‖ ≤ ∑ w : Fin m → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative period w f (EulerCylinderCoordinates.euclideanCover period z + x) - EulerCylinderSobolev.iteratedFieldDerivative period w g (EulerCylinderCoordinates.euclideanCover period z + x)‖

The operator norm of a difference of derivative tensors is controlled by the finite coordinate sum.

theorem EulerMollifierTensors.tensor_uniformCauchy_of_words (period : ℝ) (m : ℕ) (f : ℕ → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (k : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (f k) x)) (hC : ∀ (w : Fin m → Fin 4), UniformCauchySeqOn (fun (k : ℕ) => EulerCylinderSobolev.iteratedFieldDerivative period w (f k)) Filter.atTop Set.univ) (x : EulerLiftedGradientSpace.LiftDomain period) : UniformCauchySeqOn (fun (k : ℕ) => iteratedFDeriv ℝ m (EulerCylinderSobolev.euclideanLift period (f k) x)) Filter.atTop Set.univ

Uniform Cauchy convergence of every coordinate word gives uniform Cauchy convergence of the full tensor.

Smooth Uniform Limit

theorem EulerSmoothUniformLimit.contDiff_of_derivative_tower {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℕ → Type u_2} [(n : ℕ) → NormedAddCommGroup (F n)] [(n : ℕ) → NormedSpace ℝ (F n)] (J : (n : ℕ) → E → F n) (L : (n : ℕ) → F (n + 1) →L[ℝ] E →L[ℝ] F n) (hJ : ∀ (n : ℕ) (x : E), HasFDerivAt (J n) ((L n) (J (n + 1) x)) x) (n : ℕ) : ContDiff ℝ (↑⊤) (J n)

An infinite compatible derivative tower is smooth at every level.

theorem EulerSmoothUniformLimit.contDiff_of_uniform_derivative_limits {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℕ → Type u_2} [(n : ℕ) → NormedAddCommGroup (F n)] [(n : ℕ) → NormedSpace ℝ (F n)] (f : (n : ℕ) → ℕ → E → F n) (J : (n : ℕ) → E → F n) (L : (n : ℕ) → F (n + 1) →L[ℝ] E →L[ℝ] F n) (hf : ∀ (n k : ℕ) (x : E), HasFDerivAt (f n k) ((L n) (f (n + 1) k x)) x) (hlim : ∀ (n : ℕ), TendstoUniformly (f n) (J n) Filter.atTop) (n : ℕ) : ContDiff ℝ (↑⊤) (J n)

Uniform limits of a compatible smooth derivative tower are again smooth. This is the completion step for Sobolev mollifications.

theorem EulerSmoothUniformLimit.exists_smooth_limit_of_uniform_cauchy_tower {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℕ → Type u_2} [(n : ℕ) → NormedAddCommGroup (F n)] [(n : ℕ) → NormedSpace ℝ (F n)] [∀ (n : ℕ), CompleteSpace (F n)] (f : (n : ℕ) → ℕ → E → F n) (L : (n : ℕ) → F (n + 1) →L[ℝ] E →L[ℝ] F n) (hf : ∀ (n k : ℕ) (x : E), HasFDerivAt (f n k) ((L n) (f (n + 1) k x)) x) (hC : ∀ (n : ℕ), UniformCauchySeqOn (f n) Filter.atTop Set.univ) : ∃ (J : (n : ℕ) → E → F n), (∀ (n : ℕ), TendstoUniformly (f n) (J n) Filter.atTop) ∧ ∀ (n : ℕ), ContDiff ℝ (↑⊤) (J n)

Completeness constructs every limit in a uniformly Cauchy derivative tower; the limit and all of its compatible derivatives are smooth.

theorem EulerSmoothTensorLimit.exists_smooth_limit {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : ℕ → E → F) (hf : ∀ (k : ℕ), ContDiff ℝ (↑⊤) (f k)) (hC : ∀ (m : ℕ), UniformCauchySeqOn (fun (k : ℕ) => iteratedFDeriv ℝ m (f k)) Filter.atTop Set.univ) : ∃ (g : E → F), TendstoUniformly f g Filter.atTop ∧ ContDiff ℝ (↑⊤) g

A uniformly Cauchy sequence at every actual Fréchet derivative order has a genuine smooth limit.

theorem EulerSmoothTensorLimit.cylinder_smooth_of_uniformCauchy_words (period : ℝ) (f : ℕ → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (k : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (f k) x)) (hC : ∀ (m : ℕ) (w : Fin m → Fin 4), UniformCauchySeqOn (fun (k : ℕ) => EulerCylinderSobolev.iteratedFieldDerivative period w (f k)) Filter.atTop Set.univ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hpoint : ∀ (y : EulerLiftedGradientSpace.LiftDomain period), Filter.Tendsto (fun (k : ℕ) => f k y) Filter.atTop (nhds (g y))) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)

A pointwise cylinder limit is C∞ when every coordinate derivative word is uniformly Cauchy.

theorem EulerSmoothPressureRepresentative.exists_smooth_representative (period : ℝ) [Fact (0 < period)] (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : (s : ℕ) → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) : ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) ∧ ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g

All-order strong cylinder jets produce an actual C∞ representative of the L² field.

theorem EulerSmoothPressureRepresentative.exists_smooth_pressure (period : ℝ) [Fact (0 < period)] (A : EulerSpatialSobolevInverse.SmoothCoefficient period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (K : (s : ℕ) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (J : (s : ℕ) → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) : ∃ (p : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period p x)) ∧ ↑↑(A.pressure κ m c hc hpos f) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] p

The genuine coercive pressure inverse has a C∞ representative when its actual coefficients and forcing possess strong derivative jets at every finite order.