AcceptedTheorem · Statement with omitted proof

Heat-kernel solution for bounded continuous data

Convolution with the heat kernel solves the heat equation at positive times and approaches the initial value at each point.

Larsson & Thomée ↗
Theorem 8.1 · printed p. 110

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Convolution with the heat kernel solves the heat equation at positive times and approaches the initial value at each point.

u(x,t)=(G_t*v)(x),\qquad u_t=\Delta u\ (t>0),\qquad \lim_{t\downarrow0}u(x,t)=v(x).

Assumptions & context

Bounded continuous initial data on Euclidean space.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem 8.1 · printed p. 110

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem thm_8_1 {d : ℕ} (v : Euclidean d → ℝ)
    (hv_cont : Continuous v) (hv_bdd : ∃ C : ℝ, ∀ x, |v x| ≤ C) :
    IsHeatSolutionPosTime (heatConvolution v) ∧
    ∀ x : Euclidean d,
      Filter.Tendsto (fun t => heatConvolution v x t)
        (nhdsWithin 0 (Set.Ioi 0)) (nhds (v x)) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm81

/-- The function `u(x,t)` of (8.3):
`u(x,t) = (4πt)^{-d/2} ∫_{ℝ^d} v(y) e^{-|x-y|²/4t} dy`. -/
def heatConvolution {d : ℕ} (v : Euclidean d → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
  (4 * Real.pi * t) ^ (-(d : ℝ) / 2) *
    ∫ y : Euclidean d, v y * Real.exp (-‖x - y‖ ^ 2 / (4 * t))

/-- Spatial Laplacian `Δu(x,t) = ∑_i ∂²u/∂x_i²(x,t)` (classical second partials in `x`). -/
def spatialLaplacian {d : ℕ} (u : Euclidean d → ℝ → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
  ∑ i : Fin d, partialDeriv (fun y => partialDeriv (fun z => u z t) i y) i x

/-- `u` is a (classical) solution of the heat equation `∂u/∂t = Δu` in `ℝ^d` for `t > 0`:
for each `t > 0`, `u(·,t)` is twice continuously differentiable in `x`, and at every
`(x,t)` with `t > 0` the time derivative exists and equals the spatial Laplacian. -/
def IsHeatSolutionPosTime {d : ℕ} (u : Euclidean d → ℝ → ℝ) : Prop :=
  ∀ t : ℝ, 0 < t →
    ContDiff ℝ 2 (fun y => u y t) ∧
    ∀ x : Euclidean d, HasDerivAt (fun s => u x s) (spatialLaplacian u x t) t

/-- Theorem 8.1. If `v` is a bounded continuous function on `ℝ^d`, then `u` defined by (8.3)
solves the heat equation for `t > 0` and `u(x,t) → v(x)` as `t → 0⁺`. -/
theorem thm_8_1 {d : ℕ} (v : Euclidean d → ℝ)
    (hv_cont : Continuous v) (hv_bdd : ∃ C : ℝ, ∀ x, |v x| ≤ C) :
    IsHeatSolutionPosTime (heatConvolution v) ∧
    ∀ x : Euclidean d,
      Filter.Tendsto (fun t => heatConvolution v x t)
        (nhdsWithin 0 (Set.Ioi 0)) (nhds (v x)) := by
  sorry

end PDETextbook.LarssonThomee.Thm81

How to read the formalization

The initial limit is pointwise as time approaches zero from above; the statement does not assert uniform convergence over the whole space.

← Back to all statements