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

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

theorem HeatFundamental.norm_sq_le_euclidNormSq {n : ℕ} (x : Fin n → ℝ) : ‖x‖ ^ 2 ≤ euclidNormSq x

The Mathlib supremum norm squared is bounded by the Euclidean sum-of-squares norm: $\|x\|_\infty^2 \le \sum_i (x^i)^2$.

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

Definition 1.0.1: the fundamental solution of the heat equation $\Gamma_D(t, x) = \frac{1}{(4\pi D t)^{n/2}} \exp\!\left(-\frac{|x|^2}{4Dt}\right)$ for $t > 0$ and $x \in \mathbb{R}^n$.

def HeatFundamental.deltaDistribution {n : ℕ} (φ : (Fin n → ℝ) → ℝ) : ℝ

Definition 1.0.2: the Dirac delta distribution acting on a test function $\phi$ by $\langle \delta, \phi \rangle := \phi(0)$.

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

The Laplacian $\Delta f(x) = \sum_{i=1}^n \partial_i^2 f(x)$ of a real-valued function on $\mathbb{R}^n$, expressed via iterated Fréchet derivatives in the coordinate directions.

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

The heat operator $u_t - D\,\Delta u$ acting on a time-dependent function $u : \mathbb{R} \to (\mathbb{R}^n \to \mathbb{R})$ at $(t, x)$.

theorem HeatFundamental.heatKernel_time_deriv {n : ℕ} {D : ℝ} (hD : D > 0) {t : ℝ} (ht : t > 0) (x : Fin n → ℝ) : deriv (fun (s : ℝ) => heatKernel D s x) t = heatKernel D t x * (euclidNormSq x / (4 * D * t ^ 2) - ↑n / (2 * t))

Time derivative of the heat kernel: for $D, t > 0$, $\partial_t \Gamma_D(t, x) = \Gamma_D(t, x)\bigl(\frac{|x|^2}{4Dt^2} - \frac{n}{2t}\bigr)$.

theorem HeatFundamental.euclidNormSq_update {n : ℕ} (x : Fin n → ℝ) (i : Fin n) (s : ℝ) : euclidNormSq (Function.update x i s) = euclidNormSq x - x i ^ 2 + s ^ 2

Replacing the $i$-th coordinate of $x$ by $s$ changes $|x|^2$ by removing $(x_i)^2$ and adding $s^2$.

theorem HeatFundamental.fderiv_eq_deriv_update {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (i : Fin n) (f' : ℝ) (hf : HasDerivAt (fun (s : ℝ) => f (Function.update x i s)) f' (x i)) (hdf : DifferentiableAt ℝ f x) : (fderiv ℝ f x) (Pi.single i 1) = f'

Helper: the $i$-th partial derivative $(\partial_i f)(x)$, computed via the Fréchet derivative applied to the unit vector $e_i$, equals the one-variable derivative of $s \mapsto f(\text{update}\, x\, i\, s)$ at $s = x_i$.

theorem HeatFundamental.differentiableAt_euclidNormSq {n : ℕ} (x : Fin n → ℝ) : DifferentiableAt ℝ euclidNormSq x

The squared Euclidean norm $x \mapsto |x|^2$ is differentiable at every point.

theorem HeatFundamental.differentiableAt_heatKernel {n : ℕ} (D t : ℝ) (x : Fin n → ℝ) : DifferentiableAt ℝ (heatKernel D t) x

For fixed $D$ and $t$, the heat kernel $x \mapsto \Gamma_D(t, x)$ is differentiable at every point.

theorem HeatFundamental.hasDerivAt_gaussianExp_exponent {n : ℕ} (x : Fin n → ℝ) (i : Fin n) (D t : ℝ) : HasDerivAt (fun (s : ℝ) => -euclidNormSq (Function.update x i s) / (4 * D * t)) (-(2 * x i) / (4 * D * t)) (x i)

Helper: derivative in the $i$-th coordinate $s$ of the Gaussian exponent $-|x|^2/(4Dt)$ (with $x_i$ replaced by $s$), evaluated at $s = x_i$.

theorem HeatFundamental.hasDerivAt_gaussianExp {n : ℕ} (x : Fin n → ℝ) (i : Fin n) (D t : ℝ) (hD : D > 0) (ht : t > 0) : HasDerivAt (fun (s : ℝ) => Real.exp (-euclidNormSq (Function.update x i s) / (4 * D * t))) (Real.exp (-euclidNormSq x / (4 * D * t)) * (-x i / (2 * D * t))) (x i)

Helper: derivative in the $i$-th coordinate $s$ of $\exp\bigl(-|x|^2/(4Dt)\bigr)$ (with $x_i$ replaced by $s$), evaluated at $s = x_i$.

theorem HeatFundamental.hasDerivAt_update_linear {n : ℕ} (x : Fin n → ℝ) (i : Fin n) (D t : ℝ) : HasDerivAt (fun (s : ℝ) => -Function.update x i s i / (2 * D * t)) (-1 / (2 * D * t)) (x i)

Helper: the derivative of the linear map $s \mapsto -s/(2Dt)$ (written via Function.update at the $i$-th coordinate) at $s = x_i$ is $-1/(2Dt)$.

theorem HeatFundamental.hasDerivAt_gaussianExp_second {n : ℕ} (x : Fin n → ℝ) (i : Fin n) (D t : ℝ) (hD : D > 0) (ht : t > 0) : HasDerivAt (fun (s : ℝ) => Real.exp (-euclidNormSq (Function.update x i s) / (4 * D * t)) * (-Function.update x i s i / (2 * D * t))) (Real.exp (-euclidNormSq x / (4 * D * t)) * (x i ^ 2 / (2 * D * t) ^ 2 - 1 / (2 * D * t))) (x i)

Helper for computing the second partial derivative of the Gaussian: the derivative in the $i$-th coordinate of the product $\exp(-|x|^2/(4Dt)) \cdot (-x_i/(2Dt))$, evaluated at $s = x_i$.

theorem HeatFundamental.hasDerivAt_heatKernel_coord {n : ℕ} (y : Fin n → ℝ) (i : Fin n) (D t : ℝ) (hD : D > 0) (ht : t > 0) : HasDerivAt (fun (s : ℝ) => heatKernel D t (Function.update y i s)) (heatKernel D t y * (-y i / (2 * D * t))) (y i)

Coordinate derivative of the heat kernel: $\partial_{y_i} \Gamma_D(t, y) = \Gamma_D(t, y) \cdot \bigl(-y_i / (2Dt)\bigr)$.

theorem HeatFundamental.heatKernel_fderiv_single {n : ℕ} (D t : ℝ) (hD : D > 0) (ht : t > 0) (y : Fin n → ℝ) (i : Fin n) : (fderiv ℝ (heatKernel D t) y) (Pi.single i 1) = heatKernel D t y * (-y i / (2 * D * t))

Fréchet derivative of the heat kernel against the $i$-th standard basis vector $e_i$ equals $\Gamma_D(t, y) \cdot (-y_i / (2Dt))$.

theorem HeatFundamental.heatKernel_partial_eq {n : ℕ} (D t : ℝ) (hD : D > 0) (ht : t > 0) (i : Fin n) : (fun (y : Fin n → ℝ) => (fderiv ℝ (heatKernel D t) y) (Pi.single i 1)) = fun (y : Fin n → ℝ) => heatKernel D t y * (-y i / (2 * D * t))

Functional form of heatKernel_fderiv_single: as functions of $y$, the partial derivative $\partial_{y_i} \Gamma_D(t, y)$ equals $\Gamma_D(t, y) \cdot (-y_i/(2Dt))$.

theorem HeatFundamental.hasDerivAt_heatKernel_second_coord {n : ℕ} (y : Fin n → ℝ) (i : Fin n) (D t : ℝ) (hD : D > 0) (ht : t > 0) : HasDerivAt (fun (s : ℝ) => heatKernel D t (Function.update y i s) * (-Function.update y i s i / (2 * D * t))) (heatKernel D t y * (y i ^ 2 / (2 * D * t) ^ 2 - 1 / (2 * D * t))) (y i)

The derivative of the product $\Gamma_D(t, y) \cdot (-y_i/(2Dt))$ in the $i$-th coordinate at $s = y_i$ — used to compute the second partial derivative $\partial_i^2 \Gamma_D(t, y)$.

theorem HeatFundamental.differentiableAt_heatKernel_partial {n : ℕ} (D t : ℝ) (x : Fin n → ℝ) (i : Fin n) : DifferentiableAt ℝ (fun (y : Fin n → ℝ) => heatKernel D t y * (-y i / (2 * D * t))) x

The $i$-th partial derivative $y \mapsto \Gamma_D(t,y) \cdot (-y_i/(2Dt))$ of the heat kernel is itself differentiable.

theorem HeatFundamental.heatKernel_second_fderiv_single {n : ℕ} (D t : ℝ) (hD : D > 0) (ht : t > 0) (x : Fin n → ℝ) (i : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ (heatKernel D t) y) (Pi.single i 1)) x) (Pi.single i 1) = heatKernel D t x * (x i ^ 2 / (2 * D * t) ^ 2 - 1 / (2 * D * t))

