Jointly continuous positive-time heat kernels with an explicit integrable parabolic bound.

@[instance_reducible]

noncomputable def EulerSobolevHeat.sobolevNormedGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

A local name for the inherited Sobolev normed group avoids repeated subtype-instance expansion.

Equations

• EulerSobolevHeat.sobolevNormedGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevHeat.sobolevNormedSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

A local name for the inherited Sobolev scalar structure.

Equations

• EulerSobolevHeat.sobolevNormedSpace period q = inferInstance

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

The ordinary Sobolev heat flow is a contraction in its input field.

theorem EulerSobolevHeat.heatOperator_joint_continuous (period : ℝ) [Fact (0 < period)] (q : ℕ) : Continuous fun (p : NNReal × ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) => (heatOperator period q p.1) p.2

Strong continuity and contraction imply joint continuity of the actual Sobolev heat flow.

theorem EulerSobolevHeat.fixed_heatGain_continuous (period : ℝ) [Fact (0 < period)] (q : ℕ) (ε : NNReal) (hε : 0 < ε) : Continuous fun (z : { v : NNReal // 0 < v } × ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) => (heatGain period q ε hε) ((heatOperator period q (↑z.1 - ε)) z.2)

A fixed amount of smoothing composed with jointly continuous heat remains jointly continuous.

theorem EulerSobolevHeat.heatGain_tsub (period : ℝ) [Fact (0 < period)] {q : ℕ} (ε v : NNReal) (hε : 0 < ε) (hev : ε ≤ v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (heatGain period q ε hε) ((heatOperator period q (v - ε)) u) = (heatGain period q v ⋯) u

Factoring off a smaller variance leaves the same actual derivative-gaining heat output.

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

Splitting off a fixed positive smoothing time gives joint continuity with one gained derivative.

noncomputable def EulerSobolevHeat.heatKernel (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (t : ℝ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))

The positive real-time heat kernel, with zero chosen at nonpositive time.

Equations

• EulerSobolevHeat.heatKernel period q ν hν t = if ht : 0 < t then EulerSobolevHeat.heatGain period q ⟨2 * ν * t, ⋯⟩ ⋯ else 0

noncomputable def EulerSobolevHeat.parabolicConstant (ν : ℝ) : ℝ

The scalar coefficient multiplying the inverse square root in the heat-kernel bound.

Equations

• EulerSobolevHeat.parabolicConstant ν = EulerGaussianCylinderHeat.gaussianAbsMoment 1 / √(2 * ν)

noncomputable def EulerSobolevHeat.parabolicKernelBound (ν t : ℝ) : ℝ

The explicit integrable majorant for one-derivative heat smoothing.

Equations

• EulerSobolevHeat.parabolicKernelBound ν t = 1 + EulerSobolevHeat.parabolicConstant ν * t ^ (-(1 / 2))

theorem EulerSobolevHeat.parabolicKernelBound_nonneg (ν t : ℝ) (ht : 0 < t) : 0 ≤ parabolicKernelBound ν t

The scalar parabolic majorant is nonnegative on positive times.

theorem EulerSobolevHeat.heatKernel_bound (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (t : ℝ) (ht : 0 < t) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖(heatKernel period q ν hν t) u‖ ≤ parabolicKernelBound ν t * ‖u‖

The actual viscosity-scaled heat kernel satisfies the explicit inverse-square-root bound.

theorem EulerSobolevHeat.parabolicKernelBound_integrable (ν T : ℝ) (hT : 0 ≤ T) : MeasureTheory.IntegrableOn (parabolicKernelBound ν) (Set.Ioc 0 T) MeasureTheory.volume

The scalar heat majorant is genuinely integrable at time zero.

theorem EulerSobolevHeat.parabolicKernelBound_integral (ν T : ℝ) (hT : 0 ≤ T) : ∫ (t : ℝ) in Set.Ioc 0 T, parabolicKernelBound ν t = T + 2 * parabolicConstant ν * √T

The exact kernel mass is T plus the square-root parabolic contribution.