Smooth high-regularity approximations converging contractively in the original Sobolev order.

noncomputable def EulerCylinderSobolevSpace.heatGainThree (period : ℝ) [Fact (0 < period)] (q : ℕ) (v : NNReal) (hv : 0 < v) : ↥(SobolevSpace period q) →L[ℝ] ↥(SobolevSpace period (q + 3))

Three successive genuine heat smoothing steps.

Equations

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

theorem EulerCylinderSobolevSpace.heatGainThree_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (hv : 0 < v) (u : ↥(SobolevSpace period q)) : value period ((heatGainThree period q v hv) u) = (EulerGaussianCylinderHeat.cylinderHeat period (v + (v + v))) (value period u)

Its underlying field is exactly heat evolution with three times the variance.

theorem EulerCylinderSobolevSpace.restrict_heatGainThree (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (hv : 0 < v) (u : ↥(SobolevSpace period q)) : (restrictOperator period ⋯) ((heatGainThree period q v hv) u) = (EulerSobolevHeat.heatOperator period q (v + (v + v))) u

Forgetting the three gained derivatives recovers the usual contractive heat operator.

noncomputable def EulerCylinderSobolevSpace.smoothingVariance (n : ℕ) : NNReal

A positive Gaussian scale tending to zero.

Equations

• EulerCylinderSobolevSpace.smoothingVariance n = (EulerNoncompactTransport.cutoffScale n).toNNReal

theorem EulerCylinderSobolevSpace.smoothingVariance_pos (n : ℕ) : 0 < smoothingVariance n

theorem EulerCylinderSobolevSpace.smoothingVariance_tendsto : Filter.Tendsto smoothingVariance Filter.atTop (nhds 0)

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

An approximation having three extra strong derivatives and an actual C∞ representative.

Equations

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

theorem EulerCylinderSobolevSpace.restrict_smoothApprox (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(SobolevSpace period q)) : (restrictOperator period ⋯) ((smoothApprox period q n) u) = (sobolevMollifier period q n) ((EulerSobolevHeat.heatOperator period q (smoothingVariance n + (smoothingVariance n + smoothingVariance n))) u)

Exact description of the approximation in its original Sobolev topology.

theorem EulerCylinderSobolevSpace.smoothApprox_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(SobolevSpace period q)) : ‖(restrictOperator period ⋯) ((smoothApprox period q n) u)‖ ≤ ‖u‖

The approximations are contractive at the original Sobolev order.

theorem EulerCylinderSobolevSpace.contractive_comp_dist {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (M : X →L[ℝ] X) (hM : ∀ (z : X), ‖M z‖ ≤ ‖z‖) (H u : X) : dist (M H) u ≤ dist H u + dist (M u) u

theorem EulerCylinderSobolevSpace.smoothApprox_dist (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(SobolevSpace period q)) : dist ((restrictOperator period ⋯) ((smoothApprox period q n) u)) u ≤ dist ((EulerSobolevHeat.heatOperator period q (smoothingVariance n + (smoothingVariance n + smoothingVariance n))) u) u + dist ((sobolevMollifier period q n) u) u

A useful perturbation bound for simultaneous heat and convolution regularization.

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

The smooth high-regularity approximations converge in the complete original Sobolev norm.

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

Each high-regularity approximation has a concrete smooth cylinder representative.