The constructed gained-derivative heat fixed point satisfies the actual differential PDE in L².
The actual heat Duhamel integral satisfies the inhomogeneous equation in L².
theorem
EulerDuhamelDifferentiation.duhamel_eq_full_sub_tail
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ℝ)
(ht : t ∈ Set.Icc 0 T)
:
duhamel period ν T hT f t = fullDuhamel period ν T hT f t - ∫ (s : ℝ) in t..T, EulerVolterraConvolution.extendPath T hT f s
The causal Duhamel integral is the full clamped heat integral minus the unevolved source tail.
theorem
EulerDuhamelDifferentiation.source_tail_value_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ℝ)
:
HasDerivAt
(fun (r : ℝ) =>
EulerCylinderSobolevSpace.value period (∫ (s : ℝ) in r..T, EulerVolterraConvolution.extendPath T hT f s))
(-EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT f t)) t
The source tail has its genuine L² derivative by the fundamental theorem of calculus.
theorem
EulerDuhamelDifferentiation.derivativeIntegral_eq_laplacian
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q)
(ν T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ℝ)
(ht : t ∈ Set.Icc 0 T)
:
∫ (s : ℝ) in Set.Ioc 0 T, derivativeIntegrand period hq ν T hT f t s = ν • (EulerSobolevHeatGenerator.laplacianEvaluation period q hq) (duhamel period ν T hT f t)
The differentiated full convolution is the actual Laplacian of the causal Duhamel integral.
theorem
EulerDuhamelDifferentiation.duhamel_value_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q)
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (duhamel period ν T hT f r))
(ν • (EulerSobolevHeatGenerator.laplacianEvaluation period q hq) (duhamel period ν T hT f t) + EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT f t))
t
The actual Sobolev Duhamel integral is differentiable in L² and solves w′=νΔw+f.
theorem
EulerDuhamelDifferentiation.inhomogeneous_heat_value_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q)
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt
(fun (r : ℝ) =>
EulerCylinderSobolevSpace.value period
((EulerSobolevHeatGenerator.heatFlow period q ν r) u₀ + duhamel period ν T hT f r))
(ν • (EulerSobolevHeatGenerator.laplacianEvaluation period q hq)
((EulerSobolevHeatGenerator.heatFlow period q ν t) u₀ + duhamel period ν T hT f t) + EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT f t))
t
The genuine free heat plus Duhamel candidate satisfies the actual inhomogeneous L² PDE.
theorem
EulerMildEquationBridge.truncate_heatOperator
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(v : NNReal)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
(EulerCylinderSobolevSpace.truncateOperator period q) ((EulerSobolevHeat.heatOperator period (q + 1) v) u) = (EulerSobolevHeat.heatOperator period q v) ((EulerCylinderSobolevSpace.truncateOperator period q) u)
Ordinary Sobolev heat commutes with forgetting the highest derivative level.
theorem
EulerMildEquationBridge.laplacian_truncate
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
(EulerSobolevHeatGenerator.laplacianEvaluation period q hq) ((EulerCylinderSobolevSpace.truncateOperator period q) u) = (EulerSobolevHeatGenerator.laplacianEvaluation period (q + 1) ⋯) u
The actual Laplacian agrees under Sobolev truncation whenever both sides have two derivatives.
theorem
EulerMildEquationBridge.truncate_heatKernel
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 < ν)
(r : ℝ)
(hr : 0 < r)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
(EulerCylinderSobolevSpace.truncateOperator period q) ((EulerSobolevHeat.heatKernel period q ν hν r) u) = (EulerSobolevHeatGenerator.heatFlow period q ν r) u
Forgetting the gained derivative of the genuine positive-time heat kernel gives the ordinary heat flow.
theorem
EulerMildEquationBridge.truncate_heatConvolution
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderSobolevSpace.truncateOperator period q)
((EulerVolterraConvolution.convolution T hT (EulerSobolevHeat.heatKernel period q ν hν)
(EulerSobolevHeat.parabolicKernelBound ν) ⋯ ⋯ ⋯ ⋯ f)
t) = EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t
The genuine singular gained-derivative convolution becomes the ordinary Duhamel integral after truncation.
theorem
EulerMildEquationBridge.ordinary_mild_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q)
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(f u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
u t = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) u₀ + EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r))
(ν • (EulerSobolevHeatGenerator.laplacianEvaluation period q hq) (u ⟨t, ⋯⟩) + EulerCylinderSobolevSpace.value period (f ⟨t, ⋯⟩))
t
A continuous Sobolev path satisfying the actual ordinary Duhamel formula solves the inhomogeneous L² equation.
theorem
EulerMildEquationBridge.viscous_mild_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ 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)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r)
(F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r)))))
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r))
(ν • (EulerSobolevHeatGenerator.laplacianEvaluation period (q + 1) ⋯) (u ⟨t, ⋯⟩) + EulerCylinderSobolevSpace.value period (F ⟨t, ⋯⟩ (u ⟨t, ⋯⟩)))
t
Every actual gained-derivative viscous mild solution satisfies u′=νΔu+F(t,u) in L² at interior times.