The second partial derivative of the heat kernel in the $i$-th direction: $\partial_i^2 \Gamma_D(t, x) = \Gamma_D(t, x) \cdot \bigl(x_i^2/(2Dt)^2 - 1/(2Dt)\bigr)$.

theorem HeatFundamental.heatKernel_laplacian {n : ℕ} {D : ℝ} (hD : D > 0) {t : ℝ} (ht : t > 0) (x : Fin n → ℝ) : laplacian (heatKernel D t) x = heatKernel D t x * (euclidNormSq x / (4 * D ^ 2 * t ^ 2) - ↑n / (2 * D * t))

Laplacian of the heat kernel: for $D, t > 0$, $\Delta_x \Gamma_D(t, x) = \Gamma_D(t, x) \bigl(\frac{|x|^2}{4D^2 t^2} - \frac{n}{2Dt}\bigr)$.

theorem HeatFundamental.heatKernel_solves_heat {n : ℕ} {D : ℝ} (hD : 0 < D) {t : ℝ} (ht : 0 < t) (x : Fin n → ℝ) : heatOperator D (fun (s : ℝ) (y : Fin n → ℝ) => heatKernel D s y) t x = 0

Lemma 1.0.1: the fundamental solution $\Gamma_D(t, x)$ satisfies the homogeneous heat equation $u_t - D\,\Delta u = 0$ for $x \in \mathbb{R}^n$ and $t > 0$.

theorem HeatFundamental.heatKernel_pos {n : ℕ} {D : ℝ} (hD : 0 < D) {t : ℝ} (ht : 0 < t) (x : Fin n → ℝ) : 0 < heatKernel D t x

The heat kernel is strictly positive: $\Gamma_D(t, x) > 0$ for all $D, t > 0$ and all $x \in \mathbb{R}^n$.

theorem HeatFundamental.euclidNormSq_pos {n : ℕ} {x : Fin n → ℝ} (hx : x ≠ 0) : 0 < euclidNormSq x

If $x \ne 0$ then $|x|^2 > 0$.

theorem HeatFundamental.heatKernel_eq_rpow_exp {n : ℕ} {D : ℝ} (hD : 0 < D) {x : Fin n → ℝ} {t : ℝ} (ht : 0 < t) : heatKernel D t x = 1 / (4 * Real.pi * D) ^ (↑n / 2) * (t⁻¹ ^ (↑n / 2) * Real.exp (-(euclidNormSq x / (4 * D)) * t⁻¹))

Rewrites the heat kernel in a form convenient for taking limits as $t \to 0^+$: $\Gamma_D(t, x) = \frac{1}{(4\pi D)^{n/2}}\,t^{-n/2}\,\exp(-|x|^2/(4D) \cdot t^{-1})$.

theorem HeatFundamental.heatKernel_limit_zero_away {n : ℕ} {D : ℝ} (hD : 0 < D) {x : Fin n → ℝ} (hx : x ≠ 0) : Filter.Tendsto (fun (t : ℝ) => heatKernel D t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Lemma 1.0.2 (1): If $x \ne 0$, then $\lim_{t \to 0^+} \Gamma_D(t, x) = 0$.

theorem HeatFundamental.heatKernel_limit_infinity_at_zero {n : ℕ} (hn : 0 < n) {D : ℝ} (hD : 0 < D) : Filter.Tendsto (fun (t : ℝ) => heatKernel D t 0) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

Lemma 1.0.2 (2): $\lim_{t \to 0^+} \Gamma_D(t, 0) = +\infty$ in dimension $n \ge 1$.

theorem HeatFundamental.one_d_gaussian_integral (D t : ℝ) (hD : 0 < D) (ht : 0 < t) : ∫ (x : ℝ), 1 / (4 * Real.pi * D * t) ^ (1 / 2) * Real.exp (-x ^ 2 / (4 * D * t)) = 1

One-dimensional Gaussian integral: $\int_{\mathbb R} \frac{1}{\sqrt{4\pi Dt}} \exp(-x^2/(4Dt))\,dx = 1$.

theorem HeatFundamental.gaussian_integral_eq_one {n : ℕ} {D : ℝ} (hD : 0 < D) {t : ℝ} (ht : 0 < t) : ∫ (x : Fin n → ℝ), heatKernel D t x = 1

The $n$-dimensional Gaussian integral of the heat kernel equals $1$: $\int_{\mathbb R^n} \Gamma_D(t, x)\,d^n x = 1$ for all $t > 0$.

theorem HeatFundamental.heatKernel_integral_one {n : ℕ} {D : ℝ} (hD : 0 < D) {t : ℝ} (ht : 0 < t) : ∫ (x : Fin n → ℝ), heatKernel D t x = 1

Lemma 1.0.2 (3): $\int_{\mathbb R^n} \Gamma_D(t, x)\,d^n x = 1$ for all $t > 0$.

theorem HeatFundamental.heatKernel_lemma_1_0_2 {n : ℕ} {D : ℝ} (hD : 0 < D) (hn : 0 < n) : (∀ (x : Fin n → ℝ), x ≠ 0 → Filter.Tendsto (fun (t : ℝ) => heatKernel D t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) ∧ Filter.Tendsto (fun (t : ℝ) => heatKernel D t 0) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop ∧ ∀ (t : ℝ), 0 < t → ∫ (x : Fin n → ℝ), heatKernel D t x = 1

Lemma 1.0.2: combined statement of the three basic properties of $\Gamma_D(t, x)$: (1) for $x \ne 0$, $\lim_{t \to 0^+} \Gamma_D(t, x) = 0$; (2) $\lim_{t \to 0^+} \Gamma_D(t, 0) = +\infty$; (3) $\int_{\mathbb R^n} \Gamma_D(t, x)\,d^n x = 1$ for all $t > 0$.

theorem HeatFundamental.wider_gaussian_1d (D t : ℝ) (hD : 0 < D) (ht : 0 < t) : ∫ (x : ℝ), 1 / (4 * Real.pi * D * t) ^ (1 / 2) * Real.exp (-x ^ 2 / (8 * D * t)) = 2 ^ (1 / 2)

One-dimensional Gaussian with doubled variance ($8Dt$ instead of $4Dt$): $\int_{\mathbb R} \frac{1}{\sqrt{4\pi Dt}} \exp(-x^2/(8Dt))\,dx = \sqrt{2}$.

theorem HeatFundamental.wider_gaussian_integral {n : ℕ} {D : ℝ} (hD : 0 < D) {t : ℝ} (ht : 0 < t) : ∫ (x : Fin n → ℝ), 1 / (4 * Real.pi * D * t) ^ (↑n / 2) * Real.exp (-euclidNormSq x / (8 * D * t)) = 2 ^ (↑n / 2)

$n$-dimensional version of the "wider" Gaussian integral: $\int_{\mathbb R^n} \frac{1}{(4\pi Dt)^{n/2}} \exp(-|x|^2/(8Dt))\,d^n x = 2^{n/2}$.

theorem HeatFundamental.heat_tail_exp_bound {n : ℕ} {D : ℝ} (hD : 0 < D) (δ : ℝ) (hδ : δ > 0) (t : ℝ) (ht : 0 < t) : |∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x| ≤ Real.exp (-(δ ^ 2 / (8 * D * t))) * 2 ^ (↑n / 2)

Exponential decay bound on the heat-kernel tail outside the ball of radius $\delta$: $\left|\int_{|x| > \delta} \Gamma_D(t, x)\,d^n x\right| \le \exp\bigl(-\delta^2/(8Dt)\bigr) \cdot 2^{n/2}$.

theorem HeatFundamental.exp_neg_large (target : ℝ) (htarget : target > 0) : ∃ x₀ > 0, ∀ x > x₀, Real.exp (-x) < target

For any target $> 0$, the exponential decay $e^{-x}$ eventually drops below it: there exists $x_0 > 0$ such that $e^{-x} <$ target for all $x > x_0$.

theorem HeatFundamental.heatKernel_concentration {n : ℕ} {D : ℝ} (hD : 0 < D) (δ : ℝ) (hδ : δ > 0) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Concentration of the heat kernel: for any $\delta > 0$, $\lim_{t \to 0^+} \int_{|x| > \delta} \Gamma_D(t, x)\,d^n x = 0$.

theorem HeatFundamental.integrable_gauss_nD {n : ℕ} {c : ℝ} (hc : 0 < c) : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => Real.exp (-c * euclidNormSq x)) MeasureTheory.volume

For $c > 0$ the Gaussian $x \mapsto \exp(-c |x|^2)$ is Lebesgue-integrable on $\mathbb R^n$.

theorem HeatFundamental.heatKernel_mul_integrable {n : ℕ} {D : ℝ} (hD : 0 < D) {φ : (Fin n → ℝ) → ℝ} (hφ : Continuous φ) {a b : ℝ} (_ha : 0 ≤ a) (_hb : 0 ≤ b) (hbound : ∀ (x : Fin n → ℝ), |φ x| ≤ a * Real.exp (b * euclidNormSq x)) {t : ℝ} (ht : 0 < t) (htb : b * t < 1 / (4 * D)) : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => heatKernel D t x * φ x) MeasureTheory.volume

