Smooth mollifications are dense in every actual complete cylinder Sobolev space.

noncomputable def EulerCylinderSobolevSpace.sobolevMollifier (period : ℝ) [Fact (0 < period)] (q n : ℕ) : ↥(SobolevSpace period q) →L[ℝ] ↥(SobolevSpace period q)

Actual smooth convolution lifted to the complete Sobolev space.

Equations

• EulerCylinderSobolevSpace.sobolevMollifier period q n = EulerCylinderSobolevSpace.liftOperator period q (EulerCylinderMollifier.mollifierOperator period n) ⋯

@[simp]

theorem EulerCylinderSobolevSpace.sobolevMollifier_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(SobolevSpace period q)) (w : SobolevWord q) : ↑((sobolevMollifier period q n) u) w = EulerCylinderMollifier.mollify period n (↑u w)

Every derivative coordinate is mollified by the same actual convolution.

theorem EulerCylinderSobolevSpace.sobolevMollifier_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(SobolevSpace period q)) : ‖(sobolevMollifier period q n) u‖ ≤ ‖u‖

The smooth convolution is contractive in every complete Sobolev norm.

theorem EulerCylinderSobolevSpace.sobolevMollifier_tendsto (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(SobolevSpace period q)) : Filter.Tendsto (fun (n : ℕ) => (sobolevMollifier period q n) u) Filter.atTop (nhds u)

The same genuine smooth convolutions converge in the complete Sobolev topology.

theorem EulerCylinderSobolevSpace.sobolevMollifier_representative (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(SobolevSpace period q)) : ↑↑(value period ((sobolevMollifier period q n) u)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerMollifierRepresentative.smoothMollifier period n (value period u)

Every Sobolev mollification has the concrete smooth convolution as an almost-everywhere representative.

theorem EulerCylinderSobolevSpace.sobolevMollifier_word_ae (period : ℝ) [Fact (0 < period)] {q k : ℕ} (hk : k ≤ q) (n : ℕ) (u : ↥(SobolevSpace period q)) (w : Fin k → Fin 4) : ↑↑(word period ((sobolevMollifier period q n) u) hk w) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerCylinderSobolev.iteratedFieldDerivative period w (EulerMollifierRepresentative.smoothMollifier period n (value period u))

The smooth representative of a Sobolev mollifier has exactly the expected classical derivative coordinates.

theorem EulerCylinderSobolevSpace.smooth_representatives_dense (period : ℝ) [Fact (0 < period)] (q : ℕ) : Dense {u : ↥(SobolevSpace period q) | ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)}

Fields with actual smooth cylinder representatives are dense in the complete Sobolev space.