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

The (spatial) Laplacian of $f : \mathbb{R}^n \to \mathbb{R}$ at $x$, defined as $\Delta f(x) = \sum_{i=1}^{n} \partial_i^2 f(x)$.

noncomputable def HeatEquationInvariance.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)$, where $D > 0$ is the diffusion constant.

theorem HeatEquationInvariance.deriv_const_mul_fn (A : ℝ) (f : ℝ → ℝ) (t : ℝ) : deriv (fun (s : ℝ) => A * f s) t = A * deriv f t

Constants pull out of the time derivative: $\frac{d}{dt}(A f(t)) = A f'(t)$.

theorem HeatEquationInvariance.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 of the Laplacian under scalar multiplication: $\Delta(A f) = A\,\Delta f$.

theorem HeatEquationInvariance.deriv_time_translate {n : ℕ} (u : ℝ → (Fin n → ℝ) → ℝ) (t₀ t : ℝ) (x : Fin n → ℝ) : deriv (fun (s : ℝ) => u (s - t₀) x) t = deriv (fun (s : ℝ) => u s x) (t - t₀)

Time-shift identity for the time derivative: $\partial_t [u(t - t_0, x)] = (\partial_t u)(t - t_0, x)$.

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

Spatial translation commutes with the Laplacian: $\Delta(f(\cdot - x_0))(x) = (\Delta f)(x - x_0)$.

theorem HeatEquationInvariance.deriv_time_dilate {n : ℕ} (u : ℝ → (Fin n → ℝ) → ℝ) (lam t : ℝ) (x : Fin n → ℝ) : deriv (fun (s : ℝ) => u (lam ^ 2 * s) x) t = lam ^ 2 * deriv (fun (s : ℝ) => u s x) (lam ^ 2 * t)

Parabolic dilation in time: $\partial_t [u(\lambda^2 t, x)] = \lambda^2 (\partial_t u)(\lambda^2 t, x)$.

theorem HeatEquationInvariance.laplacian_dilate {n : ℕ} (f : (Fin n → ℝ) → ℝ) (lam : ℝ) (x : Fin n → ℝ) : laplacian (fun (y : Fin n → ℝ) => f (lam • y)) x = lam ^ 2 * laplacian f (lam • x)

Spatial dilation scales the Laplacian by $\lambda^2$: $\Delta(f(\lambda \cdot))(x) = \lambda^2 (\Delta f)(\lambda x)$.

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

Translation invariance of solutions to the heat equation (Lemma 2.0.2, first part): if $u$ solves $u_t - D \Delta u = 0$, then so does $A\,u(t - t_0, x - x_0)$ for any constants $A, t_0 \in \mathbb{R}$ and $x_0 \in \mathbb{R}^n$.

theorem HeatEquationInvariance.heat_parabolic_dilation {n : ℕ} {D : ℝ} (_hD : D > 0) (u : ℝ → (Fin n → ℝ) → ℝ) (hu : ∀ (t : ℝ) (x : Fin n → ℝ), heatOperator D u t x = 0) (A lam : ℝ) (_hlam : lam > 0) (t : ℝ) (x : Fin n → ℝ) : heatOperator D (fun (t : ℝ) (x : Fin n → ℝ) => A * u (lam ^ 2 * t) (lam • x)) t x = 0

Parabolic dilation invariance of solutions to the heat equation (Lemma 2.0.2, second part): if $u$ solves $u_t - D \Delta u = 0$, then so does $A\,u(\lambda^2 t, \lambda x)$ for any $A \in \mathbb{R}$ and $\lambda > 0$.

theorem HeatEquationInvariance.heat_equation_invariance {n : ℕ} {D : ℝ} (hD : D > 0) (u : ℝ → (Fin n → ℝ) → ℝ) (hu : ∀ (t : ℝ) (x : Fin n → ℝ), heatOperator D u t x = 0) : (∀ (A t₀ : ℝ) (x₀ : Fin n → ℝ) (t : ℝ) (x : Fin n → ℝ), heatOperator D (fun (t : ℝ) (x : Fin n → ℝ) => A * u (t - t₀) (x - x₀)) t x = 0) ∧ ∀ (A lam : ℝ), lam > 0 → ∀ (t : ℝ) (x : Fin n → ℝ), heatOperator D (fun (t : ℝ) (x : Fin n → ℝ) => A * u (lam ^ 2 * t) (lam • x)) t x = 0

Lemma 2.0.2 (combined): solutions to the heat equation are invariant under amplification combined with translations and parabolic dilations.