Integrability of $x \mapsto \Gamma_D(t, x)\, \phi(x)$ when $\phi$ is continuous and satisfies a Gaussian growth bound $|\phi(x)| \le a\, e^{b |x|^2}$, provided $b t < 1/(4D)$ so the resulting Gaussian remains decaying.

theorem HeatFundamental.prefactor_identity_weighted (n : ℕ) (D t : ℝ) (hD : 0 < D) (ht : 0 < t) : 2 ^ (↑n / 2) * (1 / (4 * Real.pi * (2 * D) * t) ^ (↑n / 2)) = 1 / (4 * Real.pi * D * t) ^ (↑n / 2)

Algebraic identity comparing prefactors of $\Gamma_D$ and $\Gamma_{2D}$: $2^{n/2} \cdot \frac{1}{(4\pi(2D)t)^{n/2}} = \frac{1}{(4\pi D t)^{n/2}}$.

theorem HeatFundamental.exp_bound_weighted (s D b t : ℝ) (hs : 0 ≤ s) (hD : 0 < D) (ht : 0 < t) (htb : b * t ≤ 1 / (8 * D)) : Real.exp (-s / (4 * D * t) + b * s) ≤ Real.exp (-s / (8 * D * t))

Pointwise exponential bound: for $s \ge 0$ and small enough $t$ (so $bt \le 1/(8D)$), $\exp(-s/(4Dt) + bs) \le \exp(-s/(8Dt))$.

theorem HeatFundamental.heatKernel_weighted_pointwise {n : ℕ} {D : ℝ} (hD : 0 < D) {a b : ℝ} (ha : 0 ≤ a) {t : ℝ} (ht : 0 < t) (htb : b * t ≤ 1 / (8 * D)) (x : Fin n → ℝ) : heatKernel D t x * (a * Real.exp (b * euclidNormSq x)) ≤ a * 2 ^ (↑n / 2) * heatKernel (2 * D) t x

Pointwise majorisation: $\Gamma_D(t, x)\,(a\, e^{b|x|^2}) \le a\,2^{n/2}\,\Gamma_{2D}(t, x)$ when $bt \le 1/(8D)$. Used to dominate $\Gamma_D \cdot \phi$ by a Gaussian with wider variance.

theorem HeatFundamental.heatKernel_weighted_concentration {n : ℕ} {D : ℝ} (hD : 0 < D) {φ : (Fin n → ℝ) → ℝ} (hφ : Continuous φ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hbound : ∀ (x : Fin n → ℝ), |φ x| ≤ a * Real.exp (b * euclidNormSq x)) (δ : ℝ) (hδ : 0 < δ) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x * |φ x|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Weighted concentration: for a continuous $\phi$ with Gaussian growth bound $|\phi(x)| \le a\, e^{b|x|^2}$ and any $\delta > 0$, $\lim_{t \to 0^+} \int_{|x| > \delta} \Gamma_D(t, x)\,|\phi(x)|\,d^n x = 0$.

theorem HeatFundamental.heatKernel_ball_integral_bound {n : ℕ} {D : ℝ} {φ : (Fin n → ℝ) → ℝ} {t : ℝ} (hΓint : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => heatKernel D t x) MeasureTheory.volume) (hint_eq_one : ∫ (x : Fin n → ℝ), heatKernel D t x = 1) (hΓpos : ∀ (x : Fin n → ℝ), 0 < heatKernel D t x) (ε : ℝ) (hε : 0 < ε) (δ : ℝ) (hδ : 0 < δ) (hcont : ∀ (x : Fin n → ℝ), ‖x‖ < δ → |φ x - φ 0| < ε) : |∫ (x : Fin n → ℝ) in Metric.closedBall 0 δ, heatKernel D t x * (φ x - φ 0)| ≤ ε

Bound on the contribution to $\int \Gamma_D (\phi - \phi(0))$ from the closed ball of radius $\delta$: if $|\phi(x) - \phi(0)| < \varepsilon$ for $|x| < \delta$, then $\left|\int_{|x| \le \delta} \Gamma_D(t,x)(\phi(x) - \phi(0))\,d^n x\right| \le \varepsilon$.

theorem HeatFundamental.heatKernel_compl_integral_bound {n : ℕ} {D : ℝ} {φ : (Fin n → ℝ) → ℝ} {t : ℝ} (hΓint : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => heatKernel D t x) MeasureTheory.volume) (hΓφ : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => heatKernel D t x * φ x) MeasureTheory.volume) (hΓpos : ∀ (x : Fin n → ℝ), 0 < heatKernel D t x) (δ : ℝ) (_hδ : 0 < δ) : |∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x * (φ x - φ 0)| ≤ (|φ 0| * ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x) + ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x * |φ x|

