Genuine heat regularizations of the constructed mild solution satisfy the differentiated heat equation.

Exact heat commutation with the genuine Sobolev derivatives and Laplacian.

theorem EulerSobolevLaplacian.derivative_heat (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerCylinderSobolevSpace.derivativeOperator period q i) ((EulerSobolevHeat.heatOperator period (q + 1) v) u) = (EulerSobolevHeat.heatOperator period q v) ((EulerCylinderSobolevSpace.derivativeOperator period q i) u)

Actual heat commutes with every strong coordinate derivative between consecutive Sobolev levels.

theorem EulerSobolevLaplacian.laplacian_heat (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 2))) : (laplacianOperator period q) ((EulerSobolevHeat.heatOperator period (q + 2) v) u) = (EulerSobolevHeat.heatOperator period q v) ((laplacianOperator period q) u)

Actual heat commutes with the genuine Laplacian between Sobolev levels.

noncomputable def EulerRegularizedMildEquation.regularizedState (period : ℝ) [Fact (0 < period)] (T : ℝ) (n : ℕ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))

The actual three-derivative heat regularization of an H¹ mild state.

Equations

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

noncomputable def EulerRegularizedMildEquation.regularizedForcing (period : ℝ) [Fact (0 < period)] (T : ℝ) (n : ℕ) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))

The same genuine heat regularization of the source, retained at the gradient-energy source order.

Equations

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

theorem EulerRegularizedMildEquation.regularizedState_low_eq (period : ℝ) [Fact (0 < period)] (T : ℝ) (n : ℕ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period regularizedForcing._proof_1)) (regularizedState period T n u) = EulerHeatRegularizedPaths.pathHeat period 1 T (EulerHeatRegularizedPaths.regularizerVariance n) u

The original-order restriction of the regularized state is exactly the actual H¹ heat path.

theorem EulerRegularizedMildEquation.regularizedState_low_tendsto (period : ℝ) [Fact (0 < period)] (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period regularizedForcing._proof_1)) (regularizedState period T n u)) Filter.atTop (nhds u)

The regularized state converges uniformly in its original actual H¹ topology.

theorem EulerRegularizedMildEquation.regularizedForcing_value_eq (period : ℝ) [Fact (0 < period)] (T : ℝ) (n : ℕ) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 1)) (regularizedForcing period T n f) = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 0)) (EulerHeatRegularizedPaths.pathHeat period 0 T (EulerHeatRegularizedPaths.regularizerVariance n) f)

The source's actual L² value is regularized by the same genuine heat operator.

theorem EulerRegularizedMildEquation.regularizedForcing_value_tendsto (period : ℝ) [Fact (0 < period)] (T : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 1)) (regularizedForcing period T n f)) Filter.atTop (nhds ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 0)) f))

The regularized forcing converges uniformly in actual L², with no source derivative premise.

noncomputable def EulerRegularizedMildEquation.regularizerFirst (period : ℝ) [Fact (0 < period)] (n : ℕ) (i : Fin 4) : ↥(EulerCylinderSobolevSpace.SobolevSpace period 0) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)

The first derivative of the genuine regularizer, as a bounded heat-commuting block.

Equations

• EulerRegularizedMildEquation.regularizerFirst period n i = EulerCylinderSobolevSpace.derivativeOperator period 2 i ∘SL EulerHeatRegularizedPaths.heatRegularizer period 0 n

theorem EulerRegularizedMildEquation.regularizerFirst_heat (period : ℝ) [Fact (0 < period)] (n : ℕ) (i : Fin 4) (v : NNReal) (x : ↥(EulerCylinderSobolevSpace.SobolevSpace period 0)) : (regularizerFirst period n i) ((EulerSobolevHeat.heatOperator period 0 v) x) = (EulerSobolevHeat.heatOperator period 2 v) ((regularizerFirst period n i) x)

The regularized first-derivative block commutes with actual heat.

theorem EulerRegularizedMildEquation.regularizerFirst_laplacian (period : ℝ) [Fact (0 < period)] (n : ℕ) (i : Fin 4) (x : ↥(EulerCylinderSobolevSpace.SobolevSpace period 0)) : (EulerSobolevHeatGenerator.laplacianEvaluation period 2 regularizerFirst_laplacian._proof_1) ((regularizerFirst period n i) x) = EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) ((EulerSobolevLaplacian.laplacianOperator period 1) ((EulerHeatRegularizedPaths.heatRegularizer period 0 n) x)))

The regularized first derivative has the exact commuting Laplacian value.

theorem EulerRegularizedMildEquation.regularizerFirst_source (period : ℝ) [Fact (0 < period)] (n : ℕ) (i : Fin 4) (x : ↥(EulerCylinderSobolevSpace.SobolevSpace period 0)) : EulerCylinderSobolevSpace.value period ((regularizerFirst period n i) x) = EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) ((EulerCylinderSobolevSpace.restrictOperator period regularizedForcing._proof_1) ((EulerHeatRegularizedPaths.heatRegularizer period 0 n) x)))

Restriction preserves the source's regularized first derivative exactly.

theorem EulerRegularizedMildEquation.value_derivative_smul_add (period : ℝ) [Fact (0 < period)] (i : Fin 4) (ν : ℝ) (a b : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • a + b)) = ν • EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) a) + EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) b)

Actual derivative evaluation is linear in a scaled sum.

theorem EulerRegularizedMildEquation.regularizerFirst_rhs (period : ℝ) [Fact (0 < period)] (n : ℕ) (i : Fin 4) (ν : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (f : ↥(EulerCylinderSobolevSpace.SobolevSpace period 0)) : ν • (EulerSobolevHeatGenerator.laplacianEvaluation period 2 regularizerFirst_laplacian._proof_1) ((regularizerFirst period n i) ((EulerCylinderSobolevSpace.truncateOperator period 0) u)) + EulerCylinderSobolevSpace.value period ((regularizerFirst period n i) f) = EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) ((EulerHeatRegularizedPaths.heatRegularizer period 0 n) ((EulerCylinderSobolevSpace.truncateOperator period 0) u)) + (EulerCylinderSobolevSpace.restrictOperator period regularizedForcing._proof_1) ((EulerHeatRegularizedPaths.heatRegularizer period 0 n) f)))

The exact algebraic form of the regularized first-word heat right-hand side.

theorem EulerRegularizedMildEquation.regularizedState_first_time_derivative (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period 1 (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period 0 ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) (n : ℕ) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (i : Fin 4) : HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT (regularizedState period T n u) s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT (regularizedState period T n u) t) + EulerVolterraConvolution.extendPath T hT (regularizedForcing period T n f) t))) t

Every genuine spatial heat regularization of the actual mild solution satisfies the first-word heat equation used in maximal regularity.