Actual classical smooth representatives of the strong L² cylinder mollifiers.

Classical smooth cylinder representatives obtained by Euclidean mollification.

theorem EulerCoverMollification.euclideanCover_add (period : ℝ) (z w : EulerSobolev.Domain 4) : EulerCylinderCoordinates.euclideanCover period (z + w) = EulerCylinderCoordinates.euclideanCover period z + EulerCylinderCoordinates.euclideanCover period w

theorem EulerCoverMollification.euclideanCover_sub (period : ℝ) (z w : EulerSobolev.Domain 4) : EulerCylinderCoordinates.euclideanCover period (z - w) = EulerCylinderCoordinates.euclideanCover period z - EulerCylinderCoordinates.euclideanCover period w

theorem EulerCoverMollification.euclideanCover_surjective (period : ℝ) : Function.Surjective (EulerCylinderCoordinates.euclideanCover period)

theorem EulerCoverMollification.locallyIntegrable_cover (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.LocallyIntegrable (f ∘ EulerCylinderCoordinates.euclideanCover period) MeasureTheory.volume

L² cylinder fields have locally integrable periodic lifts to the Euclidean covering space.

noncomputable def EulerCoverMollification.coverConvolution (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : ContDiffBump 0) (f : EulerLiftedGradientSpace.LiftDomain period → F) : EulerSobolev.Domain 4 → F

Euclidean convolution of the periodic lift with a normalized compact bump.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerCoverMollification.cylinderConvolution (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : ContDiffBump 0) (f : EulerLiftedGradientSpace.LiftDomain period → F) (x : EulerLiftedGradientSpace.LiftDomain period) : F

The same convolution defined directly on the cylinder, with the usual negative translation.

Equations

• EulerCoverMollification.cylinderConvolution period φ f x = ∫ (y : EulerSobolev.Domain 4), φ.normed MeasureTheory.volume y • f (x - EulerCylinderCoordinates.euclideanCover period y)

theorem EulerCoverMollification.cylinderConvolution_cover (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : ContDiffBump 0) (f : EulerLiftedGradientSpace.LiftDomain period → F) (z : EulerSobolev.Domain 4) : cylinderConvolution period φ f (EulerCylinderCoordinates.euclideanCover period z) = coverConvolution period φ f z

theorem EulerCoverMollification.coverConvolution_smooth (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : ContDiffBump 0) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) : ContDiff ℝ (↑⊤) (coverConvolution period φ f)

The classical covering-space convolution is genuinely C∞.

theorem EulerCoverMollification.cylinderConvolution_smooth (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : ContDiffBump 0) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (cylinderConvolution period φ f) x)

The convolution descends to a C∞ cylinder field in the actual local covering coordinates.

theorem EulerCoverMollification.coverConvolution_periodic (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : ContDiffBump 0) (f : EulerLiftedGradientSpace.LiftDomain period → F) : Function.Periodic (coverConvolution period φ f) (EuclideanSpace.single 0 period)

The covering-space convolution is periodic in the angular direction.

theorem EulerCoverMollification.ae_coverConvolution_tendsto (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {φ : ℕ → ContDiffBump 0} (hφ : Filter.Tendsto (fun (n : ℕ) => (φ n).rOut) Filter.atTop (nhds 0)) (hshape : ∀ᶠ (n : ℕ) in Filter.atTop, (φ n).rOut ≤ 2 * (φ n).rIn) (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) : ∀ᵐ (z : EulerSobolev.Domain 4), Filter.Tendsto (fun (n : ℕ) => coverConvolution period (φ n) f z) Filter.atTop (nhds (f (EulerCylinderCoordinates.euclideanCover period z)))

Normalized shrinking bump convolutions recover the original covering-space function almost everywhere.

The finite-set Fubini bridge identifying classical and L² cylinder mollification.

theorem EulerCoverMollificationFubini.finite_set_integral_norm_le (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) (K : Set (EulerLiftedGradientSpace.LiftDomain period)) (hK : (EulerLiftedGradientSpace.liftMeasure period) K < ⊤) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period) in K, ‖f x‖ ∂EulerLiftedGradientSpace.liftMeasure period ≤ (MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal * ((EulerLiftedGradientSpace.liftMeasure period) K).toReal ^ (1 / 2)

The elementary L²-to-L¹ bound on an arbitrary finite-measure set.

theorem EulerCoverMollificationFubini.euclideanCover_continuous (period : ℝ) : Continuous (EulerCylinderCoordinates.euclideanCover period)

The Euclidean covering map is continuous.

theorem EulerCoverMollificationFubini.kernel_integrable_prod (period : ℝ) [Fact (0 < period)] (φ : ContDiffBump 0) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (K : Set (EulerLiftedGradientSpace.LiftDomain period)) (hK : (EulerLiftedGradientSpace.liftMeasure period) K < ⊤) : MeasureTheory.Integrable (fun (p : EulerSobolev.Domain 4 × EulerLiftedGradientSpace.LiftDomain period) => φ.normed MeasureTheory.volume p.1 • ↑↑U (p.2 - EulerCylinderCoordinates.euclideanCover period p.1)) (MeasureTheory.volume.prod ((EulerLiftedGradientSpace.liftMeasure period).restrict K))

The convolution kernel is jointly integrable over the kernel variable and any finite cylinder set.

theorem EulerCoverMollificationFubini.cylinderConvolution_integrableOn (period : ℝ) [Fact (0 < period)] (φ : ContDiffBump 0) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (K : Set (EulerLiftedGradientSpace.LiftDomain period)) (hK : (EulerLiftedGradientSpace.liftMeasure period) K < ⊤) : MeasureTheory.IntegrableOn (EulerCoverMollification.cylinderConvolution period φ ↑↑U) K (EulerLiftedGradientSpace.liftMeasure period)

The classical cylinder convolution is integrable on each finite-measure set.

theorem EulerCoverMollificationFubini.setIntegral_cylinderConvolution (period : ℝ) [Fact (0 < period)] (φ : ContDiffBump 0) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (K : Set (EulerLiftedGradientSpace.LiftDomain period)) (hK : (EulerLiftedGradientSpace.liftMeasure period) K < ⊤) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period) in K, EulerCoverMollification.cylinderConvolution period φ (↑↑U) x ∂EulerLiftedGradientSpace.liftMeasure period = ∫ (y : EulerSobolev.Domain 4), φ.normed MeasureTheory.volume y • ∫ (x : EulerLiftedGradientSpace.LiftDomain period) in K, ↑↑U (x - EulerCylinderCoordinates.euclideanCover period y) ∂EulerLiftedGradientSpace.liftMeasure period