Triangle-style bound on the contribution from $\{|x| > \delta\}$: $\left|\int_{|x|>\delta} \Gamma_D(t,x)(\phi(x) - \phi(0))\right| \le |\phi(0)| \cdot \int_{|x|>\delta} \Gamma_D + \int_{|x|>\delta} \Gamma_D |\phi|$.

theorem HeatFundamental.heatKernel_approx_pointwise_bound {n : ℕ} {D : ℝ} (hD : 0 < D) {φ : (Fin n → ℝ) → ℝ} (hφ : Continuous φ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hbound : ∀ (x : Fin n → ℝ), |φ x| ≤ a * Real.exp (b * euclidNormSq x)) (ε : ℝ) (hε : 0 < ε) (δ : ℝ) (hδ : 0 < δ) (hcont : ∀ (x : Fin n → ℝ), ‖x‖ < δ → |φ x - φ 0| < ε) {t : ℝ} (ht : 0 < t) (htb : b * t < 1 / (4 * D)) : |(∫ (x : Fin n → ℝ), heatKernel D t x * φ x) - φ 0| ≤ (ε + |φ 0| * ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x) + ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x * |φ x|

Combined pointwise approximation estimate splitting the integral $(\int \Gamma_D \phi) - \phi(0)$ into a ball contribution (bounded by $\varepsilon$) and a tail contribution (bounded via heatKernel_compl_integral_bound).

theorem HeatFundamental.heatKernel_approx_identity_estimate {n : ℕ} {D : ℝ} (hD : 0 < D) {φ : (Fin n → ℝ) → ℝ} (hφ : Continuous φ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hbound : ∀ (x : Fin n → ℝ), |φ x| ≤ a * Real.exp (b * euclidNormSq x)) (ε : ℝ) (hε : 0 < ε) (δ : ℝ) (hδ : 0 < δ) (hcont : ∀ (x : Fin n → ℝ), ‖x‖ < δ → |φ x - φ 0| < ε) : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), |(∫ (x : Fin n → ℝ), heatKernel D t x * φ x) - φ 0| < 2 * ε

Eventual estimate: for any $\varepsilon, \delta > 0$ where $\phi$ has oscillation $< \varepsilon$ on the ball of radius $\delta$, the absolute error $|(\int \Gamma_D(t,x) \phi(x)\,d^n x) - \phi(0)|$ is eventually less than $2\varepsilon$ as $t \to 0^+$.

theorem HeatFundamental.heatKernel_approx_identity_inner {n : ℕ} {D : ℝ} (hD : 0 < D) (φ : (Fin n → ℝ) → ℝ) : Continuous φ → ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → (∀ (x : Fin n → ℝ), |φ x| ≤ a * Real.exp (b * euclidNormSq x)) → Filter.Tendsto (fun (t : ℝ) => ∫ (x : Fin n → ℝ), heatKernel D t x * φ x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ 0))

Lemma 1.0.3 (inner form): for any continuous $\phi : \mathbb R^n \to \mathbb R$ satisfying a Gaussian bound $|\phi(x)| \le a\, e^{b|x|^2}$, $\lim_{t \to 0^+} \int_{\mathbb R^n} \Gamma_D(t, x) \phi(x)\,d^n x = \phi(0)$.

theorem HeatFundamental.heatKernel_approx_identity (n : ℕ) (D : ℝ) (hD : D > 0) (φ : (Fin n → ℝ) → ℝ) (hφ_cont : Continuous φ) (a b : ℝ) (ha : a ≥ 0) (hb : b ≥ 0) (hφ_bound : ∀ (x : Fin n → ℝ), ‖φ x‖ ≤ a * Real.exp (b * ‖x‖ ^ 2)) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : Fin n → ℝ), heatKernel D t x * φ x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ 0))

Lemma 1.0.3: convenient version using the Mathlib norm $\|x\|$ in the Gaussian bound. For continuous $\phi$ with $\|\phi(x)\| \le a\, e^{b \|x\|^2}$, $\lim_{t \to 0^+} \int \Gamma_D(t, x) \phi(x)\,d^n x = \phi(0)$.

theorem HeatFundamental.heatKernel_properties {n : ℕ} {D : ℝ} (hD : 0 < D) : (∀ t > 0, ∀ (x : Fin n → ℝ), 0 < heatKernel D t x) ∧ (∀ t > 0, ∫ (x : Fin n → ℝ), heatKernel D t x = 1) ∧ (∀ δ > 0, Filter.Tendsto (fun (t : ℝ) => ∫ (x : Fin n → ℝ) in {x : Fin n → ℝ | δ < ‖x‖}, heatKernel D t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) ∧ (∀ t > 0, ∀ (x : Fin n → ℝ), heatOperator D (fun (s : ℝ) (y : Fin n → ℝ) => heatKernel D s y) t x = 0) ∧ ∀ (φ : (Fin n → ℝ) → ℝ), Continuous φ → ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → (∀ (x : Fin n → ℝ), |φ x| ≤ a * Real.exp (b * euclidNormSq x)) → Filter.Tendsto (fun (t : ℝ) => ∫ (x : Fin n → ℝ), heatKernel D t x * φ x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ 0))

Proposition 1.0.4 (Properties of $\Gamma_D(t, x)$): collected statement that the heat kernel is positive, integrates to $1$, concentrates near $0$, satisfies the heat equation, and acts as an approximate identity (delta) at $t \to 0^+$.

theorem HeatFundamental.leibniz_integral_rule {I : ℝ → ℝ → ℝ} {b₀ : ℝ} (hI_int : ∀ᶠ (b : ℝ) in nhds b₀, MeasureTheory.Integrable (fun (a : ℝ) => I a b) MeasureTheory.volume) {s : Set ℝ} (hs : s ∈ nhds b₀) (hI_meas : ∀ b ∈ s, MeasureTheory.AEStronglyMeasurable (fun (a : ℝ) => I a b) MeasureTheory.volume) (hI'_meas : ∀ b ∈ s, MeasureTheory.AEStronglyMeasurable (fun (a : ℝ) => deriv (fun (b' : ℝ) => I a b') b) MeasureTheory.volume) {bound : ℝ → ℝ} (h_bound : ∀ᵐ (a : ℝ), ∀ b ∈ s, ‖deriv (fun (b' : ℝ) => I a b') b‖ ≤ bound a) (bound_int : MeasureTheory.Integrable bound MeasureTheory.volume) (h_diff : ∀ᵐ (a : ℝ), ∀ b ∈ s, HasDerivAt (fun (b' : ℝ) => I a b') (deriv (fun (b' : ℝ) => I a b') b) b) : ∀ᶠ (b : ℝ) in nhds b₀, HasDerivAt (fun (b : ℝ) => ∫ (a : ℝ), I a b) (∫ (a : ℝ), deriv (fun (b' : ℝ) => I a b') b) b

Proposition 1.1.1 (Differentiation under the integral): under integrability, measurability, a dominating bound, and pointwise differentiability hypotheses, $\partial_b \int_{\mathbb R} I(a, b)\,da = \int_{\mathbb R} \partial_b I(a, b)\,da$ holds eventually for $b$ near $b_0$.

theorem HeatFundamental.laplacian_const_mul' {n : ℕ} (A : ℝ) (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : laplacian (fun (y : Fin n → ℝ) => A * f y) x = A * laplacian f x

Linearity (constant scaling): $\Delta(A f) = A \cdot \Delta f$.

theorem HeatFundamental.laplacian_translate' {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x₀ x : Fin n → ℝ) : laplacian (fun (y : Fin n → ℝ) => f (y - x₀)) x = laplacian f (x - x₀)

