Genuine approximate identities for the lifted L² translation representation.

theorem EulerCylinderMollifier.translation_continuous (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Continuous fun (a : EulerLiftedGradientSpace.LiftDomain period) => (EulerLiftedGradientSpace.translation period a) f

Actual cylinder translations act strongly continuously on L².

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

theorem EulerCylinderMollifier.euclideanCover_add (period : ℝ) (x y : EulerSobolev.Domain 4) : EulerCylinderCoordinates.euclideanCover period (x + y) = EulerCylinderCoordinates.euclideanCover period x + EulerCylinderCoordinates.euclideanCover period y

theorem EulerCylinderMollifier.euclideanCover_zero (period : ℝ) : EulerCylinderCoordinates.euclideanCover period 0 = 0

noncomputable def EulerCylinderMollifier.orbit (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (x : EulerSobolev.Domain 4) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual L² translation orbit in Euclidean covering coordinates.

Equations

• EulerCylinderMollifier.orbit period f x = (EulerLiftedGradientSpace.translation period (EulerCylinderCoordinates.euclideanCover period x)) f

theorem EulerCylinderMollifier.orbit_continuous (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Continuous (orbit period f)

@[simp]

theorem EulerCylinderMollifier.orbit_zero (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : orbit period f 0 = f

theorem EulerCylinderMollifier.orbit_norm (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (x : EulerSobolev.Domain 4) : ‖orbit period f x‖ = ‖f‖

noncomputable def EulerCylinderMollifier.mollifierBump (n : ℕ) : ContDiffBump 0

A normalized approximate-identity bump with radii tending to zero.

Equations

• EulerCylinderMollifier.mollifierBump n = { rIn := EulerNoncompactTransport.cutoffScale n, rOut := 2 * EulerNoncompactTransport.cutoffScale n, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def EulerCylinderMollifier.mollifierKernel (n : ℕ) : EulerSobolev.Domain 4 → ℝ

The real smooth compact approximate-identity kernel.

Equations

• EulerCylinderMollifier.mollifierKernel n = (EulerCylinderMollifier.mollifierBump n).normed MeasureTheory.volume

theorem EulerCylinderMollifier.mollifierKernel_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (mollifierKernel n)

theorem EulerCylinderMollifier.mollifierKernel_compact (n : ℕ) : HasCompactSupport (mollifierKernel n)

theorem EulerCylinderMollifier.mollifierKernel_nonneg (n : ℕ) (x : EulerSobolev.Domain 4) : 0 ≤ mollifierKernel n x

theorem EulerCylinderMollifier.mollifierKernel_integral (n : ℕ) : ∫ (x : EulerSobolev.Domain 4), mollifierKernel n x = 1

noncomputable def EulerCylinderMollifier.smoothOrbit (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : EulerSobolev.Domain 4 → ↥(EulerLiftedGradientSpace.LiftL2 period)

Bochner convolution of the actual L² orbit with the smooth approximate identity.

Equations

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

noncomputable def EulerCylinderMollifier.mollify (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual L² mollification; its expected representative is the classical periodic convolution.

Equations

• EulerCylinderMollifier.mollify period n f = EulerCylinderMollifier.smoothOrbit period n f 0

theorem EulerCylinderMollifier.smoothOrbit_contDiff (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ContDiff ℝ (↑⊤) (smoothOrbit period n f)

theorem EulerCylinderMollifier.mollify_tendsto (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Filter.Tendsto (fun (n : ℕ) => mollify period n f) Filter.atTop (nhds f)

These actual smoothings converge strongly in the genuine cylinder L² space.

theorem EulerCylinderMollifier.mollify_eq_integral (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : mollify period n f = ∫ (y : EulerSobolev.Domain 4), mollifierKernel n y • orbit period f (-y)

theorem EulerCylinderMollifier.kernel_orbit_integrable (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : MeasureTheory.Integrable (fun (y : EulerSobolev.Domain 4) => mollifierKernel n y • orbit period f (-y)) MeasureTheory.volume

theorem EulerCylinderMollifier.mollify_norm_le (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖mollify period n f‖ ≤ ‖f‖

Smoothing is contractive in the actual cylinder L² norm.

theorem EulerCylinderMollifier.mollify_add (period : ℝ) [Fact (0 < period)] (n : ℕ) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) : mollify period n (f + g) = mollify period n f + mollify period n g

theorem EulerCylinderMollifier.mollify_smul (period : ℝ) [Fact (0 < period)] (n : ℕ) (c : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : mollify period n (c • f) = c • mollify period n f

noncomputable def EulerCylinderMollifier.mollifierLinearMap (period : ℝ) [Fact (0 < period)] (n : ℕ) : ↥(EulerLiftedGradientSpace.LiftL2 period) →ₗ[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual linear averaging map associated with a smooth compact kernel.

Equations

• EulerCylinderMollifier.mollifierLinearMap period n = { toFun := EulerCylinderMollifier.mollify period n, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerCylinderMollifier.mollifierOperator (period : ℝ) [Fact (0 < period)] (n : ℕ) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The bounded L² approximate-identity operator, with operator norm at most one.

Equations

• EulerCylinderMollifier.mollifierOperator period n = (EulerCylinderMollifier.mollifierLinearMap period n).mkContinuous 1 ⋯

theorem EulerCylinderMollifier.mollifierOperator_apply (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (mollifierOperator period n) f = mollify period n f

theorem EulerCylinderMollifier.mollifierOperator_norm_le (period : ℝ) [Fact (0 < period)] (n : ℕ) : ‖mollifierOperator period n‖ ≤ 1

theorem EulerCylinderMollifier.mollify_translation (period : ℝ) [Fact (0 < period)] (n : ℕ) (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerLiftedGradientSpace.translation period a) (mollify period n f) = mollify period n ((EulerLiftedGradientSpace.translation period a) f)

The averaging operator commutes with every actual spatial or angular translation.

noncomputable def EulerCylinderMollifier.mollifyJet (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (n : ℕ) : EulerSpatialSobolevInverse.SpatialJet period directions s (mollify period n f)

Smoothing produces actual strong Sobolev jets and commutes with every derivative word.

Equations

• EulerCylinderMollifier.mollifyJet period J n = EulerPressureJetIdentities.SpatialJet.map (EulerCylinderMollifier.mollifierOperator period n) ⋯ J

theorem EulerCylinderMollifier.mollifyJet_word (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s k : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (n : ℕ) (w : Fin k → Fin 4) : (mollifyJet period J n).word w = mollify period n (J.word w)

theorem EulerCylinderMollifier.mollifyJet_word_tendsto (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s k : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (w : Fin k → Fin 4) : Filter.Tendsto (fun (n : ℕ) => (mollifyJet period J n).word w) Filter.atTop (nhds (J.word w))

Every finite actual derivative word converges strongly under the same mollification.

theorem EulerCylinderMollifier.sub_word (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s k : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (K : EulerSpatialSobolevInverse.SpatialJet period directions s g) (w : Fin k → Fin 4) : (J.sub K).word w = J.word w - K.word w

theorem EulerCylinderMollifier.mollifyJet_sobolevNorm_tendsto (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) : Filter.Tendsto (fun (n : ℕ) => ((mollifyJet period J n).sub J).sobolevNorm) Filter.atTop (nhds 0)

The same genuine mollifiers converge in every finite Sobolev jet norm.

theorem EulerCylinderMollifier.smoothOrbit_eq_orbit_mollify (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (x : EulerSobolev.Domain 4) : smoothOrbit period n f x = orbit period (mollify period n f) x

The smooth Hilbert-valued convolution is exactly the translation orbit of the mollified field.

theorem EulerCylinderMollifier.mollify_orbit_contDiff (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ContDiff ℝ (↑⊤) (orbit period (mollify period n f))

Mollification produces C∞ vectors for the genuine L² translation representation.

theorem EulerCylinderMollifier.mollify_diagonal_sequence (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : (s : ℕ) → EulerSpatialSobolevInverse.SpatialJet period directions s f) : ∃ (index : ℕ → ℕ), (∀ (n : ℕ), n ≤ index n) ∧ ∀ (n s : ℕ), s ≤ n → ((mollifyJet period (J s) (index n)).sub (J s)).sobolevNorm ≤ (1 / 2) ^ n

A single sequence of genuine mollifiers approximates every derivative order with geometrically small errors once that order has entered the diagonal.