Links

Stream: Lean for PDEs 2025

[Rémy Degenne]

Here are a few useful links.

Tutorial website: https://github.com/RemyDegenne/GlimpseOfLean

Lean community website, with all kind of information: https://leanprover-community.github.io/
Mathlib documentation (select files in the left column): https://leanprover-community.github.io/mathlib4_docs/
The new members channel on this zulip, for quick help: #new members (you can also ask in this workshop channel)
Mathlib github, with pull requests for new additions: https://github.com/leanprover-community/mathlib4/pulls

[David Renshaw]

This link in the GlimpseOfLean README is broken:

After the basic tutorial, we'll learn about differential calculus and PDEs.

[Rémy Degenne]

Yes it is. To make it less confusing, I'll deactivate the link for now and add a note to say that it will become available tomorrow.

[Michael Rothgang]

Slides from the introductory session: slides.pdf

[David Renshaw]

just for fun, I made an animation of this Introduction proof: https://sandstorm-6bufjh18p7b20s6gumc6.dwrensha.ws/seq_limit_eq.mp4

[Srayan Jana]

Hello all! I'm planning on showing up tomorrow! I live in the area and really want to meet other Lean users, so I hope its okay! I wasn't able to come in today though.;..

[Rémy Degenne]

More links to helpful things:

• Tactic cheatsheet: https://leanprover-community.github.io/papers/lean-tactics.pdf
• Blog post on how to search for theorems in Mathlib: blog post . Highlight: look for theorems with natural language queries at https://leansearch.net

[Jason Reed]

The question just got asked of "how should we read mathlib theorem names" and https://leanprover-community.github.io/contribute/naming.html describes some conventions pertaining to that

[Jason Reed]

But maybe also a right answer to that question might be #check to find out what the theorem's type is really stating.

[Rémy Degenne]

The slides about differential calculus:
derivatives.pdf

[Rémy Degenne]

If you want to do more basic exercises to practice Lean, there are more exercise files on the tutorial repository https://github.com/RemyDegenne/GlimpseOfLean (see the "Online version, no registration" part of the readme, below the files we used yesterday)

[Rémy Degenne]

import Mathlib

noncomputable section
open InnerProductSpace
open scoped Real

section MissingLemmasInMathlib

/-! A few hours ago, Mathlib did not know that the Laplacian in 1D is the second derivative,
so we proved it. -/

variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]

theorem laplacianWithin_eq_iteratedDerivWithin_real {e : ℝ} {s : Set ℝ} (f : ℝ → F)
    (hs : UniqueDiffOn ℝ s) (he : e ∈ s) :
    (Δ[s] f) e = iteratedDerivWithin 2 f s e := by
  simp only [laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he
        (OrthonormalBasis.singleton (Fin 1) ℝ),
    Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, OrthonormalBasis.singleton_apply,
    Finset.sum_const, Finset.card_singleton, one_smul]
  rw [iteratedDerivWithin_eq_iteratedFDerivWithin]
  congr
  ext i; fin_cases i <;> simp

theorem laplacian_eq_iteratedDeriv_real {e : ℝ} (f : ℝ → F) :
    Δ f e = iteratedDeriv 2 f e := by
  rw [← laplacianWithin_univ, laplacianWithin_eq_iteratedDerivWithin_real _ (by simp) (by simp),
    iteratedDerivWithin_univ]

end MissingLemmasInMathlib

/-- A definition of classical solutions to the 1D heat equation. -/
def IsClassical1DHeatSolution (U : Set ℝ) (u : ℝ → ℝ → ℝ) : Prop :=
  ContDiffOn ℝ 2 (fun xt : ℝ × ℝ ↦ u xt.1 xt.2) (U ×ˢ Set.Ioi 0)
    ∧ ∀ x ∈ U, ∀ t, 0 < t → deriv (fun s ↦ u x s) t - Δ (fun y ↦ u y t) x = 0

/-! Let's check a 1D solution. -/