Translation invariance of the Laplacian: $\Delta(f(\cdot - x_0))(x) = (\Delta f)(x - x_0)$.

theorem HeatFundamental.laplacian_smul' {n : ℕ} (f : (Fin n → ℝ) → ℝ) (l : ℝ) (x : Fin n → ℝ) : laplacian (fun (y : Fin n → ℝ) => f (l • y)) x = l ^ 2 * laplacian f (l • x)

Dilation behavior of the Laplacian: $\Delta(f(l \cdot \,))(x) = l^2\,(\Delta f)(l \cdot x)$.

theorem HeatFundamental.heat_invariance_translation {n : ℕ} {D : ℝ} (_hD : 0 < D) {u : ℝ → (Fin n → ℝ) → ℝ} (hu : ∀ (t : ℝ) (x : Fin n → ℝ), heatOperator D u t x = 0) (A t₀ : ℝ) (x₀ : Fin n → ℝ) (t : ℝ) : t > 0 → ∀ (x : Fin n → ℝ), heatOperator D (fun (s : ℝ) (y : Fin n → ℝ) => A * u (s - t₀) (y - x₀)) t x = 0

Lemma 2.0.2 (translation part): if $u$ solves the heat equation, then so does $(t, x) \mapsto A \cdot u(t - t_0, x - x_0)$ for any constants $A$, $t_0$, $x_0$.

theorem HeatFundamental.heat_invariance_parabolic_dilation {n : ℕ} {D : ℝ} (_hD : 0 < D) {u : ℝ → (Fin n → ℝ) → ℝ} (hu : ∀ t > 0, ∀ (x : Fin n → ℝ), heatOperator D u t x = 0) (A : ℝ) {l : ℝ} (hl : 0 < l) (t : ℝ) : t > 0 → ∀ (x : Fin n → ℝ), heatOperator D (fun (s : ℝ) (y : Fin n → ℝ) => A * u (l ^ 2 * s) (l • y)) t x = 0

Lemma 2.0.2 (parabolic dilation part): if $u$ solves the heat equation, then so does $(t, x) \mapsto A \cdot u(l^2 t, l \cdot x)$ for any constant $A$ and any $l > 0$.

noncomputable def HeatFundamental.totalThermalEnergy {n : ℕ} (u : ℝ → (Fin n → ℝ) → ℝ) (t : ℝ) : ℝ

Total thermal energy at time $t$: $\mathcal{T}(t) := \int_{\mathbb R^n} u(t, x)\,d^n x$.

theorem HeatFundamental.integral_laplacian_eq_zero_of_decay {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf_decay : Filter.Tendsto (fun (R : ℝ) => ∫ (x : Fin n → ℝ) in Metric.sphere 0 R, ‖fderiv ℝ f x‖) Filter.atTop (nhds 0)) : ∫ (x : Fin n → ℝ), laplacian f x = 0

If the surface integral of $\|\nabla f\|$ over the sphere of radius $R$ tends to $0$ as $R \to \infty$, then $\int_{\mathbb R^n} \Delta f = 0$ (divergence theorem in the limit).

theorem HeatFundamental.hasDerivAt_totalThermalEnergy_of_heat {n : ℕ} {D : ℝ} {u : ℝ → (Fin n → ℝ) → ℝ} (_hu_solves : ∀ t > 0, ∀ (x : Fin n → ℝ), heatOperator D u t x = 0) (hu_dom : ∃ (f : (Fin n → ℝ) → ℝ), MeasureTheory.Integrable f MeasureTheory.volume ∧ ∀ t > 0, ∀ (x : Fin n → ℝ), ‖deriv (fun (s : ℝ) => u s x) t‖ ≤ f x) {t : ℝ} (ht : 0 < t) : HasDerivAt (totalThermalEnergy u) (∫ (x : Fin n → ℝ), deriv (fun (s : ℝ) => u s x) t) t

Under a uniform integrable bound on $\partial_t u$, the total thermal energy $\mathcal T(t)$ is differentiable in $t$ with $\mathcal T'(t) = \int \partial_t u(t, x)\,d^n x$.

theorem HeatFundamental.continuousOn_totalThermalEnergy_of_dom {n : ℕ} {u : ℝ → (Fin n → ℝ) → ℝ} (hu_dom : ∃ (f : (Fin n → ℝ) → ℝ), MeasureTheory.Integrable f MeasureTheory.volume ∧ ∀ t > 0, ∀ (x : Fin n → ℝ), ‖deriv (fun (s : ℝ) => u s x) t‖ ≤ f x) : ContinuousOn (totalThermalEnergy u) (Set.Ici 0)

Under an integrable dominating bound on $\partial_t u$, the total thermal energy $\mathcal T$ is continuous on $[0, \infty)$.

theorem HeatFundamental.hasDerivAt_totalThermalEnergy_zero {n : ℕ} {D : ℝ} (_hD : 0 < D) {u : ℝ → (Fin n → ℝ) → ℝ} (hu_solves : ∀ t > 0, ∀ (x : Fin n → ℝ), heatOperator D u t x = 0) (hu_decay : ∀ t > 0, Filter.Tendsto (fun (R : ℝ) => ∫ (x : Fin n → ℝ) in Metric.sphere 0 R, ‖fderiv ℝ (u t) x‖) Filter.atTop (nhds 0)) (hu_dom : ∃ (f : (Fin n → ℝ) → ℝ), MeasureTheory.Integrable f MeasureTheory.volume ∧ ∀ t > 0, ∀ (x : Fin n → ℝ), ‖deriv (fun (s : ℝ) => u s x) t‖ ≤ f x) {s : ℝ} (hs : 0 < s) : HasDerivAt (totalThermalEnergy u) 0 s

If $u$ solves the heat equation and decays appropriately at infinity, then $\mathcal T'(s) = 0$ for all $s > 0$.

theorem HeatFundamental.thermal_energy_conservation {n : ℕ} {D : ℝ} (hD : 0 < D) {u : ℝ → (Fin n → ℝ) → ℝ} (hu_solves : ∀ t > 0, ∀ (x : Fin n → ℝ), heatOperator D u t x = 0) (hu_decay : ∀ t > 0, Filter.Tendsto (fun (R : ℝ) => ∫ (x : Fin n → ℝ) in Metric.sphere 0 R, ‖fderiv ℝ (u t) x‖) Filter.atTop (nhds 0)) (hu_dom : ∃ (f : (Fin n → ℝ) → ℝ), MeasureTheory.Integrable f MeasureTheory.volume ∧ ∀ t > 0, ∀ (x : Fin n → ℝ), ‖deriv (fun (s : ℝ) => u s x) t‖ ≤ f x) (t : ℝ) : t > 0 → totalThermalEnergy u t = totalThermalEnergy u 0

Conservation of thermal energy: for a sufficiently decaying solution $u$ of the heat equation, $\mathcal T(t) = \mathcal T(0)$ for all $t > 0$.

noncomputable def HeatFundamental.cauchySolution {n : ℕ} (D : ℝ) (g : (Fin n → ℝ) → ℝ) (t : ℝ) (x : Fin n → ℝ) : ℝ

Candidate solution to the global Cauchy problem (Theorem 1.1), realized as the convolution $(g * \Gamma_D(t, \cdot))(x) = \int_{\mathbb R^n} g(y)\,\Gamma_D(t, x-y)\,d^n y$.

theorem HeatFundamental.euclidNormSq_nonneg {n : ℕ} (x : Fin n → ℝ) : 0 ≤ euclidNormSq x

$|x|^2 \ge 0$ for every $x \in \mathbb R^n$.

theorem HeatFundamental.euclidNormSq_sub_le {n : ℕ} (x z : Fin n → ℝ) : euclidNormSq (x - z) ≤ 2 * euclidNormSq x + 2 * euclidNormSq z

