def Duhamel.euclidNormSq {n : ℕ} (x : Fin n → ℝ) : ℝ

The squared Euclidean norm $|x|^2 = \sum_{i=1}^n (x^i)^2$ for $x \in \mathbb{R}^n$.

noncomputable def Duhamel.heatKernel {n : ℕ} (D t : ℝ) (x : Fin n → ℝ) : ℝ

The heat kernel (fundamental solution) on $\mathbb{R}^n$: $\Gamma_D(t, x) = \frac{1}{(4 \pi D t)^{n/2}} \exp\!\left(-\frac{|x|^2}{4 D t}\right)$.

noncomputable def Duhamel.laplacian {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

The spatial Laplacian $\Delta f(x) = \sum_{i=1}^n \partial_i^2 f(x)$.

noncomputable def Duhamel.heatOperator {n : ℕ} (D : ℝ) (u : ℝ → (Fin n → ℝ) → ℝ) (t : ℝ) (x : Fin n → ℝ) : ℝ

The heat operator $\partial_t u - D \Delta u$ applied to $u$ at $(t, x)$.

noncomputable def Duhamel.spatialConvolution {n : ℕ} (f g : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

Spatial convolution $(f * g)(x) = \int_{\mathbb{R}^n} f(x - y) g(y)\, d^n y$.

noncomputable def Duhamel.duhamelSolution {n : ℕ} (D : ℝ) (g : (Fin n → ℝ) → ℝ) (f : ℝ → (Fin n → ℝ) → ℝ) (t : ℝ) (x : Fin n → ℝ) : ℝ

Duhamel's formula: the candidate solution to the inhomogeneous heat equation $u_t - D \Delta u = f$ with initial data $g$ is $u(t, x) = (\Gamma_D(t, \cdot) * g)(x) + \int_0^t (\Gamma_D(t - s, \cdot) * f(s, \cdot))(x)\, ds$.

theorem Duhamel.theorem_1_2_duhamel {n : ℕ} (D : ℝ) (hD : D > 0) (g : (Fin n → ℝ) → ℝ) (hg_cont : Continuous g) {a : ℝ} (ha : 0 < a) {b : ℝ} (hb : 0 < b) (hg_bound : ∀ (x : Fin n → ℝ), |g x| ≤ a * Real.exp (b * euclidNormSq x)) (f : ℝ → (Fin n → ℝ) → ℝ) (hf_cont : Continuous fun (p : ℝ × (Fin n → ℝ)) => f p.1 p.2) (hf_bdd : ∃ (M : ℝ), ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t < 1 / (4 * D * b) → |f t x| ≤ M) (hf_deriv_bdd : ∀ (i : Fin n), ∃ (M : ℝ), ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t < 1 / (4 * D * b) → ‖(fderiv ℝ (f t) x) (Pi.single i 1)‖ ≤ M) (hf_deriv2_bdd : ∀ (i j : Fin n), ∃ (M : ℝ), ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t < 1 / (4 * D * b) → ‖(fderiv ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ (f t) y) (Pi.single i 1)) x) (Pi.single j 1)‖ ≤ M) : ∃ (u : ℝ → (Fin n → ℝ) → ℝ), (∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → u t x = duhamelSolution D g f t x) ∧ (∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → heatOperator D u t x = f t x) ∧ (∀ (x : Fin n → ℝ), Filter.Tendsto (fun (t : ℝ) => u t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g x))) ∧ ContinuousOn (fun (p : ℝ × (Fin n → ℝ)) => u p.1 p.2) (Set.Ico 0 (1 / (4 * D * b)) ×ˢ Set.univ) ∧ (∀ (x : Fin n → ℝ), ContDiffOn ℝ 1 (fun (t : ℝ) => u t x) (Set.Ioo 0 (1 / (4 * D * b)))) ∧ (∀ t ∈ Set.Ioo 0 (1 / (4 * D * b)), ContDiff ℝ 2 (u t)) ∧ ∀ (v : ℝ → (Fin n → ℝ) → ℝ), (∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → heatOperator D v t x = f t x) → (∀ (x : Fin n → ℝ), Filter.Tendsto (fun (t : ℝ) => v t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g x))) → (∃ (A : ℝ) (B : ℝ), 0 < A ∧ 0 < B ∧ ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t < 1 / (4 * D * b) → |v t x| ≤ A * Real.exp (B * euclidNormSq x)) → ∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → v t x = u t x

Duhamel's principle (Theorem 1.2): for continuous initial data $g$ satisfying $|g(x)| \leq a\,e^{b|x|^2}$ and a continuous, bounded forcing $f$ with bounded first and second spatial derivatives, the inhomogeneous heat equation $u_t - D \Delta u = f$, $u(0, x) = g(x)$ has a unique solution $u \in C([0, T) \times \mathbb{R}^n) \cap C^{1,2}((0, T) \times \mathbb{R}^n)$ on $[0, T) \times \mathbb{R}^n$ with $T = \tfrac{1}{4 D b}$, given on $(0, T)$ by the Duhamel formula.