/-- The fundamental solution to the 1D heat equation. -/
def Ψ x t := (√(4 * π * t))⁻¹ * rexp (- x^2 / (4 * t))

/-- First derivative of Ψ with respect to time. -/
lemma deriv_Ψ_t {x t : ℝ} (ht : 0 < t) :
    deriv (fun t ↦ Ψ x t) t = Ψ x t * (-2/t + x^2/t^2) / 4 := by
  unfold Ψ
  rw [deriv_fun_mul, deriv_fun_inv'', deriv_sqrt, deriv_const_mul, deriv_id'', deriv_exp,
    deriv_fun_div, deriv_const, deriv_const_mul, deriv_id'']
  · rw [Real.sq_sqrt (by positivity)]
    grind
  any_goals fun_prop (disch := positivity)
  all_goals positivity

/-- First derivative of Ψ with respect to space. -/
lemma deriv_Ψ_x {x t : ℝ} (ht : 0 < t) :
    deriv (fun x ↦ Ψ x t) x = Ψ x t * (-x / (2 * t)) := by
  unfold Ψ
  simp only [deriv_const_mul_field']
  rw [mul_assoc _ _ (-x / (2 * t))]
  congr
  rw [deriv_exp (by fun_prop)]
  simp only [deriv_div_const, deriv.fun_neg', differentiableAt_fun_id, deriv_fun_pow,
    Nat.cast_ofNat, Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, mul_eq_mul_left_iff,
    Real.exp_ne_zero, or_false]
  field_simp
  ring

/-- Ψ is differentiable in space. -/
@[fun_prop]
lemma differentiableAt_Ψ (x t : ℝ) : DifferentiableAt ℝ (fun x ↦ Ψ x t) x := by
  unfold Ψ
  fun_prop

/-- Second derivative of Ψ with respect to space. -/
lemma iteratedDeriv_two_Ψ_x {x t : ℝ} (ht : 0 < t) :
    iteratedDeriv 2 (fun x ↦ Ψ x t) x = Ψ x t * (-2/t + x^2/t^2) / 4 := by
  rw [iteratedDeriv_succ, iteratedDeriv_one] -- copilot wrote that
  suffices deriv (fun x ↦ Ψ x t * (-x / (2 * t))) x = Ψ x t * (-2 / t + x ^ 2 / t ^ 2) / 4 by
    convert this using 2
    ext x
    exact deriv_Ψ_x ht
  rw [deriv_fun_mul (by fun_prop) (by fun_prop), deriv_Ψ_x ht]
  simp only [deriv_div_const, deriv_neg'']
  grind

/-- Ψ is twice continuously differentiable on ℝ × (0, ∞). -/
lemma condDiff_two_Ψ : ContDiffOn ℝ 2 (fun xt : ℝ × ℝ ↦ Ψ xt.1 xt.2) (Set.univ ×ˢ Set.Ioi 0) := by
  unfold Ψ
  rintro ⟨x, t⟩ ht
  simp only [Set.mem_prod, Set.mem_univ, Set.mem_Ioi, true_and] at ht
  fun_prop (disch := positivity)

/-- Ψ is a classical solution to the 1D heat equation on ℝ × (0, ∞). -/
theorem isClassical1DHeatSolution_Ψ :
    IsClassical1DHeatSolution (Set.univ : Set ℝ) Ψ := by
  constructor
  · exact condDiff_two_Ψ
  · intros x hx t ht
    rw [laplacian_eq_iteratedDeriv_real, deriv_Ψ_t ht, iteratedDeriv_two_Ψ_x ht]
    ring

open MeasureTheory

/-- The integral of Ψ over space is 1 for any positive time. -/
theorem integral_Ψ {t : ℝ} (ht : 0 < t) : ∫ x, Ψ x t = 1 := by
  unfold Ψ
  have h_gaussian : ∫ x, rexp (-x ^ 2 / (4 * t)) = √(π / (1 / (4 * t))) := by
    convert integral_gaussian (1 / (4 * t)) using 4 with x
    ring
  rw [integral_const_mul, h_gaussian]
  field_simp