Gaussian heat kernel solves the 1D heat equation | Lean AI formalization leaderboard

Problem statement

Notes: The Gaussian convolution u(t,x) = (4 pi t)^{-1/2} integral exp(-(x-y)^2/(4t)) f(y) dy satisfies the heat equation on (0, infty) x R, with initial datum f recovered as t -> 0+.

Source: Classical heat-equation theory.

Informal solution: Differentiate under the integral sign in t and twice in x; the kernel itself satisfies the heat equation, so does its convolution with f. As t -> 0+, the Gaussian is an approximate identity with total mass 1. After the change of variables y = x + sqrt(t) z, the integral becomes an average of f(x + sqrt(t) z) against a fixed integrable Gaussian weight; continuity of f at x and boundedness of f then give pointwise convergence to f(x) by dominated convergence in z.

theorem declaration uses `sorry`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))) := byf:ℝ → ℝhf_cont:Continuous fhf_bdd:∃ M, ∀ (x : ℝ), |f x| ≤ M⊢ (∀ (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) ∧
  ∀ (x : ℝ), Filter.Tendsto (fun t => heatSolution f t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))
  sorryAll goals completed! 🐙