Subadditivity-style bound from the AM-GM inequality: $|x - z|^2 \le 2|x|^2 + 2|z|^2$.

theorem HeatFundamental.heatKernel_time_leibniz_conditions {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : ∃ (s : Set ℝ) (bound : (Fin n → ℝ) → ℝ), s ∈ nhds t ∧ (∀ᶠ (τ : ℝ) in nhds t, MeasureTheory.AEStronglyMeasurable (fun (y : Fin n → ℝ) => g y * heatKernel D τ (x - y)) MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (y : Fin n → ℝ) => g y * heatKernel D t (x - y)) MeasureTheory.volume ∧ MeasureTheory.AEStronglyMeasurable (fun (y : Fin n → ℝ) => g y * deriv (fun (τ : ℝ) => heatKernel D τ (x - y)) t) MeasureTheory.volume ∧ (∀ᵐ (y : Fin n → ℝ), ∀ τ ∈ s, ‖g y * deriv (fun (τ' : ℝ) => heatKernel D τ' (x - y)) τ‖ ≤ bound y) ∧ MeasureTheory.Integrable bound MeasureTheory.volume ∧ ∀ᵐ (y : Fin n → ℝ), ∀ τ ∈ s, HasDerivAt (fun (τ' : ℝ) => g y * heatKernel D τ' (x - y)) (g y * deriv (fun (τ' : ℝ) => heatKernel D τ' (x - y)) τ) τ

Packaged hypotheses needed to apply the dominated-convergence form of the Leibniz rule to differentiate $t \mapsto \int g(y)\,\Gamma_D(t, x - y)\,d^n y$ in $t$.

theorem HeatFundamental.hasDerivAt_cauchySolution_time {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : HasDerivAt (fun (s : ℝ) => cauchySolution D g s x) (∫ (y : Fin n → ℝ), g y * deriv (fun (s : ℝ) => heatKernel D s (x - y)) t) t ∧ MeasureTheory.Integrable (fun (y : Fin n → ℝ) => g y * deriv (fun (s : ℝ) => heatKernel D s (x - y)) t) MeasureTheory.volume

Differentiability in time of the convolution Cauchy solution at $x$: $\partial_t (g * \Gamma_D(t, \cdot))(x) = \int g(y)\,\partial_t \Gamma_D(t, x-y)\,d^n y$, with the integrand integrable.

theorem HeatFundamental.heatKernel_partial_deriv_interchange {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) (i : Fin n) : (fderiv ℝ (fun (z : Fin n → ℝ) => (fderiv ℝ (fun (z' : Fin n → ℝ) => ∫ (y : Fin n → ℝ), g y * heatKernel D t (z' - y)) z) (Pi.single i 1)) x) (Pi.single i 1) = ∫ (y : Fin n → ℝ), g y * (fderiv ℝ (fun (z : Fin n → ℝ) => (fderiv ℝ (fun (z' : Fin n → ℝ) => heatKernel D t z') z) (Pi.single i 1)) (x - y)) (Pi.single i 1)

Interchange of second-order space partial derivative and convolution: the iterated partial $\partial_i^2$ of $(g * \Gamma_D(t, \cdot))$ at $x$ equals the convolution of $g$ with the second partial of $\Gamma_D$ at $x - y$.

theorem HeatFundamental.heatKernel_partial_deriv_integrable {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) (i : Fin n) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => g y * (fderiv ℝ (fun (z : Fin n → ℝ) => (fderiv ℝ (fun (z' : Fin n → ℝ) => heatKernel D t z') z) (Pi.single i 1)) (x - y)) (Pi.single i 1)) MeasureTheory.volume

Integrability of $y \mapsto g(y) \cdot \partial_i^2 \Gamma_D(t, x - y)$ under the Gaussian growth hypothesis on $g$ and the smallness condition $t < 1/(4Db)$.

theorem HeatFundamental.leibniz_laplacian_interchange {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : laplacian (fun (z : Fin n → ℝ) => ∫ (y : Fin n → ℝ), g y * heatKernel D t (z - y)) x = ∫ (y : Fin n → ℝ), g y * laplacian (fun (z : Fin n → ℝ) => heatKernel D t z) (x - y) ∧ MeasureTheory.Integrable (fun (y : Fin n → ℝ) => g y * laplacian (fun (z : Fin n → ℝ) => heatKernel D t z) (x - y)) MeasureTheory.volume

Interchange of Laplacian and convolution: $\Delta_x \int g(y)\,\Gamma_D(t, x-y)\,d^n y = \int g(y)\,(\Delta \Gamma_D)(t, x-y)\,d^n y$, together with integrability of the integrand on the right.

theorem HeatFundamental.leibniz_time_deriv_integral {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : deriv (fun (s : ℝ) => ∫ (y : Fin n → ℝ), g y * heatKernel D s (x - y)) t = ∫ (y : Fin n → ℝ), g y * deriv (fun (s : ℝ) => heatKernel D s (x - y)) t

Time-derivative form of the Leibniz interchange: $\partial_t \int g(y)\,\Gamma_D(t, x-y)\,d^n y = \int g(y)\,\partial_t \Gamma_D(t, x-y)\,d^n y$.

theorem HeatFundamental.leibniz_laplacian_integral {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : laplacian (fun (z : Fin n → ℝ) => ∫ (y : Fin n → ℝ), g y * heatKernel D t (z - y)) x = ∫ (y : Fin n → ℝ), g y * laplacian (fun (z : Fin n → ℝ) => heatKernel D t z) (x - y)

Equality-only form of the Laplacian/convolution interchange (the first component of leibniz_laplacian_interchange).

theorem HeatFundamental.integrable_g_mul_heatKernel_deriv {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => g y * deriv (fun (s : ℝ) => heatKernel D s (x - y)) t) MeasureTheory.volume

Integrability of $y \mapsto g(y)\, \partial_t \Gamma_D(t, x - y)$ under the standard Gaussian growth and smallness hypotheses.

theorem HeatFundamental.integrable_g_mul_heatKernel_laplacian {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => g y * laplacian (fun (z : Fin n → ℝ) => heatKernel D t z) (x - y)) MeasureTheory.volume

Integrability of $y \mapsto g(y)\, (\Delta \Gamma_D)(t, x - y)$ under the standard Gaussian growth and smallness hypotheses.

theorem HeatFundamental.leibniz_heat_operator_commutes_axiom {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : heatOperator D (cauchySolution D g) t x = ∫ (y : Fin n → ℝ), g y * heatOperator D (fun (s : ℝ) (z : Fin n → ℝ) => heatKernel D s z) t (x - y)

The heat operator commutes with convolution against $g$: $(\partial_t - D \Delta)(g * \Gamma_D(t, \cdot))(x) = \int g(y)\,(\partial_t - D \Delta) \Gamma_D(t, x - y)\,d^n y$.

theorem HeatFundamental.contDiffOn_parametric_integral_leibniz {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) : ContDiffOn ℝ ⊤ (fun (p : ℝ × (Fin n → ℝ)) => cauchySolution D g p.1 p.2) (Set.Ioo 0 (1 / (4 * D * b)) ×ˢ Set.univ)

Smoothness of the Cauchy convolution solution on the parabolic strip $(0, 1/(4Db)) \times \mathbb R^n$: it is $C^\infty$ in $(t, x)$ jointly.

theorem HeatFundamental.contDiffOn_parametric_integral_heatKernel {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) : ContDiffOn ℝ ⊤ (fun (p : ℝ × (Fin n → ℝ)) => cauchySolution D g p.1 p.2) (Set.Ioo 0 (1 / (4 * D * b)) ×ˢ Set.univ)

Alias for contDiffOn_parametric_integral_leibniz: the parametric heat-kernel convolution is $C^\infty$ on the parabolic strip.

theorem HeatFundamental.heatKernel_nonneg_pos_time {n : ℕ} {D t : ℝ} (hD : 0 < D) (ht : 0 < t) (x : Fin n → ℝ) : 0 ≤ heatKernel D t x

Non-negativity of the heat kernel for $t > 0$: $\Gamma_D(t, x) \ge 0$.

theorem HeatFundamental.cauchySolution_zero_pos_dim {n : ℕ} (hn : 0 < n) (D : ℝ) (g : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : cauchySolution D g 0 x = 0

In positive dimension, the Cauchy solution evaluates to $0$ at $t = 0$ because the formal heat kernel $\Gamma_D(0, \cdot)$ vanishes (degeneracy of the formula).

theorem HeatFundamental.cinv_sub_b_pos_aux (c b : ℝ) (hc : 0 < c) (hcb : c * b < 1) : 0 < c⁻¹ - b

Auxiliary positivity: if $c > 0$ and $cb < 1$, then $c^{-1} - b > 0$.

theorem HeatFundamental.completing_square_identity_aux (c b a y : ℝ) (hc : 0 < c) (hcb : c * b < 1) : -(a - y) ^ 2 / c + b * y ^ 2 = b / (1 - c * b) * a ^ 2 - (c⁻¹ - b) * (y - a * c⁻¹ / (c⁻¹ - b)) ^ 2

Algebraic "completing the square" identity used to evaluate the 1D Gaussian-times-Gaussian integral $\int e^{-(a-y)^2/c + b y^2}\,dy$.

theorem HeatFundamental.one_d_completing_square_integral_aux (c b a : ℝ) (hc : 0 < c) (hb : 0 < b) (hcb : c * b < 1) : ∫ (y : ℝ), 1 / (Real.pi * c) ^ (1 / 2) * Real.exp (-(a - y) ^ 2 / c + b * y ^ 2) = (1 / (1 - c * b)) ^ (1 / 2) * Real.exp (b / (1 - c * b) * a ^ 2)

One-dimensional Gaussian convolution-style integral evaluated via completing the square: $\int_{\mathbb R} \frac{1}{\sqrt{\pi c}} \exp(-(a-y)^2/c + b y^2)\,dy = (1 - cb)^{-1/2}\, \exp\bigl(b/(1-cb)\cdot a^2\bigr)$ when $cb < 1$.

theorem HeatFundamental.heatKernel_exp_prod_aux {n : ℕ} (D t b : ℝ) (hD : 0 < D) (ht : 0 < t) (x : Fin n → ℝ) : (fun (y : Fin n → ℝ) => heatKernel D t (x - y) * Real.exp (b * euclidNormSq y)) = fun (y : Fin n → ℝ) => ∏ i : Fin n, 1 / (Real.pi * (4 * D * t)) ^ (1 / 2) * Real.exp (-(x i - y i) ^ 2 / (4 * D * t) + b * y i ^ 2)

Factorisation of $\Gamma_D(t, x - y) \cdot \exp(b |y|^2)$ as a product over the coordinates $i = 1, \dots, n$, used to reduce the $n$-dimensional integral to a product of 1D integrals.

theorem HeatFundamental.gaussian_nD_integral_eq {n : ℕ} (D t b : ℝ) (hD : 0 < D) (ht : 0 < t) (hb : 0 < b) (hcb : 4 * D * t * b < 1) (x : Fin n → ℝ) : ∫ (y : Fin n → ℝ), heatKernel D t (x - y) * Real.exp (b * euclidNormSq y) = (1 / (1 - 4 * D * t * b)) ^ (↑n / 2) * Real.exp (b / (1 - 4 * D * t * b) * euclidNormSq x)

Closed-form $n$-dimensional Gaussian-times-Gaussian integral: $\int_{\mathbb R^n} \Gamma_D(t, x - y) \exp(b |y|^2)\,d^n y = (1 - 4Dtb)^{-n/2}\,\exp\bigl(b/(1 - 4Dtb)\cdot |x|^2\bigr)$ when $4Dtb < 1$.

theorem HeatFundamental.gaussian_integral_completing_square {n : ℕ} {D : ℝ} (hD : 0 < D) {b : ℝ} (hb : 0 < b) {t T' : ℝ} (ht : 0 < t) (htT' : t ≤ T') (hT'bound : T' < 1 / (4 * D * b)) (x : Fin n → ℝ) : ∫ (y : Fin n → ℝ), heatKernel D t (x - y) * Real.exp (b * euclidNormSq y) ≤ (1 / (1 - 4 * D * T' * b)) ^ (↑n / 2) * Real.exp (b / (1 - 4 * D * T' * b) * euclidNormSq x)

Uniform-in-$t$ upper bound on the closed-form integral $\int \Gamma_D(t, x-y) e^{b |y|^2}$, replacing $t$ by an upper bound $T'$ in the resulting prefactor and exponent.

theorem HeatFundamental.integrable_majorant_heatKernel {n : ℕ} {D : ℝ} (hD : 0 < D) {a b : ℝ} (hb : 0 < b) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => a * Real.exp (b * euclidNormSq y) * heatKernel D t (x - y)) MeasureTheory.volume

Integrability of the dominating function $y \mapsto a \exp(b |y|^2)\, \Gamma_D(t, x - y)$ when $t < 1/(4Db)$.

theorem HeatFundamental.gaussian_convolution_uniform_bound {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {T' : ℝ} (hT' : 0 < T') (hT'bound : T' < 1 / (4 * D * b)) (t : ℝ) (x : Fin n → ℝ) : 0 ≤ t → t ≤ T' → |cauchySolution D g t x| ≤ a * (1 / (1 - 4 * D * T' * b)) ^ (↑n / 2) * Real.exp (b / (1 - 4 * D * T' * b) * euclidNormSq x)

Uniform Gaussian growth bound on the Cauchy convolution solution over the strip $[0, T'] \times \mathbb R^n$ (with $T' < 1/(4Db)$): $|u(t, x)| \le a\,(1 - 4DT'b)^{-n/2}\,\exp\bigl(b/(1 - 4DT'b)\cdot |x|^2\bigr)$.

theorem HeatFundamental.gaussian_integral_growth_bound {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) (T' : ℝ) : 0 < T' → T' < 1 / (4 * D * b) → ∃ (A : ℝ) (B : ℝ), 0 < A ∧ 0 < B ∧ ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t ≤ T' → |cauchySolution D g t x| ≤ A * Real.exp (B * euclidNormSq x)

Existence of explicit growth constants $A, B > 0$ such that for any $T'$ in the admissible range, $|u(t, x)| \le A \exp(B |x|^2)$ on $[0, T'] \times \mathbb R^n$.

theorem HeatFundamental.leibniz_heat_operator_commutes {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) {t : ℝ} (ht : 0 < t) (htb : t < 1 / (4 * D * b)) (x : Fin n → ℝ) : heatOperator D (cauchySolution D g) t x = ∫ (y : Fin n → ℝ), g y * heatOperator D (fun (s : ℝ) (z : Fin n → ℝ) => heatKernel D s z) t (x - y)

Re-export of leibniz_heat_operator_commutes_axiom: the heat operator commutes with convolution against $g$ over the admissible $(t, x)$ strip.

theorem HeatFundamental.cauchy_solution_smooth {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) : ContDiffOn ℝ ⊤ (fun (p : ℝ × (Fin n → ℝ)) => cauchySolution D g p.1 p.2) (Set.Ioo 0 (1 / (4 * D * b)) ×ˢ Set.univ)

The Cauchy convolution solution is $C^\infty$ on $(0, 1/(4Db)) \times \mathbb R^n$.

theorem HeatFundamental.cauchy_solution_growth_bound {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) (T' : ℝ) : 0 < T' → T' < 1 / (4 * D * b) → ∃ (A : ℝ) (B : ℝ), 0 < A ∧ 0 < B ∧ ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t ≤ T' → |cauchySolution D g t x| ≤ A * Real.exp (B * euclidNormSq x)

For each compact sub-interval $[0, T'] \subset [0, 1/(4Db))$, the Cauchy solution admits a uniform Gaussian growth bound $|u(t, x)| \le A \exp(B|x|^2)$.

theorem HeatFundamental.heat_cauchy_solves_heat {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) (t : ℝ) : 0 < t → t < 1 / (4 * D * b) → ∀ (x : Fin n → ℝ), heatOperator D (cauchySolution D g) t x = 0

The Cauchy convolution solution $(g * \Gamma_D)(t, x)$ satisfies the homogeneous heat equation $u_t - D \Delta u = 0$ on $(0, 1/(4Db)) \times \mathbb R^n$.

theorem HeatFundamental.cauchy_convolution_change_of_var {n : ℕ} {D : ℝ} {g : (Fin n → ℝ) → ℝ} (t : ℝ) (x : Fin n → ℝ) : ∫ (y : Fin n → ℝ), g y * heatKernel D t (x - y) = ∫ (z : Fin n → ℝ), heatKernel D t z * g (x - z)

Symmetry of convolution: $\int g(y)\,\Gamma_D(t, x-y)\,d^n y = \int \Gamma_D(t, z)\,g(x-z)\,d^n z$, via the change of variable $z = x - y$.

theorem HeatFundamental.translated_growth_bound {n : ℕ} {g : (Fin n → ℝ) → ℝ} {a : ℝ} (ha : 0 < a) {b : ℝ} (hb : 0 < b) (hg_bound : ∀ (x : Fin n → ℝ), |g x| ≤ a * Real.exp (b * euclidNormSq x)) (x : Fin n → ℝ) : ∃ (a' : ℝ) (b' : ℝ), 0 ≤ a' ∧ 0 ≤ b' ∧ ∀ (z : Fin n → ℝ), |g (x - z)| ≤ a' * Real.exp (b' * euclidNormSq z)

If $|g(y)| \le a \exp(b |y|^2)$ globally, then the translated function $z \mapsto g(x - z)$ satisfies a Gaussian bound $|g(x - z)| \le a' \exp(b' |z|^2)$ with constants depending on $x$.

theorem HeatFundamental.heat_cauchy_initial_condition {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) (x : Fin n → ℝ) : Filter.Tendsto (fun (t : ℝ) => cauchySolution D g t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g x))

Initial condition for the Cauchy problem: for each $x \in \mathbb R^n$, $\lim_{t \to 0^+} (g * \Gamma_D(t, \cdot))(x) = g(x)$.

theorem HeatFundamental.heat_cauchy_existence {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) : (∀ (t : ℝ), 0 < t → t < 1 / (4 * D * b) → ∀ (x : Fin n → ℝ), heatOperator D (cauchySolution D g) t x = 0) ∧ (∀ (x : Fin n → ℝ), Filter.Tendsto (fun (t : ℝ) => cauchySolution D g t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g x))) ∧ ContDiffOn ℝ ⊤ (fun (p : ℝ × (Fin n → ℝ)) => cauchySolution D g p.1 p.2) (Set.Ioo 0 (1 / (4 * D * b)) ×ˢ Set.univ)

Existence package for the global Cauchy problem (Theorem 1.1, existence part): the Cauchy convolution solution solves the heat equation on the admissible strip, attains the initial data $g$ as $t \to 0^+$, and is $C^\infty$ jointly in $(t, x)$.

theorem HeatFundamental.heat_cauchy_growth_bound {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) (T' : ℝ) : 0 < T' → T' < 1 / (4 * D * b) → ∃ (A : ℝ) (B : ℝ), 0 < A ∧ 0 < B ∧ ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t ≤ T' → |cauchySolution D g t x| ≤ A * Real.exp (B * euclidNormSq x)

Compatibility wrapper for the Theorem 1.1 statement: Gaussian growth bound on $(t, x) \mapsto u(t, x) = (g * \Gamma_D)(t, x)$ over $[0, T'] \times \mathbb R^n$.

theorem HeatFundamental.heat_cauchy_uniqueness {n : ℕ} {D : ℝ} (hD : 0 < D) {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)) (v : ℝ → (Fin n → ℝ) → ℝ) (hv_solves : ∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → heatOperator D v t x = 0) (hv_init : ∀ (x : Fin n → ℝ), Filter.Tendsto (fun (t : ℝ) => v t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g x))) (hv_growth : ∃ (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 = cauchySolution D g t x

Uniqueness part of Theorem 1.1: any other solution $v$ of the heat equation matching the initial data $g$ and satisfying a Gaussian growth bound $|v(t, x)| \le A \exp(B|x|^2)$ must coincide with the Cauchy convolution solution on $(0, 1/(4Db)) \times \mathbb R^n$.

theorem HeatFundamental.theorem_1_1_cauchy_problem {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)) : ∃ (u : ℝ → (Fin n → ℝ) → ℝ), (∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → u t x = ∫ (y : Fin n → ℝ), g y * heatKernel D t (x - y)) ∧ (∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → heatOperator D u t x = 0) ∧ (∀ (x : Fin n → ℝ), Filter.Tendsto (fun (t : ℝ) => u t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (g x))) ∧ ContDiffOn ℝ ⊤ (fun (p : ℝ × (Fin n → ℝ)) => u p.1 p.2) (Set.Ioo 0 (1 / (4 * D * b)) ×ˢ Set.univ) ∧ (∀ (T' : ℝ), 0 < T' → T' < 1 / (4 * D * b) → ∃ (A : ℝ) (B : ℝ), 0 < A ∧ 0 < B ∧ ∀ (t : ℝ) (x : Fin n → ℝ), 0 ≤ t → t ≤ T' → |u t x| ≤ A * Real.exp (B * euclidNormSq x)) ∧ ∀ (v : ℝ → (Fin n → ℝ) → ℝ), (∀ (t : ℝ) (x : Fin n → ℝ), 0 < t → t < 1 / (4 * D * b) → heatOperator D v t x = 0) → (∀ (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

Theorem 1.1 (Global Cauchy problem via the fundamental solution): for continuous initial data $g$ with Gaussian growth $|g(x)| \le a \exp(b |x|^2)$, the function $u(t, x) = (g * \Gamma_D(t, \cdot))(x)$ exists on $[0, 1/(4Db)) \times \mathbb R^n$, solves the homogeneous heat equation with initial condition $u(0, x) = g(x)$, is $C^\infty$ in the interior, satisfies a uniform Gaussian growth bound on each compact sub-interval, and is the unique such solution in this growth class.

theorem HeatFundamental.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 = (∫ (y : Fin n → ℝ), g y * heatKernel D t (x - y)) + ∫ (s : ℝ) in Set.Icc 0 t, ∫ (y : Fin n → ℝ), heatKernel D (t - s) (x - y) * f s y) ∧ (∀ (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

Theorem 1.2 (Duhamel's principle): for continuous initial data $g$ with Gaussian growth and a continuous source term $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 on $[0, 1/(4Db)) \times \mathbb R^n$ given by the convolution $u(t, x) = (g * \Gamma_D(t, \cdot))(x) + \int_0^t (\Gamma_D(t-s, \cdot) * f(s, \cdot))(x)\,ds$, with appropriate continuity and regularity properties.