A bounded actual Laplacian evaluation and the genuine heat generator on finite Sobolev data.

The genuine cylinder heat semigroup solves the Laplacian evolution equation.

The Gaussian variance generator is one half of the genuine squared translation derivative.

noncomputable def EulerGaussianCylinderHeat.realLineHeat (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

A continuous real-parameter extension of the Gaussian average, constant for negative variance.

Equations

• EulerGaussianCylinderHeat.realLineHeat period a t f = ∫ (x : ℝ), EulerGaussianCylinderHeat.lineOrbit period a f (√t * x) ∂EulerGaussianCylinderHeat.gaussianMeasure 0 1

theorem EulerGaussianCylinderHeat.realLineHeat_eq (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) {t : ℝ} (ht : 0 ≤ t) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realLineHeat period a t f = lineHeat period a ⟨t, ht⟩ f

@[simp]

theorem EulerGaussianCylinderHeat.realLineHeat_zero (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realLineHeat period a 0 f = f

theorem EulerGaussianCylinderHeat.realLineHeat_continuous (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Continuous fun (t : ℝ) => realLineHeat period a t f

theorem EulerGaussianCylinderHeat.scaledOrbit_hasDerivAt (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : HasDerivAt (lineOrbit period a f) g 0) (x t : ℝ) (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => lineOrbit period a f (√s * x)) ((x / (2 * √t)) • lineOrbit period a g (√t * x)) t

The chain-rule derivative of a scaled orbit, before Gaussian integration.

theorem EulerGaussianCylinderHeat.realLineHeat_hasDerivAt_moment (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : HasDerivAt (lineOrbit period a f) g 0) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => realLineHeat period a s f) (∫ (x : ℝ), (x / (2 * √t)) • lineOrbit period a g (√t * x) ∂gaussianMeasure 0 1) t

Differentiation of the Gaussian average at positive variance is justified by an integrable first moment.

theorem EulerGaussianCylinderHeat.varianceMoment_eq_half_derivative (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) {t : ℝ} (ht : 0 < t) (g : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ∫ (x : ℝ), (x / (2 * √t)) • lineOrbit period a g (√t * x) ∂gaussianMeasure 0 1 = (1 / 2) • lineHeatDerivative period a ⟨t, ⋯⟩ g

Gaussian scaling rewrites the variance derivative as one half of the averaged orbit derivative.

theorem EulerGaussianCylinderHeat.realLineHeat_generator_pos (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f g h : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : HasDerivAt (lineOrbit period a f) g 0) (hDD : HasDerivAt (lineOrbit period a g) h 0) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => realLineHeat period a s f) ((1 / 2) • realLineHeat period a t h) t

At every positive variance, the generator is one half of the genuine second translation derivative.

theorem EulerGaussianCylinderHeat.realLineHeat_generator_zero (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f g h : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : HasDerivAt (lineOrbit period a f) g 0) (hDD : HasDerivAt (lineOrbit period a g) h 0) : HasDerivWithinAt (fun (s : ℝ) => realLineHeat period a s f) ((1 / 2) • h) (Set.Ici 0) 0

The generator formula also holds as a genuine right derivative at zero variance.

Differentiation of jointly continuous operator families without operator-norm differentiability.

theorem EulerStrongOperatorDerivative.slope_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : ℝ → E →L[ℝ] F) (u : ℝ → E) (t s : ℝ) : slope (fun (r : ℝ) => (A r) (u r)) t s = (A s) (slope u t s) + slope (fun (r : ℝ) => (A r) (u t)) t s

The exact slope decomposition for a varying bounded linear operator and a varying input.

theorem EulerStrongOperatorDerivative.hasDerivAt_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : ℝ → E →L[ℝ] F) (u : ℝ → E) (t : ℝ) (u' : E) (a' : F) (hu : HasDerivAt u u' t) (ha : HasDerivAt (fun (s : ℝ) => (A s) (u t)) a' t) (hc : ContinuousAt (fun (p : ℝ × E) => (A p.1) p.2) (t, u')) : HasDerivAt (fun (s : ℝ) => (A s) (u s)) ((A t) u' + a') t

A product rule requiring joint strong continuity only at the limiting derivative vector.

theorem EulerStrongOperatorDerivative.hasDerivWithinAt_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : ℝ → E →L[ℝ] F) (u : ℝ → E) (t : ℝ) (s : Set ℝ) (u' : E) (a' : F) (hu : HasDerivWithinAt u u' s t) (ha : HasDerivWithinAt (fun (r : ℝ) => (A r) (u t)) a' s t) (hc : ContinuousAt (fun (p : ℝ × E) => (A p.1) p.2) (t, u')) : HasDerivWithinAt (fun (r : ℝ) => (A r) (u r)) ((A t) u' + a') s t

The same product rule for a one-sided derivative.

theorem EulerGaussianCylinderHeat.realLineHeat_eq_toNNReal (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realLineHeat period a t f = lineHeat period a t.toNNReal f

The real extension is the nonnegative-variance heat operator evaluated at the positive part.

noncomputable def EulerGaussianCylinderHeat.realLineHeatOperator (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Real-parameter version of the actual bounded heat operator.

Equations

• EulerGaussianCylinderHeat.realLineHeatOperator period a t = EulerGaussianCylinderHeat.lineHeatOperator period a t.toNNReal

@[simp]

theorem EulerGaussianCylinderHeat.realLineHeatOperator_apply (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (realLineHeatOperator period a t) f = realLineHeat period a t f

theorem EulerGaussianCylinderHeat.realLineHeat_joint_continuous (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) : Continuous fun (p : ℝ × ↥(EulerLiftedGradientSpace.LiftL2 period)) => realLineHeat period a p.1 p.2

theorem EulerGaussianCylinderHeat.realLineHeat_varying_input (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (u : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (t : ℝ) (u' g h : ↥(EulerLiftedGradientSpace.LiftL2 period)) (ht : 0 < t) (hu : HasDerivAt u u' t) (hD : HasDerivAt (lineOrbit period a (u t)) g 0) (hDD : HasDerivAt (lineOrbit period a g) h 0) : HasDerivAt (fun (s : ℝ) => realLineHeat period a s (u s)) (realLineHeat period a t u' + (1 / 2) • realLineHeat period a t h) t

Product rule for the real heat operator applied to a differentiable input curve.

def EulerGaussianCylinderHeat.realHeatList (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The real extension of a finite commuting heat product.

Equations

• EulerGaussianCylinderHeat.realHeatList period [] t f = f
• EulerGaussianCylinderHeat.realHeatList period (a :: tail) t f = EulerGaussianCylinderHeat.realLineHeat period a t (EulerGaussianCylinderHeat.realHeatList period tail t f)

theorem EulerGaussianCylinderHeat.realHeatList_eq (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) {t : ℝ} (ht : 0 ≤ t) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realHeatList period directions t f = heatList period directions ⟨t, ht⟩ f

theorem EulerGaussianCylinderHeat.realLineHeat_add (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realLineHeat period a t (f + g) = realLineHeat period a t f + realLineHeat period a t g

theorem EulerGaussianCylinderHeat.realLineHeat_smul (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (t c : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realLineHeat period a t (c • f) = c • realLineHeat period a t f

theorem EulerGaussianCylinderHeat.realHeatList_add (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realHeatList period directions t (f + g) = realHeatList period directions t f + realHeatList period directions t g

theorem EulerGaussianCylinderHeat.realHeatList_smul (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (t c : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realHeatList period directions t (c • f) = c • realHeatList period directions t f

@[simp]

theorem EulerGaussianCylinderHeat.realHeatList_zero_field (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : realHeatList period directions t 0 = 0

@[simp]

theorem EulerGaussianCylinderHeat.realHeatList_zero_time (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realHeatList period directions 0 f = f

theorem EulerGaussianCylinderHeat.realHeatList_eq_toNNReal (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : realHeatList period directions t f = heatList period directions t.toNNReal f

theorem EulerGaussianCylinderHeat.realHeatList_continuous (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Continuous fun (t : ℝ) => realHeatList period directions t f

theorem EulerGaussianCylinderHeat.realHeatList_strongDerivative (period : ℝ) [Fact (0 < period)] (directions : List EulerLiftedGradientSpace.LiftTangent) (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : HasDerivAt (lineOrbit period a f) g 0) : HasDerivAt (lineOrbit period a (realHeatList period directions t f)) (realHeatList period directions t g) 0

Every strong coordinate derivative commutes with every finite heat product.

theorem EulerGaussianCylinderHeat.realHeatList_generator_pos (period : ℝ) [Fact (0 < period)] {ι : Type u_1} (indices : List ι) (direction : ι → EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (df ddf : ι → ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : ∀ i ∈ indices, HasDerivAt (lineOrbit period (direction i) f) (df i) 0) (hDD : ∀ i ∈ indices, HasDerivAt (lineOrbit period (direction i) (df i)) (ddf i) 0) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => realHeatList period (List.map direction indices) s f) ((1 / 2) • realHeatList period (List.map direction indices) t (List.map ddf indices).sum) t

The finite directional heat product has the sum of its actual second derivatives as generator.

theorem EulerGaussianCylinderHeat.realHeatList_generator_zero (period : ℝ) [Fact (0 < period)] {ι : Type u_1} (indices : List ι) (direction : ι → EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (df ddf : ι → ↥(EulerLiftedGradientSpace.LiftL2 period)) (hD : ∀ i ∈ indices, HasDerivAt (lineOrbit period (direction i) f) (df i) 0) (hDD : ∀ i ∈ indices, HasDerivAt (lineOrbit period (direction i) (df i)) (ddf i) 0) : HasDerivWithinAt (fun (s : ℝ) => realHeatList period (List.map direction indices) s f) ((1 / 2) • (List.map ddf indices).sum) (Set.Ici 0) 0

The full directional generator identity holds as a right derivative at zero as well.

Exact identification of the Gaussian cylinder generator with the actual strong-jet Laplacian.

noncomputable def EulerGaussianCylinderHeat.cylinderHeatJet (period : ℝ) [Fact (0 < period)] {q : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f) (v : NNReal) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q ((cylinderHeat period v) f)

Every existing strong Sobolev jet is transported by the genuine heat operator.

Equations

• EulerGaussianCylinderHeat.cylinderHeatJet period J v = EulerPressureJetIdentities.SpatialJet.map (EulerGaussianCylinderHeat.cylinderHeat period v) ⋯ J

theorem EulerGaussianCylinderHeat.cylinderHeatJet_word (period : ℝ) [Fact (0 < period)] {q n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f) (v : NNReal) (w : Fin n → Fin 4) : (cylinderHeatJet period J v).word w = (cylinderHeat period v) (J.word w)

Heat preserves every actual derivative coordinate.

theorem EulerGaussianCylinderHeat.cylinderHeatJet_laplacian (period : ℝ) [Fact (0 < period)] {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) (v : NNReal) : EulerMetricHeatEnergy.jetLaplacian period (cylinderHeatJet period J v) = (cylinderHeat period v) (EulerMetricHeatEnergy.jetLaplacian period J)

The actual heat operator commutes with the true strong-jet Laplacian.

noncomputable def EulerGaussianCylinderHeat.realCylinderHeat (period : ℝ) [Fact (0 < period)] (t : ℝ) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Real-time extension of the cylinder heat semigroup.

Equations

• EulerGaussianCylinderHeat.realCylinderHeat period t = EulerGaussianCylinderHeat.cylinderHeat period t.toNNReal

theorem EulerGaussianCylinderHeat.realCylinderHeat_apply (period : ℝ) [Fact (0 < period)] (t : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (realCylinderHeat period t) f = realHeatList period cylinderDirections t f

theorem EulerGaussianCylinderHeat.realCylinderHeat_generator_pos (period : ℝ) [Fact (0 < period)] {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => (realCylinderHeat period s) f) ((1 / 2) • (realCylinderHeat period t) (EulerMetricHeatEnergy.jetLaplacian period J)) t

The actual cylinder heat generator at positive variance is one half of the Laplacian.

theorem EulerGaussianCylinderHeat.realCylinderHeat_generator_zero (period : ℝ) [Fact (0 < period)] {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) : HasDerivWithinAt (fun (s : ℝ) => (realCylinderHeat period s) f) ((1 / 2) • EulerMetricHeatEnergy.jetLaplacian period J) (Set.Ici 0) 0

The actual cylinder heat generator at zero variance is a right Laplacian derivative.

noncomputable def EulerGaussianCylinderHeat.viscousCylinderHeat (period : ℝ) [Fact (0 < period)] (ν t : ℝ) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Variance2νt is the genuine viscosity-ν heat evolution.

Equations

• EulerGaussianCylinderHeat.viscousCylinderHeat period ν t = EulerGaussianCylinderHeat.realCylinderHeat period (2 * ν * t)

theorem EulerGaussianCylinderHeat.viscousCylinderHeat_equation (period : ℝ) [Fact (0 < period)] {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 f) {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => (viscousCylinderHeat period ν s) f) (ν • EulerMetricHeatEnergy.jetLaplacian period (cylinderHeatJet period J (2 * ν * t).toNNReal)) t

The constructed heat evolution solves u_t=νΔu, with the actual strong spatial Laplacian.

noncomputable def EulerSobolevHeatGenerator.laplacianEvaluation (period : ℝ) [Fact (0 < period)] (q : ℕ) (hq : 2 ≤ q) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual spatial Laplacian evaluated as a bounded map from Hq to L², q≥2.

Equations

• EulerSobolevHeatGenerator.laplacianEvaluation period q hq = ∑ i : Fin 4, EulerCylinderSobolevSpace.wordOperator period ⟨⟨2, ⋯⟩, fun (x : Fin 2) => i⟩

theorem EulerSobolevHeatGenerator.laplacianEvaluation_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (laplacianEvaluation period q hq) u = ∑ i : Fin 4, EulerCylinderSobolevSpace.word period u hq fun (x : Fin 2) => i

The Laplacian evaluation is the sum of the four genuine second derivative coordinates.

theorem EulerSobolevHeatGenerator.laplacianEvaluation_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖(laplacianEvaluation period q hq) u‖ ≤ 4 * ‖u‖

The actual Laplacian is bounded by four times the complete Sobolev norm.

theorem EulerSobolevHeatGenerator.laplacianEvaluation_eq_jet (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (laplacianEvaluation period q hq) u = EulerMetricHeatEnergy.jetLaplacian period (EulerH6Pressure.SpatialJet.restrict (EulerCylinderSobolevSpace.toJet period u) 2 hq)

Bounded Laplacian evaluation agrees exactly with the existing genuine strong-jet Laplacian.

theorem EulerSobolevHeatGenerator.laplacianEvaluation_heat (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (laplacianEvaluation period q hq) ((EulerSobolevHeat.heatOperator period q v) u) = (EulerGaussianCylinderHeat.cylinderHeat period v) ((laplacianEvaluation period q hq) u)

The actual Laplacian evaluation commutes with Gaussian heat.

noncomputable def EulerSobolevHeatGenerator.heatFlow (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν t : ℝ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Actual viscous heat on the complete Sobolev space, extended constantly to negative physical time.

Equations

• EulerSobolevHeatGenerator.heatFlow period q ν t = EulerSobolevHeat.heatOperator period q (2 * ν * t).toNNReal

@[simp]

theorem EulerSobolevHeatGenerator.heatFlow_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν t : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((heatFlow period q ν t) u) = (EulerGaussianCylinderHeat.viscousCylinderHeat period ν t) (EulerCylinderSobolevSpace.value period u)

The Sobolev flow has exactly the original genuine L² viscous heat value.

theorem EulerSobolevHeatGenerator.heatFlow_value_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν : ℝ) (hν : 0 < ν) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (t : ℝ) (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((heatFlow period q ν s) u)) (ν • (laplacianEvaluation period q hq) ((heatFlow period q ν t) u)) t

Positive-time heat is differentiable in L² with the actual bounded Laplacian evaluation.

theorem EulerSobolevHeatGenerator.realHeat_value_hasDerivWithinAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (t : ℝ) (ht : 0 ≤ t) : HasDerivWithinAt (fun (s : ℝ) => (EulerGaussianCylinderHeat.realCylinderHeat period s) (EulerCylinderSobolevSpace.value period u)) ((1 / 2) • (EulerGaussianCylinderHeat.realCylinderHeat period t) ((laplacianEvaluation period q hq) u)) (Set.Ici 0) t

The actual L² heat orbit has the half-Laplacian derivative on the nonnegative variance half-line.

theorem EulerSobolevHeatGenerator.heat_value_lipschitz (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : LipschitzWith (Real.nnabs (2 * ‖u‖)) fun (v : NNReal) => (EulerGaussianCylinderHeat.cylinderHeat period v) (EulerCylinderSobolevSpace.value period u)

The heat orbit is Lipschitz in nonnegative variance with a bound from the actual Hq norm.

theorem EulerSobolevHeatGenerator.realHeat_value_lipschitz (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : LipschitzWith (Real.nnabs (2 * ‖u‖)) fun (t : ℝ) => (EulerGaussianCylinderHeat.realCylinderHeat period t) (EulerCylinderSobolevSpace.value period u)

The constantly extended real-variance heat orbit is globally Lipschitz in L².

theorem EulerSobolevHeatGenerator.heatFlow_value_norm_sub_le (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν : ℝ) (hν : 0 < ν) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (s t : ℝ) : ‖EulerCylinderSobolevSpace.value period ((heatFlow period q ν s) u) - EulerCylinderSobolevSpace.value period ((heatFlow period q ν t) u)‖ ≤ 4 * ν * ‖u‖ * |s - t|

The actual viscous heat orbit is globally Lipschitz in L², uniformly in time.