The actual Gaussian cylinder heat semigroup on the complete Sobolev scale.

Genuine one-derivative L² smoothing lifts to the complete cylinder Sobolev scale.

noncomputable def EulerSobolevSmoothing.smoothingDerivative (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The uniquely determined strong derivative of a genuinely smoothing L² operator.

Equations

• EulerSobolevSmoothing.smoothingDerivative period A C hD i f = Classical.choose ⋯

theorem EulerSobolevSmoothing.smoothingDerivative_hasDerivAt (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) (smoothingDerivative period A C hD i f) 0

The chosen derivative is the actual strong derivative of the translated output.

theorem EulerSobolevSmoothing.smoothingDerivative_bound (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖smoothingDerivative period A C hD i f‖ ≤ C * ‖f‖

The actual derivative obeys the given L² smoothing estimate.

theorem EulerSobolevSmoothing.smoothingDerivative_add (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) : smoothingDerivative period A C hD i (f + g) = smoothingDerivative period A C hD i f + smoothingDerivative period A C hD i g

Uniqueness of strong derivatives proves additivity of the smoothing derivative.

theorem EulerSobolevSmoothing.smoothingDerivative_smul (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) (r : ℝ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : smoothingDerivative period A C hD i (r • f) = r • smoothingDerivative period A C hD i f

Uniqueness of strong derivatives proves homogeneity of the smoothing derivative.

noncomputable def EulerSobolevSmoothing.smoothingDerivativeOperator (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Each derivative of the smoothing operator is a bounded linear L² operator.

Equations

• EulerSobolevSmoothing.smoothingDerivativeOperator period A C hD i = { toFun := EulerSobolevSmoothing.smoothingDerivative period A C hD i, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯

theorem EulerSobolevSmoothing.smoothingDerivativeOperator_hasDerivAt (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) ((smoothingDerivativeOperator period A C hD i) f) 0

The bounded derivative operator retains its actual strong-derivative characterization.

theorem EulerSobolevSmoothing.smoothingDerivativeOperator_bound (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖(smoothingDerivativeOperator period A C hD i) f‖ ≤ C * ‖f‖

The bounded derivative operator retains the actual smoothing estimate.

theorem EulerSobolevSmoothing.smoothingDerivative_translation (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (i : Fin 4) (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerLiftedGradientSpace.translation period a) ((smoothingDerivativeOperator period A C hD i) f) = (smoothingDerivativeOperator period A C hD i) ((EulerLiftedGradientSpace.translation period a) f)

Differentiating a translation-commuting smoothing operator preserves translation commutation.

noncomputable def EulerSobolevSmoothing.gainJet (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) {q : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection (q + 1) (A f)

A true smoothing operator adds one complete level to any finite strong derivative jet.

Equations

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

noncomputable def EulerSobolevSmoothing.gain (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) {q : ℕ} (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))

The Sobolev element obtained by actual one-derivative smoothing.

Equations

• EulerSobolevSmoothing.gain period A C hD hA u = EulerCylinderSobolevSpace.ofJet period (EulerSobolevSmoothing.gainJet period A C hD hA (EulerCylinderSobolevSpace.toJet period u))

@[simp]

theorem EulerSobolevSmoothing.gain_value (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) {q : ℕ} (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period (gain period A C hD hA u) = A (EulerCylinderSobolevSpace.value period u)

Smoothing on the Sobolev scale has exactly the original L² output.

theorem EulerSobolevSmoothing.gain_bound (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) {q : ℕ} (hC : 0 ≤ C) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖gain period A C hD hA u‖ ≤ max ‖A‖ C * ‖u‖

The Sobolev derivative gain has an explicit bound independent of the derivative order.

noncomputable def EulerSobolevSmoothing.gainLinearMap (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (q : ℕ) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →ₗ[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))

The actual Sobolev smoothing construction is linear.

Equations

• EulerSobolevSmoothing.gainLinearMap period A C hD q hA = { toFun := EulerSobolevSmoothing.gain period A C hD hA, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerSobolevSmoothing.gainOperator (period : ℝ) [Fact (0 < period)] (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (C : ℝ) (hD : ∀ (i : Fin 4) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), ∃ (g : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (A f)) g 0 ∧ ‖g‖ ≤ C * ‖f‖) (q : ℕ) (hC : 0 ≤ C) (hA : ∀ (a : EulerLiftedGradientSpace.LiftDomain period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)), A ((EulerLiftedGradientSpace.translation period a) f) = (EulerLiftedGradientSpace.translation period a) (A f)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))

A genuine bounded map H^q to H^(q+1), obtained from actual L² smoothing derivatives.

Equations

• EulerSobolevSmoothing.gainOperator period A C hD q hC hA = (EulerSobolevSmoothing.gainLinearMap period A C hD q hA).mkContinuous (max ‖A‖ C) ⋯

noncomputable def EulerSobolevHeat.heatOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) (v : NNReal) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The genuine cylinder heat semigroup lifted to the complete Sobolev space.

Equations

• EulerSobolevHeat.heatOperator period q v = EulerCylinderSobolevSpace.liftOperator period q (EulerGaussianCylinderHeat.cylinderHeat period v) ⋯

@[simp]

theorem EulerSobolevHeat.heatOperator_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (w : EulerCylinderSobolevSpace.SobolevWord q) : ↑((heatOperator period q v) u) w = (EulerGaussianCylinderHeat.cylinderHeat period v) (↑u w)

Every Sobolev derivative coordinate evolves by the actual L² heat semigroup.

theorem EulerSobolevHeat.heatOperator_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖(heatOperator period q v) u‖ ≤ ‖u‖

The heat semigroup is contractive in every complete Sobolev norm.

@[simp]

theorem EulerSobolevHeat.heatOperator_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((heatOperator period q v) u) = (EulerGaussianCylinderHeat.cylinderHeat period v) (EulerCylinderSobolevSpace.value period u)

The underlying L² field evolves by exactly the original heat operator.

@[simp]

theorem EulerSobolevHeat.heatOperator_zero (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (heatOperator period q 0) u = u

Zero variance is the identity on the complete Sobolev space.

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

The actual Sobolev heat operators obey the semigroup law.

theorem EulerSobolevHeat.heatOperator_continuous (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : Continuous fun (v : NNReal) => (heatOperator period q v) u

Strong heat continuity holds in every complete Sobolev norm, including at zero variance.

noncomputable def EulerSobolevHeat.heatDerivativeConstant (v : NNReal) : ℝ

The explicit parabolic derivative constant of the Gaussian heat operator.

Equations

• EulerSobolevHeat.heatDerivativeConstant v = EulerGaussianCylinderHeat.gaussianAbsMoment 1 / √↑v

theorem EulerSobolevHeat.heatDerivativeConstant_nonneg (v : NNReal) : 0 ≤ heatDerivativeConstant v

The Gaussian derivative constant is nonnegative.

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

Positive-time heat smoothing is a genuine bounded map between successive Sobolev levels.

Equations

• EulerSobolevHeat.heatGain period q v hv = EulerSobolevSmoothing.gainOperator period (EulerGaussianCylinderHeat.cylinderHeat period v) (EulerSobolevHeat.heatDerivativeConstant v) ⋯ q ⋯ ⋯

@[simp]

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

The derivative-gaining map has exactly the actual L² heat output.

theorem EulerSobolevHeat.heatGain_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (hv : 0 < v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖(heatGain period q v hv) u‖ ≤ max 1 (heatDerivativeConstant v) * ‖u‖

Actual Gaussian smoothing gains one Sobolev derivative, uniformly in the Sobolev order.

theorem EulerSobolevHeat.truncate_heatGain (period : ℝ) [Fact (0 < period)] {q : ℕ} (v : NNReal) (hv : 0 < v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerCylinderSobolevSpace.truncateOperator period q) ((heatGain period q v hv) u) = (heatOperator period q v) u

Truncating the gained derivative gives the ordinary Sobolev heat action.

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

A fixed positive amount of smoothing may be separated from any remaining heat evolution.

theorem EulerSobolevHeat.heatGain_continuous (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : Continuous fun (v : { v : NNReal // 0 < v }) => (heatGain period q ↑v ⋯) u

The gained-derivative heat orbit is strongly continuous at every positive variance.