The actual cylinder heat kernel in the singular Volterra existence theorem.

def EulerSobolevHeat.positiveVariance (ν : ℝ) (hν : 0 < ν) (t : { t : ℝ // 0 < t }) : { v : NNReal // 0 < v }

Positive physical time converted to positive Gaussian variance for viscosity ν.

Equations

• EulerSobolevHeat.positiveVariance ν hν t = ⟨⟨2 * ν * ↑t, ⋯⟩, ⋯⟩

theorem EulerSobolevHeat.positiveVariance_continuous (ν : ℝ) (hν : 0 < ν) : Continuous (positiveVariance ν hν)

Physical time to Gaussian variance is continuous on positive times.

theorem EulerSobolevHeat.heatKernel_joint_continuous (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) : ContinuousOn (fun (p : ℝ × ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) => (heatKernel period q ν hν p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)

The actual one-derivative heat kernel is jointly continuous at every positive physical time.

noncomputable def EulerSobolevHeat.freeHeatPath (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν T : ℝ) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The free viscous heat evolution is an actual continuous path in every Sobolev space.

Equations

• EulerSobolevHeat.freeHeatPath period q ν T u₀ = { toFun := fun (t : ↑(Set.Icc 0 T)) => (EulerSobolevHeat.heatOperator period q (2 * ν * ↑t).toNNReal) u₀, continuous_toFun := ⋯ }

theorem EulerSobolevHeat.freeHeatPath_bound (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν T : ℝ) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖freeHeatPath period q ν T u₀‖ ≤ ‖u₀‖

The free heat path obeys the initial-data bound in the actual uniform Sobolev norm.

theorem EulerSobolevHeat.exists_viscous_mild_solution (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (F : ↑(Set.Icc 0 T) → ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) => F p.1 p.2) (R M L : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (hL : 0 ≤ L) (hFM : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))), ‖x‖ ≤ R → ‖F t x‖ ≤ M) (hFL : ∀ (t : ↑(Set.Icc 0 T)) (x y : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))), ‖x‖ ≤ R → ‖y‖ ≤ R → ‖F t x - F t y‖ ≤ L * ‖x - y‖) (hbudget : ‖u₀‖ + (T + 2 * parabolicConstant ν * √T) * M ≤ R) (hsmall : (T + 2 * parabolicConstant ν * √T) * L < 1) : ∃ (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖u‖ ≤ R ∧ ∀ (t : ↑(Set.Icc 0 T)), u t = (heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (heatKernel period q ν hν r) (F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r))))

The actual viscous heat equation has a local mild solution for every continuous locally Lipschitz derivative-losing source satisfying the explicit time budget.