Heat equation

DefinitionHeat-kernel solution#✓fully proved

For \(f\colon \mathbb{R} \to \mathbb{R}\), the heat solution \(u(t, x)\) of \(f\) is given for \(t > 0\) by

\[u(t, x) = (4 \pi t)^{-1/2} \int_{\mathbb{R}} e^{-(x - y)^2/(4t)} f(y) \, dy\]

and by \(u(t, x) = f(x)\) for \(t \le 0\).

The integral is the Lebesgue integral, taken to be \(0\) when the integrand is not integrable. The value for \(t \le 0\) only makes \(u\) defined for all real \(t\) and \(x\); the heat equation statement constrains \(u\) only for \(t > 0\).

noncomputable def heatSolution (f : ℝ → ℝ) (t x : ℝ) : ℝ :=
  if 0 < t then
    (4 * Real.pi * t)⁻¹ ^ ((1 : ℝ) / 2) *
      ∫ y : ℝ, Real.exp (-((x - y) ^ 2) / (4 * t)) * f y
  else
    f x

Used by 1

Used byThe Gaussian heat kernel solves the heat equation

TheoremThe Gaussian heat kernel solves the heat equation#●ready to prove

Let \(f\colon \mathbb{R} \to \mathbb{R}\) be continuous and bounded, and let \(u(t, x)\) be the heat solution of \(f\). Then for every \(t > 0\) and every \(x \in \mathbb{R}\) there are a function \(u_x\colon \mathbb{R} \to \mathbb{R}\) and a real number \(u_{xx}\) such that \(u(t, \cdot)\) has derivative \(u_x(y)\) at every \(y \in \mathbb{R}\), \(u_x\) has derivative \(u_{xx}\) at \(x\), and \(u(\cdot, x)\) has derivative \(u_{xx}\) at \(t\); that is, \(\partial_t u = \partial_x^2 u\) on \((0, \infty) \times \mathbb{R}\). Moreover, for every \(x \in \mathbb{R}\), \(u(t, x) \to f(x)\) as \(t \to 0\) from above.

public theorem_wanted heat_kernel_solves_heat_equation
    (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) :
    -- The PDE on (0, ∞) × ℝ.
    (∀ t : ℝ, 0 < t → ∀ x : ℝ, ∃ ux : ℝ → ℝ, ∃ uxx : ℝ,
        (∀ y : ℝ, HasDerivAt (fun z => heatSolution f t z) (ux y) y) ∧
        HasDerivAt ux uxx x ∧
        HasDerivAt (fun s => heatSolution f s x) uxx t) ∧
    -- Initial condition recovered as a one-sided limit at t = 0.
    (∀ x : ℝ,
        Filter.Tendsto (fun t : ℝ => heatSolution f t x)
          (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (f x)))

Sources

• Classical heat-equation theory. Problem heat_kernel_solves_heat_equation of the lean-eval benchmark.

Uses 1

Statement usesHeat-kernel solution

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.