Genuine heat regularization of continuous Sobolev paths, uniformly in time.

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

A concrete three-derivative heat regularizer on the actual Sobolev scale.

Equations

• EulerHeatRegularizedPaths.heatRegularizer period q n = EulerCylinderSobolevSpace.heatGainThree period q (EulerCylinderSobolevSpace.smoothingVariance n) ⋯

noncomputable def EulerHeatRegularizedPaths.regularizerVariance (n : ℕ) : NNReal

The total actual Gaussian variance of the regularizer.

Equations

• EulerHeatRegularizedPaths.regularizerVariance n = EulerCylinderSobolevSpace.smoothingVariance n + (EulerCylinderSobolevSpace.smoothingVariance n + EulerCylinderSobolevSpace.smoothingVariance n)

theorem EulerHeatRegularizedPaths.regularizerVariance_tendsto : Filter.Tendsto regularizerVariance Filter.atTop (nhds 0)

The total regularizing variance tends to zero.

theorem EulerHeatRegularizedPaths.heatRegularizer_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((heatRegularizer period q n) u) = (EulerGaussianCylinderHeat.cylinderHeat period (regularizerVariance n)) (EulerCylinderSobolevSpace.value period u)

The regularizer has exactly its stated genuine L² heat value.

theorem EulerHeatRegularizedPaths.restrict_heatRegularizer (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerCylinderSobolevSpace.restrictOperator period ⋯) ((heatRegularizer period q n) u) = (EulerSobolevHeat.heatOperator period q (regularizerVariance n)) u

Forgetting the three extra derivatives gives the actual contractive heat evolution.

theorem EulerHeatRegularizedPaths.heatRegularizer_heat (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (heatRegularizer period q n) ((EulerSobolevHeat.heatOperator period q v) u) = (EulerSobolevHeat.heatOperator period (q + 3) v) ((heatRegularizer period q n) u)

The genuine regularizer commutes with actual heat.

noncomputable def EulerHeatRegularizedPaths.pathHeat (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (v : NNReal) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

Heat acting pointwise on a continuous Sobolev time path.

Equations

• EulerHeatRegularizedPaths.pathHeat period q T v u = EulerMildWordEquation.mapPath period T (EulerSobolevHeat.heatOperator period q v) u

theorem EulerHeatRegularizedPaths.pathHeat_continuous (period : ℝ) [Fact (0 < period)] {q : ℕ} (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : Continuous fun (v : NNReal) => pathHeat period q T v u

Strong heat continuity is uniform over every compact continuous time path.

noncomputable def EulerHeatRegularizedPaths.regularizedPath (period : ℝ) [Fact (0 < period)] {q : ℕ} (T : ℝ) (n : ℕ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3)))

A continuous path regularized by three genuine spatial heat derivatives.

Equations

• EulerHeatRegularizedPaths.regularizedPath period T n u = EulerMildWordEquation.mapPath period T (EulerHeatRegularizedPaths.heatRegularizer period q n) u

theorem EulerHeatRegularizedPaths.regularizedPath_tendsto (period : ℝ) [Fact (0 < period)] {q : ℕ} (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : Filter.Tendsto (fun (n : ℕ) => EulerMildWordEquation.mapPath period T (EulerCylinderSobolevSpace.restrictOperator period ⋯) (regularizedPath period T n u)) Filter.atTop (nhds u)

Regularized paths converge uniformly in their original complete Sobolev norm.

theorem EulerHeatRegularizedPaths.heatRegularizer_truncate (period : ℝ) [Fact (0 < period)] {q : ℕ} (n : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (heatRegularizer period q n) ((EulerCylinderSobolevSpace.truncateOperator period q) u) = (EulerCylinderSobolevSpace.restrictOperator period ⋯) ((heatRegularizer period (q + 1) n) u)

Regularization at adjacent Sobolev levels has exactly the same underlying field.