Exact Fubini identity for every finite cylinder set.

theorem EulerCoverMollificationFubini.ae_eq_cylinderConvolution_of_setIntegrals (period : ℝ) [Fact (0 < period)] (φ : ContDiffBump 0) (U V : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hV : ∀ (K : Set (EulerLiftedGradientSpace.LiftDomain period)), MeasurableSet K → (EulerLiftedGradientSpace.liftMeasure period) K < ⊤ → ∫ (x : EulerLiftedGradientSpace.LiftDomain period) in K, ↑↑V x ∂EulerLiftedGradientSpace.liftMeasure period = ∫ (y : EulerSobolev.Domain 4), φ.normed MeasureTheory.volume y • ∫ (x : EulerLiftedGradientSpace.LiftDomain period) in K, ↑↑U (x - EulerCylinderCoordinates.euclideanCover period y) ∂EulerLiftedGradientSpace.liftMeasure period) : ↑↑V =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerCoverMollification.cylinderConvolution period φ ↑↑U

Equality of finite-set integrals identifies a Bochner L² mollifier with the classical smooth field.

noncomputable def EulerMollifierRepresentative.smoothMollifier (period : ℝ) [Fact (0 < period)] (n : ℕ) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3

The concrete classical convolution representing the Bochner L² mollifier.

Equations

• EulerMollifierRepresentative.smoothMollifier period n U = EulerCoverMollification.cylinderConvolution period (EulerCylinderMollifier.mollifierBump n) ↑↑U

theorem EulerMollifierRepresentative.mollify_ae_smoothMollifier (period : ℝ) [Fact (0 < period)] (n : ℕ) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↑↑(EulerCylinderMollifier.mollify period n U) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] smoothMollifier period n U

The smooth convolution and the Bochner convolution are the same almost everywhere.

theorem EulerMollifierRepresentative.smoothMollifier_smooth (period : ℝ) [Fact (0 < period)] (n : ℕ) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (smoothMollifier period n U) x)

Every strong L² mollifier has an actual C∞ representative on the cylinder.

theorem EulerMollifierRepresentative.smoothMollifier_word_ae (period : ℝ) [Fact (0 < period)] {s k : ℕ} (hk : k ≤ s) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (n : ℕ) (w : Fin k → Fin 4) : ↑↑(EulerCylinderMollifier.mollify period n (J.word w)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerCylinderSobolev.iteratedFieldDerivative period w (smoothMollifier period n U)

Strong mollified jets are precisely the classical derivatives of the smooth convolution.

theorem EulerMollifierRepresentative.smoothMollifier_word_memLp (period : ℝ) [Fact (0 < period)] {s k : ℕ} (hk : k ≤ s) (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (n : ℕ) (w : Fin k → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (smoothMollifier period n U)) 2 (EulerLiftedGradientSpace.liftMeasure period)

All available classical derivatives of the smooth mollifier are genuinely in L².

theorem EulerMollifierRepresentative.smoothMollifier_sobolevNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (U : ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (n : ℕ) : (EulerCylinderMollifier.mollifyJet period J n).sobolevNorm = EulerCylinderSobolev.liftSobolevNorm period s (smoothMollifier period n U)

The strong and classical Sobolev norms of each mollifier agree exactly.