Skip to content

Instantly share code, notes, and snippets.

@kim-em

kim-em/Challenge.lean

Created May 3, 2026 10:25
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save kim-em/f796143690a6c9ba2312f7a7956efbdc to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save kim-em/f796143690a6c9ba2312f7a7956efbdc to your computer and use it in GitHub Desktop.
Download ZIP
lean-eval Aristotle (Harmonic) submission for heat_kernel_solves_heat_equation
Raw
Challenge.lean
import ChallengeDeps
open LeanEval.Analysis.ODE
open Real MeasureTheory
theorem 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))) := by
sorry
Raw
config.json
{
"challenge_module": "Challenge",
"solution_module": "Solution",
"theorem_names": [
"heat_kernel_solves_heat_equation"
],
"permitted_axioms": [
"propext",
"Quot.sound",
"Classical.choice"
],
"enable_nanoda": false
}
Raw
Helpers.lean
namespace Submission.Helpers
end Submission.Helpers
Raw
lakefile.toml
name = "heat_kernel_solves_heat_equation"
testDriver = "workspace_test"
defaultTargets = ["Challenge", "Solution", "Submission"]
[leanOptions]
autoImplicit = false
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "5450b53e5ddc"
[[lean_lib]]
name = "ChallengeDeps"
[[lean_lib]]
name = "Challenge"
[[lean_lib]]
name = "Solution"
[[lean_lib]]
name = "Submission"
[[lean_exe]]
name = "workspace_test"
root = "WorkspaceTest"
Raw
lean-toolchain
leanprover/lean4:v4.30.0-rc2
Raw
Solution.lean
import ChallengeDeps
import Submission
open LeanEval.Analysis.ODE
open Real MeasureTheory
theorem 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))) := by
exact Submission.heat_kernel_solves_heat_equation f hf_cont hf_bdd
Raw
Submission.lean
import ChallengeDeps
open LeanEval.Analysis.ODE
open Real MeasureTheory
namespace Submission
-- ============================================================================
-- Helper lemmas
-- ============================================================================
noncomputable section
open Filter Topology
/-- When `t > 0`, the `if` in heatKernel drops away. -/
lemma heatKernel_of_pos {t : ℝ} (ht : 0 < t) (x : ℝ) :
heatKernel t x = (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-(x ^ 2 / (4 * t))) := by
simp [heatKernel, not_le.mpr ht]
/-- The prefactor `(√(4πt))⁻¹` is positive for `t > 0`. -/
lemma heatKernel_prefactor_pos {t : ℝ} (ht : 0 < t) :
0 < (Real.sqrt (4 * Real.pi * t))⁻¹ := by
positivity
/-- `heatKernel t x ≥ 0` for `t > 0`. -/
lemma heatKernel_nonneg {t : ℝ} (ht : 0 < t) (x : ℝ) : 0 ≤ heatKernel t x := by
rw [heatKernel_of_pos ht]
positivity
/-
The heat kernel integrates to 1 over ℝ.
-/
lemma heatKernel_integral_one {t : ℝ} (ht : 0 < t) :
∫ x, heatKernel t x = 1 := by
rw [ MeasureTheory.integral_congr_ae, MeasureTheory.integral_const_mul ];
case r => exact ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹;
rotate_left;
exact fun x => Real.exp ( -x ^ 2 / ( 4 * t ) );
· filter_upwards [ ] with x using by rw [ heatKernel_of_pos ht ] ; ring;
· rw [ inv_mul_eq_div, div_eq_iff ] <;> first | positivity | have := integral_gaussian ( 1 / ( 4 * t ) ) ; simp_all +decide [ div_eq_inv_mul ] ;
ring
/-- The heat kernel (for fixed t > 0) is continuous in x. -/
lemma heatKernel_continuous {t : ℝ} (ht : 0 < t) : Continuous (heatKernel t) := by
have : heatKernel t = fun x => (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-(x ^ 2 / (4 * t))) :=
funext (heatKernel_of_pos ht)
rw [this]; fun_prop
/-- The heat kernel is integrable (for fixed t > 0). -/
lemma heatKernel_integrable {t : ℝ} (ht : 0 < t) : Integrable (heatKernel t) volume :=
integrable_of_integral_eq_one (heatKernel_integral_one ht)
/-
The integrand `heatKernel t (x - ·) * f ·` is integrable when `f` is bounded and continuous.
-/
lemma heatSolution_integrable {f : ℝ → ℝ} {t : ℝ} (ht : 0 < t)
(hf_cont : Continuous f) (hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) :
Integrable (fun y => heatKernel t (x - y) * f y) volume := by
have h_integrable : Integrable (fun y => heatKernel t (x - y) * hf_bdd.choose) volume := by
exact MeasureTheory.Integrable.mul_const ( MeasureTheory.Integrable.comp_sub_left ( heatKernel_integrable ht ) x ) _;
refine' h_integrable.norm.mono' _ _;
· exact MeasureTheory.AEStronglyMeasurable.mul ( by exact Continuous.aestronglyMeasurable ( by exact heatKernel_continuous ht |> Continuous.comp <| continuous_const.sub continuous_id' ) ) hf_cont.aestronglyMeasurable;
· simp +zetaDelta at *;
filter_upwards [ ] with y using mul_le_mul_of_nonneg_left ( le_trans ( hf_bdd.choose_spec y ) ( le_abs_self _ ) ) ( abs_nonneg _ )
/-
After substitution u = (x-y)/√(4t), the heat solution becomes
`∫ u, (1/√π) exp(-u²) f(x - u√(4t))`.
-/
lemma heatSolution_substitution {f : ℝ → ℝ} {t : ℝ} (ht : 0 < t) (x : ℝ) :
heatSolution f t x =
∫ u, (Real.sqrt Real.pi)⁻¹ * Real.exp (-(u ^ 2)) * f (x - u * Real.sqrt (4 * t)) := by
-- We'll use the substitution $u = \frac{x - y}{\sqrt{4t}}$ to transform the integral.
have h_subst : ∀ {g : ℝ → ℝ}, ∫ y, g y = ∫ u, g (x - u * Real.sqrt (4 * t)) * Real.sqrt (4 * t) := by
intro g; rw [ MeasureTheory.integral_mul_const ] ; rw [ MeasureTheory.Measure.integral_comp_mul_right ( fun u => g ( x - u ) ) ] ; norm_num [ ht.le ] ;
rw [ abs_of_nonneg ( Real.sqrt_nonneg _ ), MeasureTheory.integral_sub_left_eq_self ] ; ring ; norm_num [ ht.le, ht.ne' ];
convert h_subst using 3;
unfold heatKernel; norm_num [ ht.le ] ; ring;
grind
/-
`(√π)⁻¹ exp(-u²)` integrates to 1.
-/
lemma gauss_normalized :
∫ u : ℝ, (Real.sqrt Real.pi)⁻¹ * Real.exp (-(u ^ 2)) = 1 := by
rw [ MeasureTheory.integral_const_mul, show ∫ u : ℝ, Real.exp ( -u ^ 2 ) = Real.sqrt Real.pi by simpa using integral_gaussian ( 1 : ℝ ) ] ; norm_num [ ne_of_gt, Real.pi_pos ]
/-
============================================================================
Part 2: Initial condition
============================================================================
As `t → 0⁺`, `heatSolution f t x → f x`.
-/
lemma heatSolution_initial (f : ℝ → ℝ) (hf_cont : Continuous f)
(hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) (x : ℝ) :
Tendsto (fun t => heatSolution f t x)
(nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (f x)) := by
-- Use the substitution $u = \frac{x - y}{\sqrt{4t}}$ to rewrite the integral.
suffices h_subst : Filter.Tendsto (fun t => ∫ u, (Real.sqrt Real.pi)⁻¹ * Real.exp (-(u ^ 2)) * f (x - u * Real.sqrt (4 * t))) (𝓝[>] 0) (𝓝 (f x)) by
exact h_subst.congr' ( Filter.eventuallyEq_of_mem self_mem_nhdsWithin fun t ht => by rw [ heatSolution_substitution ht ] );
-- Apply the dominated convergence theorem.
have h_dominated : Filter.Tendsto (fun t => ∫ u, (Real.sqrt Real.pi)⁻¹ * Real.exp (-(u ^ 2)) * f (x - u * Real.sqrt (4 * t))) (𝓝[>] 0) (𝓝 (∫ u, (Real.sqrt Real.pi)⁻¹ * Real.exp (-(u ^ 2)) * f x)) := by
refine' MeasureTheory.tendsto_integral_filter_of_dominated_convergence _ _ _ _ _;
refine' fun u => ( Real.sqrt Real.pi ) ⁻¹ * Real.exp ( -u ^ 2 ) * hf_bdd.choose;
· exact Filter.Eventually.of_forall fun t => Continuous.aestronglyMeasurable ( by continuity );
· filter_upwards [ self_mem_nhdsWithin ] with t ht using Filter.Eventually.of_forall fun u => by simpa [ abs_mul, abs_inv, abs_of_nonneg ( Real.sqrt_nonneg _ ), abs_of_nonneg ( Real.exp_pos _ |> le_of_lt ) ] using mul_le_mul_of_nonneg_left ( hf_bdd.choose_spec _ ) ( by positivity ) ;
· exact MeasureTheory.Integrable.mul_const ( MeasureTheory.Integrable.const_mul ( by simpa using ( integrable_exp_neg_mul_sq ( by norm_num : ( 0 : ℝ ) < 1 ) ) ) _ ) _;
· exact Filter.Eventually.of_forall fun u => tendsto_const_nhds.mul ( hf_cont.continuousAt.tendsto.comp <| tendsto_nhdsWithin_of_tendsto_nhds <| Continuous.tendsto' ( by continuity ) _ _ <| by norm_num );
convert h_dominated using 2 ; norm_num [ MeasureTheory.integral_const_mul, MeasureTheory.integral_mul_const, gauss_normalized ];
have := integral_gaussian ( 1 : ℝ ) ; norm_num at this ; rw [ this ] ; ring ; norm_num [ Real.sqrt_ne_zero'.mpr Real.pi_pos ]
-- ============================================================================
-- Part 1: PDE — differentiation under the integral
-- ============================================================================
/-- Derivative of heatKernel w.r.t. x -/
noncomputable def heatKernel_dx (t : ℝ) (x : ℝ) : ℝ :=
if t ≤ 0 then 0
else (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-(x ^ 2 / (4 * t))) * (-(x / (2 * t)))
/-- Second derivative of heatKernel w.r.t. x -/
noncomputable def heatKernel_dxx (t : ℝ) (x : ℝ) : ℝ :=
if t ≤ 0 then 0
else (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-(x ^ 2 / (4 * t))) *
(x ^ 2 / (4 * t ^ 2) - 1 / (2 * t))
/-
`heatKernel t` has derivative `heatKernel_dx t` at `x`.
-/
lemma heatKernel_hasDerivAt_x {t : ℝ} (ht : 0 < t) (x : ℝ) :
HasDerivAt (heatKernel t) (heatKernel_dx t x) x := by
convert HasDerivAt.congr_of_eventuallyEq _ ?_ using 1;
exact fun x => ( Real.sqrt ( t * 4 * Real.pi ) ) ⁻¹ * Real.exp ( - ( x ^ 2 / ( 4 * t ) ) );
· convert HasDerivAt.const_mul _ ( HasDerivAt.exp ( HasDerivAt.neg ( HasDerivAt.div_const ( hasDerivAt_pow 2 x ) _ ) ) ) using 1 ; ring;
unfold heatKernel_dx; norm_num [ ht.le ] ; ring;
grind;
· filter_upwards [ ] using fun x => by unfold heatKernel; rw [ if_neg ( by linarith ) ] ; ring
/-
`heatKernel_dx t` has derivative `heatKernel_dxx t` at `x`.
-/
lemma heatKernel_hasDerivAt_xx {t : ℝ} (ht : 0 < t) (x : ℝ) :
HasDerivAt (heatKernel_dx t) (heatKernel_dxx t x) x := by
convert HasDerivAt.congr_of_eventuallyEq _ ?_ using 1;
exact fun x => ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ * Real.exp ( - ( x ^ 2 / ( 4 * t ) ) ) * ( - ( x / ( 2 * t ) ) );
· convert HasDerivAt.mul ( HasDerivAt.mul ( hasDerivAt_const _ _ ) ( HasDerivAt.exp ( HasDerivAt.neg ( HasDerivAt.div_const ( hasDerivAt_pow 2 x ) _ ) ) ) ) ( HasDerivAt.neg ( HasDerivAt.div_const ( hasDerivAt_id x ) _ ) ) using 1 ; norm_num [ heatKernel_dxx ] ; ring;
grind;
· exact Filter.eventuallyEq_of_mem ( Metric.ball_mem_nhds _ ht ) fun y hy => if_neg <| not_le_of_gt <| by linarith [ abs_lt.mp hy.out ] ;
/-
The first spatial derivative of heatSolution: differentiate under the integral.
-/
lemma heatSolution_hasDerivAt_x (f : ℝ → ℝ) (hf_cont : Continuous f)
(hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) {t : ℝ} (ht : 0 < t) (x : ℝ) :
HasDerivAt (fun z => heatSolution f t z)
(∫ y, heatKernel_dx t (x - y) * f y) x := by
-- By the mean value theorem, we can write the difference quotient as an integral.
have h_mean_value : ∀ h ≠ 0, (heatSolution f t (x + h) - heatSolution f t x) / h = ∫ y, (∫ u in (0 : ℝ)..1, heatKernel_dx t (x - y + u * h)) * f y := by
intro h hh
have h_mean_value : ∀ y, (heatKernel t (x + h - y) - heatKernel t (x - y)) = h * ∫ u in (0 : ℝ)..1, heatKernel_dx t (x - y + u * h) := by
intro y
have h_mean_value : ∀ a b, ∫ u in a..b, heatKernel_dx t (x - y + u * h) = (1 / h) * (heatKernel t (x - y + b * h) - heatKernel t (x - y + a * h)) := by
intro a b; rw [ intervalIntegral.integral_comp_mul_right ( fun u => heatKernel_dx t ( x - y + u ) ) ] <;> norm_num [ hh ] ; ring;
rw [ intervalIntegral.integral_eq_sub_of_hasDerivAt ];
· exact fun u hu => heatKernel_hasDerivAt_x ht u;
· apply_rules [ Continuous.intervalIntegrable ];
exact Continuous.congr ( show Continuous fun x => ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ * Real.exp ( - ( x ^ 2 / ( 4 * t ) ) ) * ( - ( x / ( 2 * t ) ) ) from by continuity ) fun x => by unfold heatKernel_dx; aesop;
grind;
have h_integral_mean_value : ∫ y, (heatKernel t (x + h - y) - heatKernel t (x - y)) * f y = h * ∫ y, (∫ u in (0 : ℝ)..1, heatKernel_dx t (x - y + u * h)) * f y := by
simp +decide only [h_mean_value, mul_assoc, integral_const_mul];
convert congr_arg ( fun z => z / h ) h_integral_mean_value using 1;
· simp +decide only [heatSolution, sub_mul];
rw [ MeasureTheory.integral_sub ];
· exact?;
· exact?;
· rw [ mul_div_cancel_left₀ _ hh ];
-- To apply the dominated convergence theorem, we need to show that the integrand is dominated by an integrable function.
have h_dominate : ∀ h : ℝ, ∀ y : ℝ, |(∫ u in (0 : ℝ)..1, heatKernel_dx t (x - y + u * h)) * f y| ≤ (∫ u in (0 : ℝ)..1, |heatKernel_dx t (x - y + u * h)|) * |f y| := by
intro h y; rw [ intervalIntegral.integral_of_le zero_le_one, intervalIntegral.integral_of_le zero_le_one ] ; simp +decide [ abs_mul, MeasureTheory.integral_const_mul ] ;
exact mul_le_mul_of_nonneg_right ( MeasureTheory.norm_integral_le_integral_norm ( _ : ℝ → ℝ ) ) ( abs_nonneg _ );
-- To apply the dominated convergence theorem, we need to show that the integrand is dominated by an integrable function. We'll use the fact that |heatKernel_dx t (x - y + u * h)| is bounded.
have h_bound : ∃ C : ℝ, ∀ y : ℝ, ∀ h : ℝ, |h| ≤ 1 → ∫ u in (0 : ℝ)..1, |heatKernel_dx t (x - y + u * h)| ≤ C * (1 + |x - y|) * Real.exp (-(x - y)^2 / (8 * t)) := by
-- We'll use the fact that |heatKernel_dx t (x - y + u * h)| is bounded by a constant times (1 + |x - y|) * exp(-(x - y)^2 / (8 * t)).
have h_bound : ∃ C : ℝ, ∀ y : ℝ, ∀ u : ℝ, |u| ≤ 1 → |heatKernel_dx t (x - y + u)| ≤ C * (1 + |x - y|) * Real.exp (-(x - y)^2 / (8 * t)) := by
-- We'll use the fact that |heatKernel_dx t (x - y + u)| is bounded by a constant times (1 + |x - y|) * exp(-(x - y)^2 / (8 * t)). This follows from the properties of the Gaussian function and the fact that |u| ≤ 1.
have h_bound : ∃ C : ℝ, ∀ y : ℝ, ∀ u : ℝ, |u| ≤ 1 → |(x - y + u) * Real.exp (-(x - y + u)^2 / (4 * t))| ≤ C * (1 + |x - y|) * Real.exp (-(x - y)^2 / (8 * t)) := by
use 2 * Real.exp (1 / (4 * t));
intro y u hu
have h_exp_bound : Real.exp (-(x - y + u)^2 / (4 * t)) ≤ Real.exp (1 / (4 * t)) * Real.exp (-(x - y)^2 / (8 * t)) := by
rw [ ← Real.exp_add ] ; ring_nf ; norm_num;
nlinarith [ sq_nonneg ( x - y - 2 * u ), sq_nonneg ( x - y + 2 * u ), abs_le.mp hu, inv_pos.mpr ht, mul_inv_cancel₀ ht.ne' ];
rw [ abs_mul, abs_of_nonneg ( Real.exp_pos _ |> LT.lt.le ) ];
refine le_trans ( mul_le_mul_of_nonneg_right ( show |x - y + u| ≤ 1 + |x - y| by cases abs_cases ( x - y + u ) <;> cases abs_cases ( x - y ) <;> linarith [ abs_le.mp hu ] ) ( Real.exp_nonneg _ ) ) ?_;
nlinarith [ show 0 ≤ ( 1 + |x - y| ) * Real.exp ( 1 / ( 4 * t ) ) * Real.exp ( - ( x - y ) ^ 2 / ( 8 * t ) ) by positivity, show 0 ≤ ( 1 + |x - y| ) * Real.exp ( - ( x - y + u ) ^ 2 / ( 4 * t ) ) by positivity, Real.exp_pos ( 1 / ( 4 * t ) ), Real.exp_pos ( - ( x - y ) ^ 2 / ( 8 * t ) ), Real.exp_pos ( - ( x - y + u ) ^ 2 / ( 4 * t ) ) ];
unfold heatKernel_dx;
obtain ⟨ C, hC ⟩ := h_bound;
use C * (Real.sqrt (4 * Real.pi * t))⁻¹ * (1 / (2 * t));
intro y u hu; split_ifs <;> simp_all +decide [ abs_mul, abs_div, abs_neg, abs_of_pos ];
· linarith;
· convert mul_le_mul_of_nonneg_right ( hC y u hu ) ( show 0 ≤ ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ * ( t⁻¹ * 2⁻¹ ) by positivity ) using 1 <;> ring;
rw [ abs_of_nonneg ( Real.sqrt_nonneg _ ) ] ; ring;
obtain ⟨ C, hC ⟩ := h_bound;
use C;
intro y h hh; rw [ intervalIntegral.integral_of_le zero_le_one ] ; refine' le_trans ( MeasureTheory.integral_mono_of_nonneg _ _ _ ) _;
refine' fun u => C * ( 1 + |x - y| ) * Real.exp ( - ( x - y ) ^ 2 / ( 8 * t ) );
· exact Filter.Eventually.of_forall fun _ => abs_nonneg _;
· fun_prop;
· filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Ioc ] with u hu using hC y ( u * h ) ( by rw [ abs_mul ] ; exact mul_le_one₀ ( abs_le.mpr ⟨ by linarith [ hu.1 ], by linarith [ hu.2 ] ⟩ ) ( abs_nonneg _ ) hh );
· norm_num;
-- Using the bound, we can show that the integrand is dominated by an integrable function.
obtain ⟨C, hC⟩ := h_bound;
have h_integrable : MeasureTheory.Integrable (fun y => C * (1 + |x - y|) * Real.exp (-(x - y)^2 / (8 * t)) * |f y|) MeasureTheory.volume := by
have h_integrable : MeasureTheory.Integrable (fun y => (1 + |x - y|) * Real.exp (-(x - y)^2 / (8 * t))) MeasureTheory.volume := by
have h_integrable : MeasureTheory.Integrable (fun y => (1 + |y|) * Real.exp (-y^2 / (8 * t))) MeasureTheory.volume := by
have h_integrable : MeasureTheory.Integrable (fun y => |y| * Real.exp (-y^2 / (8 * t))) MeasureTheory.volume := by
have := @integrable_rpow_mul_exp_neg_mul_sq;
specialize @this ( 1 / ( 8 * t ) ) ( by positivity ) 1 ; norm_num at this;
convert this.norm using 2 ; norm_num ; ring;
norm_num;
simp_all +decide [ add_mul ];
simpa [ div_eq_inv_mul ] using ( integrable_exp_neg_mul_sq ( by positivity ) );
convert h_integrable.comp_sub_left x using 1;
have h_integrable : MeasureTheory.Integrable (fun y => (1 + |x - y|) * Real.exp (-(x - y)^2 / (8 * t)) * |f y|) MeasureTheory.volume := by
refine' h_integrable.norm.mul_const _ |> fun h => h.mono' _ _;
exact hf_bdd.choose;
· exact MeasureTheory.AEStronglyMeasurable.mul ( h_integrable.aestronglyMeasurable ) ( hf_cont.abs.aestronglyMeasurable );
· filter_upwards [ ] using fun y => by simpa [ abs_mul ] using mul_le_mul_of_nonneg_left ( hf_bdd.choose_spec y ) ( by positivity ) ;
simpa only [ mul_assoc ] using h_integrable.const_mul C;
have h_dominated_convergence : Filter.Tendsto (fun h => ∫ y, (∫ u in (0 : ℝ)..1, heatKernel_dx t (x - y + u * h)) * f y) (nhdsWithin 0 {0}ᶜ) (nhds (∫ y, heatKernel_dx t (x - y) * f y)) := by
refine' MeasureTheory.tendsto_integral_filter_of_dominated_convergence _ _ _ _ _;
use fun y => C * ( 1 + |x - y| ) * Real.exp ( - ( x - y ) ^ 2 / ( 8 * t ) ) * |f y|;
· refine' Filter.eventually_of_mem self_mem_nhdsWithin fun n hn => Continuous.aestronglyMeasurable _;
unfold heatKernel_dx;
split_ifs <;> norm_num ; continuity;
fun_prop;
· filter_upwards [ self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds ( Metric.ball_mem_nhds _ zero_lt_one ) ] with n hn hn' using Filter.Eventually.of_forall fun y => le_trans ( h_dominate n y ) ( mul_le_mul_of_nonneg_right ( hC y n ( by simpa using hn'.out.le ) ) ( abs_nonneg _ ) );
· exact h_integrable;
· refine' Filter.Eventually.of_forall fun y => _;
refine' Filter.Tendsto.mul _ tendsto_const_nhds;
have h_cont : Continuous (fun n => ∫ u in (0 : ℝ)..1, heatKernel_dx t (x - y + u * n)) := by
have h_cont : Continuous (fun n => ∫ u in (0 : ℝ)..1, (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-( (x - y + u * n) ^ 2 / (4 * t))) * (-( (x - y + u * n) / (2 * t)))) := by
fun_prop;
convert h_cont using 1;
ext n; refine' intervalIntegral.integral_congr fun u hu => _; unfold heatKernel_dx; aesop;
convert h_cont.continuousWithinAt.tendsto using 2 ; norm_num;
rw [ hasDerivAt_iff_tendsto_slope_zero ];
exact h_dominated_convergence.congr' ( by filter_upwards [ self_mem_nhdsWithin ] with h hh using by rw [ ← h_mean_value h hh ] ; norm_num [ div_eq_inv_mul ] )
/-
The second spatial derivative of heatSolution.
-/
set_option maxHeartbeats 800000 in
lemma heatSolution_hasDerivAt_xx (f : ℝ → ℝ) (hf_cont : Continuous f)
(hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) {t : ℝ} (ht : 0 < t) (x : ℝ) :
HasDerivAt (fun z => ∫ y, heatKernel_dx t (z - y) * f y)
(∫ y, heatKernel_dxx t (x - y) * f y) x := by
rw [ hasDerivAt_iff_tendsto_slope_zero ];
-- By Fubini's theorem, we can interchange the order of integration.
have h_fubini : ∀ h : ℝ, h ≠ 0 → ∫ y, (∫ u in (0 : ℝ)..1, heatKernel_dxx t (x + u * h - y) * f y) = ∫ u in (0 : ℝ)..1, ∫ y, heatKernel_dxx t (x + u * h - y) * f y := by
intro h hh; rw [ intervalIntegral.integral_of_le zero_le_one ] ; rw [ MeasureTheory.integral_integral_swap ] ;
· norm_num [ intervalIntegral.integral_of_le zero_le_one ];
· -- The function $heatKernel_dxx t (x + u * h - y) * f y$ is integrable because $heatKernel_dxx$ is bounded and $f$ is bounded.
have h_integrable : ∀ u ∈ Set.Icc (0 : ℝ) 1, Integrable (fun y => heatKernel_dxx t (x + u * h - y) * f y) volume := by
intro u hu
have h_integrable : Integrable (fun y => heatKernel_dxx t (x + u * h - y)) volume := by
have h_integrable : Integrable (fun y => heatKernel_dxx t y) volume := by
have h_integrable : Integrable (fun y => (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-(y ^ 2 / (4 * t))) * (y ^ 2 / (4 * t ^ 2) - 1 / (2 * t))) volume := by
have h_integrable : Integrable (fun y => Real.exp (-(y ^ 2 / (4 * t))) * y ^ 2) volume := by
have := @integrable_rpow_mul_exp_neg_mul_sq;
convert @this ( 1 / ( 4 * t ) ) ( by positivity ) 2 ( by norm_num ) using 1 ; norm_num ; ring;
ac_rfl;
have h_integrable : Integrable (fun y => Real.exp (-(y ^ 2 / (4 * t)))) volume := by
simpa [ div_eq_inv_mul ] using ( integrable_exp_neg_mul_sq ( by positivity ) );
convert ‹Integrable ( fun y => Real.exp ( - ( y ^ 2 / ( 4 * t ) ) ) * y ^ 2 ) volume›.const_mul ( ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ / ( 4 * t ^ 2 ) ) |> fun h => h.sub ( h_integrable.const_mul ( ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ / ( 2 * t ) ) ) using 2 ; ring;
norm_num ; ring;
convert h_integrable using 1;
ext y; unfold heatKernel_dxx; aesop;
exact h_integrable.comp_sub_left _;
refine' h_integrable.norm.mul_const _ |> fun h => h.mono' _ _;
exact hf_bdd.choose;
· exact h_integrable.1.mul ( hf_cont.aestronglyMeasurable );
· filter_upwards [ ] using fun y => by rw [ norm_mul ] ; exact mul_le_mul_of_nonneg_left ( hf_bdd.choose_spec y ) ( norm_nonneg _ ) ;
rw [ MeasureTheory.integrable_prod_iff ];
· have h_integrable : ∀ u ∈ Set.Icc (0 : ℝ) 1, ∫ y, ‖heatKernel_dxx t (x + u * h - y) * f y‖ ≤ (Real.sqrt (4 * Real.pi * t))⁻¹ * (1 / (2 * t)) * hf_bdd.choose * ∫ y, Real.exp (-( (x + u * h - y) ^ 2 / (4 * t) )) * (1 + (x + u * h - y) ^ 2 / (2 * t)) := by
intro u hu
have h_bound : ∀ y, ‖heatKernel_dxx t (x + u * h - y) * f y‖ ≤ (Real.sqrt (4 * Real.pi * t))⁻¹ * (1 / (2 * t)) * hf_bdd.choose * Real.exp (-( (x + u * h - y) ^ 2 / (4 * t) )) * (1 + (x + u * h - y) ^ 2 / (2 * t)) := by
intro y
have h_bound : ‖heatKernel_dxx t (x + u * h - y)‖ ≤ (Real.sqrt (4 * Real.pi * t))⁻¹ * (1 / (2 * t)) * Real.exp (-( (x + u * h - y) ^ 2 / (4 * t) )) * (1 + (x + u * h - y) ^ 2 / (2 * t)) := by
unfold heatKernel_dxx;
split_ifs <;> norm_num;
· grind;
· rw [ abs_of_nonneg ( Real.sqrt_nonneg _ ) ];
field_simp;
rw [ abs_div, abs_of_nonneg ( by positivity : ( 0 : ℝ ) ≤ 4 * t ^ 2 * 2 ) ];
rw [ mul_div, div_le_iff₀ ] <;> cases abs_cases ( ( x + u * h - y ) ^ 2 * 2 - 4 * t ) <;> nlinarith [ sq_nonneg ( x + u * h - y ), mul_pos ht ht ];
rw [ norm_mul ];
refine le_trans ( mul_le_mul_of_nonneg_right h_bound <| norm_nonneg _ ) ?_;
convert mul_le_mul_of_nonneg_left ( hf_bdd.choose_spec y ) ( show 0 ≤ ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ * ( 1 / ( 2 * t ) ) * Real.exp ( - ( ( x + u * h - y ) ^ 2 / ( 4 * t ) ) ) * ( 1 + ( x + u * h - y ) ^ 2 / ( 2 * t ) ) by positivity ) using 1 ; ring;
rw [ ← MeasureTheory.integral_const_mul ];
refine' MeasureTheory.integral_mono_of_nonneg _ _ _;
· exact Filter.Eventually.of_forall fun y => norm_nonneg _;
· have h_integrable : Integrable (fun y => Real.exp (-( (x + u * h - y) ^ 2 / (4 * t) )) * (1 + (x + u * h - y) ^ 2 / (2 * t))) volume := by
have h_integrable : Integrable (fun y => Real.exp (-(y ^ 2 / (4 * t))) * (1 + y ^ 2 / (2 * t))) volume := by
have h_gauss_integrable : Integrable (fun y => Real.exp (-(y ^ 2 / (4 * t))) * y ^ 2) volume := by
have := @integrable_rpow_mul_exp_neg_mul_sq;
convert @this ( 1 / ( 4 * t ) ) ( by positivity ) 2 ( by norm_num ) using 1 ; norm_num ; ring;
ac_rfl;
convert h_gauss_integrable.div_const ( 2 * t ) |> Integrable.add <| ( integrable_exp_neg_mul_sq ( show 0 < 1 / ( 4 * t ) by positivity ) ) using 2 ; ring;
norm_num ; ring;
convert h_integrable.comp_sub_left ( x + u * h ) using 1;
exact h_integrable.const_mul _;
· filter_upwards [ ] using fun y => by simpa only [ mul_assoc ] using h_bound y;
have h_integrable : ∀ u ∈ Set.Icc (0 : ℝ) 1, ∫ y, Real.exp (-( (x + u * h - y) ^ 2 / (4 * t) )) * (1 + (x + u * h - y) ^ 2 / (2 * t)) = Real.sqrt (4 * Real.pi * t) * (1 + 1 / (2 * t) * (2 * t)) := by
intro u hu
have h_gauss : ∫ y, Real.exp (-(y ^ 2 / (4 * t))) * (1 + y ^ 2 / (2 * t)) = Real.sqrt (4 * Real.pi * t) * (1 + 1 / (2 * t) * (2 * t)) := by
have h_gauss : ∫ y, Real.exp (-(y ^ 2 / (4 * t))) * y ^ 2 = Real.sqrt (4 * Real.pi * t) * (2 * t) := by
have := @integral_rpow_mul_exp_neg_mul_rpow;
have h_gauss : ∫ y in Set.Ioi 0, Real.exp (-(y ^ 2 / (4 * t))) * y ^ 2 = Real.sqrt (4 * Real.pi * t) * (2 * t) / 2 := by
convert @this 2 2 ( 1 / ( 4 * t ) ) ( by norm_num ) ( by norm_num ) ( by positivity ) using 1 <;> norm_num [ div_eq_inv_mul ];
· ac_rfl;
· rw [ show ( 3 / 2 : ℝ ) = 1 / 2 + 1 by norm_num, Real.Gamma_add_one ( by norm_num ), Real.rpow_neg_eq_inv_rpow ] ; ring ; norm_num [ ht.le ];
rw [ show ( t * 4 ) ^ ( 3 / 2 : ℝ ) = ( t * 4 ) * Real.sqrt ( t * 4 ) by rw [ Real.sqrt_eq_rpow, ← Real.rpow_one_add' ] <;> norm_num ; positivity ] ; norm_num [ Real.Gamma_one_half_eq, ht.le ] ; ring;
have h_gauss_symm : ∫ y in Set.Iic 0, Real.exp (-(y ^ 2 / (4 * t))) * y ^ 2 = Real.sqrt (4 * Real.pi * t) * (2 * t) / 2 := by
rw [ ← h_gauss, ← neg_zero, ← integral_comp_neg_Iic ] ; norm_num;
convert congr_arg₂ ( · + · ) h_gauss_symm h_gauss using 1;
· rw [ ← MeasureTheory.setIntegral_union ] <;> norm_num;
· exact ( by contrapose! h_gauss_symm; rw [ MeasureTheory.integral_undef h_gauss_symm ] ; positivity );
· exact ( by contrapose! h_gauss; rw [ MeasureTheory.integral_undef h_gauss ] ; positivity );
· ring;
have h_gauss : ∫ y, Real.exp (-(y ^ 2 / (4 * t))) = Real.sqrt (4 * Real.pi * t) := by
convert integral_gaussian ( 1 / ( 4 * t ) ) using 1 <;> norm_num [ div_eq_inv_mul ] ; ring;
have h_gauss : ∫ y, Real.exp (-(y ^ 2 / (4 * t))) * (1 + y ^ 2 / (2 * t)) = (∫ y, Real.exp (-(y ^ 2 / (4 * t)))) + (∫ y, Real.exp (-(y ^ 2 / (4 * t))) * y ^ 2 / (2 * t)) := by
rw [ ← MeasureTheory.integral_add ] ; congr ; ext y ; ring;
· exact ( by contrapose! h_gauss; rw [ MeasureTheory.integral_undef h_gauss ] ; positivity );
· exact MeasureTheory.Integrable.div_const ( by exact ( by contrapose! h_gauss; rw [ MeasureTheory.integral_undef h_gauss ] at *; nlinarith [ Real.sqrt_pos.mpr ( show 0 < 4 * Real.pi * t by positivity ) ] ) ) _;
simp_all +decide [ MeasureTheory.integral_div ];
grind;
rw [ ← h_gauss, eq_comm, ← MeasureTheory.integral_sub_left_eq_self ];
simp +zetaDelta at *;
refine' ⟨ Filter.eventually_inf_principal.mpr _, _ ⟩;
· exact Filter.Eventually.of_forall fun u hu => ‹∀ u : ℝ, 0 ≤ u → u ≤ 1 → Integrable ( fun y => heatKernel_dxx t ( x + u * h - y ) * f y ) volume› u hu.1.le hu.2;
· refine' MeasureTheory.Integrable.mono' _ _ _;
use fun u => ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ * ( t⁻¹ * 2⁻¹ ) * hf_bdd.choose * ( Real.sqrt ( 4 * Real.pi * t ) * ( 1 + t⁻¹ * 2⁻¹ * ( 2 * t ) ) );
· fun_prop;
· refine' MeasureTheory.StronglyMeasurable.aestronglyMeasurable _;
refine' MeasureTheory.StronglyMeasurable.integral_prod_right _;
refine' Measurable.stronglyMeasurable _;
refine' Measurable.mul _ _;
· refine' Measurable.abs _;
refine' Measurable.ite _ _ _ <;> norm_num;
fun_prop;
· exact hf_cont.abs.measurable.comp measurable_snd;
· filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Ioc ] with u hu using by rw [ Real.norm_of_nonneg ( MeasureTheory.integral_nonneg fun _ => by positivity ) ] ; exact le_trans ( by solve_by_elim [ hu.1.le, hu.2 ] ) ( by rw [ h_integrable u hu.1.le hu.2 ] ) ;
· refine' Measurable.aestronglyMeasurable _;
refine' Measurable.mul _ _;
· refine' Measurable.ite _ _ _ <;> norm_num;
fun_prop;
· exact hf_cont.measurable.comp measurable_snd;
-- By the properties of the heat kernel, we know that $\int_{-\infty}^{\infty} \text{heatKernel}_{xx}(t, x-y) f(y) \, dy$ is continuous in $x$.
have h_cont : Continuous (fun x => ∫ y, heatKernel_dxx t (x - y) * f y) := by
-- By the properties of the heat kernel, we know that $\int_{-\infty}^{\infty} \text{heatKernel}_{xx}(t, x-y) f(y) \, dy$ is continuous in $x$ because the heat kernel is continuous and the integral of a continuous function is continuous.
have h_cont : Continuous (fun x => ∫ y, heatKernel_dxx t y * f (x - y)) := by
refine' continuous_iff_continuousAt.mpr _;
intro x;
refine' MeasureTheory.tendsto_integral_filter_of_dominated_convergence _ _ _ _ _;
use fun y => |heatKernel_dxx t y| * hf_bdd.choose;
· refine' Filter.Eventually.of_forall fun n => MeasureTheory.AEStronglyMeasurable.mul _ _;
· refine' Measurable.aestronglyMeasurable _;
refine' Measurable.ite _ _ _ <;> norm_num;
fun_prop;
· exact Continuous.aestronglyMeasurable ( hf_cont.comp ( continuous_const.sub continuous_id' ) );
· filter_upwards [ ] using fun n => Filter.Eventually.of_forall fun a => by simpa [ abs_mul ] using mul_le_mul_of_nonneg_left ( hf_bdd.choose_spec ( n - a ) ) ( abs_nonneg _ ) ;
· refine' MeasureTheory.Integrable.mul_const _ _;
refine' MeasureTheory.Integrable.abs _;
-- The second derivative of the heat kernel is integrable because it is a product of a Gaussian function and a polynomial function, both of which are integrable.
have h_integrable : Integrable (fun x => Real.exp (-x^2 / (4 * t)) * (x^2 / (4 * t^2) - 1 / (2 * t))) volume := by
have h_integrable : Integrable (fun x => Real.exp (-x^2 / (4 * t)) * x^2) volume := by
have := @integrable_rpow_mul_exp_neg_mul_sq;
convert @this ( 1 / ( 4 * t ) ) ( by positivity ) 2 ( by norm_num ) using 1 ; norm_num ; ring;
ac_rfl;
convert h_integrable.div_const ( 4 * t ^ 2 ) |> fun h => h.sub ( MeasureTheory.Integrable.const_mul ( show MeasureTheory.Integrable ( fun x => Real.exp ( -x ^ 2 / ( 4 * t ) ) ) volume from by simpa [ div_eq_inv_mul ] using ( integrable_exp_neg_mul_sq ( by positivity ) ) ) ( 1 / ( 2 * t ) ) ) using 2 ; ring;
norm_num ; ring;
convert h_integrable.const_mul ( ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ ) using 2 ; unfold heatKernel_dxx ; ring;
grind;
· exact Filter.Eventually.of_forall fun y => Filter.Tendsto.mul tendsto_const_nhds ( hf_cont.continuousAt.tendsto.comp ( Filter.tendsto_id.sub tendsto_const_nhds ) );
convert h_cont using 1;
ext x;
rw [ ← MeasureTheory.integral_sub_left_eq_self ];
swap;
exacts [ x, by congr; ext y; ring ];
-- By the properties of the heat kernel, we know that $\int_{-\infty}^{\infty} \text{heatKernel}_{xx}(t, x-y) f(y) \, dy$ is continuous in $x$, and thus the limit can be passed inside the integral.
have h_limit : Filter.Tendsto (fun h => ∫ u in (0 : ℝ)..1, ∫ y, heatKernel_dxx t (x + u * h - y) * f y) (nhdsWithin 0 {0}ᶜ) (nhds (∫ u in (0 : ℝ)..1, ∫ y, heatKernel_dxx t (x - y) * f y)) := by
refine' tendsto_nhdsWithin_of_tendsto_nhds _;
refine' intervalIntegral.tendsto_integral_filter_of_dominated_convergence _ _ _ _ _;
use fun u => SupSet.sSup ( Set.image ( fun x => |∫ y, heatKernel_dxx t ( x - y ) * f y| ) ( Set.Icc ( x - 1 ) ( x + 1 ) ) );
· exact Filter.Eventually.of_forall fun n => Continuous.aestronglyMeasurable ( by exact h_cont.comp ( by continuity ) );
· rw [ Metric.eventually_nhds_iff ];
refine' ⟨ 1, by norm_num, fun y hy => Filter.Eventually.of_forall fun z hz => _ ⟩;
refine' le_csSup _ _;
· exact IsCompact.bddAbove ( isCompact_Icc.image ( h_cont.abs ) );
· exact ⟨ x + z * y, ⟨ by cases Set.mem_uIoc.mp hz <;> nlinarith [ abs_lt.mp hy ], by cases Set.mem_uIoc.mp hz <;> nlinarith [ abs_lt.mp hy ] ⟩, rfl ⟩;
· norm_num;
· exact Filter.Eventually.of_forall fun u hu => by simpa using h_cont.continuousAt.tendsto.comp ( Continuous.tendsto' ( by continuity ) _ _ <| by norm_num ) ;
have h_limit : Filter.Tendsto (fun h => ∫ y, (∫ u in (0 : ℝ)..1, heatKernel_dxx t (x + u * h - y) * f y)) (nhdsWithin 0 {0}ᶜ) (nhds (∫ y, heatKernel_dxx t (x - y) * f y)) := by
exact Filter.Tendsto.congr' ( Filter.eventuallyEq_of_mem self_mem_nhdsWithin fun h hh => by rw [ h_fubini h hh ] ) ( h_limit.trans ( by norm_num ) );
refine' h_limit.congr' _;
filter_upwards [ self_mem_nhdsWithin ] with h hh;
rw [ ← MeasureTheory.integral_sub ];
· rw [ ← MeasureTheory.integral_smul ];
refine' MeasureTheory.integral_congr_ae _;
filter_upwards [ ] with y;
rw [ intervalIntegral.integral_eq_sub_of_hasDerivAt ];
rotate_right;
use fun u => h⁻¹ * ( heatKernel_dx t ( x + u * h - y ) * f y );
· norm_num ; ring;
· intro u hu; convert HasDerivAt.const_mul ( h⁻¹ ) ( HasDerivAt.mul ( HasDerivAt.comp u ( heatKernel_hasDerivAt_xx ht _ ) ( HasDerivAt.sub ( HasDerivAt.add ( hasDerivAt_const _ _ ) ( hasDerivAt_mul_const _ ) ) ( hasDerivAt_const _ _ ) ) ) ( hasDerivAt_const _ _ ) ) using 1 ; ring;
simp +decide [ mul_assoc, mul_comm h, hh ] ; ring;
exact eq_div_of_mul_eq ( by aesop ) ( by ring );
· apply_rules [ Continuous.intervalIntegrable ];
refine' Continuous.mul _ continuous_const;
refine' Continuous.if _ _ _;
· grind +suggestions;
· exact continuous_const;
· fun_prop;
· have h_integrable : Integrable (fun y => heatKernel_dx t y * f (x + h - y)) volume := by
have h_integrable : Integrable (fun y => heatKernel_dx t y) volume := by
have h_integrable : Integrable (fun y => (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-(y ^ 2 / (4 * t))) * (-(y / (2 * t)))) volume := by
have h_integrable : Integrable (fun y => y * Real.exp (-(y ^ 2 / (4 * t)))) volume := by
have := @integrable_rpow_mul_exp_neg_mul_sq;
convert @this ( 1 / ( 4 * t ) ) ( by positivity ) 1 ( by norm_num ) using 3 ; norm_num ; ring;
convert h_integrable.const_mul ( - ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ / ( 2 * t ) ) using 2 ; ring;
convert h_integrable using 1;
ext y; simp [heatKernel_dx, heatKernel];
grind +splitImp;
refine' h_integrable.norm.mul_const _ |> fun h => h.mono' _ _;
exact hf_bdd.choose;
· exact h_integrable.1.mul ( hf_cont.comp ( continuous_const.sub continuous_id' ) |> Continuous.aestronglyMeasurable );
· filter_upwards [ ] using fun y => by rw [ norm_mul ] ; exact mul_le_mul_of_nonneg_left ( hf_bdd.choose_spec _ ) ( norm_nonneg _ ) ;
convert h_integrable.comp_sub_left ( x + h ) using 1 ; ext ; simp +decide [ mul_comm ];
· have h_integrable : Integrable (fun y => heatKernel_dx t (x - y)) volume := by
have h_integrable : Integrable (fun y => heatKernel_dx t y) volume := by
have h_integrable : Integrable (fun y => (Real.sqrt (4 * Real.pi * t))⁻¹ * Real.exp (-(y ^ 2 / (4 * t))) * (-(y / (2 * t)))) volume := by
have h_integrable : Integrable (fun y => y * Real.exp (-(y ^ 2 / (4 * t)))) volume := by
have := @integrable_rpow_mul_exp_neg_mul_sq;
convert @this ( 1 / ( 4 * t ) ) ( by positivity ) 1 ( by norm_num ) using 3 ; norm_num ; ring;
convert h_integrable.const_mul ( - ( Real.sqrt ( 4 * Real.pi * t ) ) ⁻¹ / ( 2 * t ) ) using 2 ; ring;
convert h_integrable using 1;
ext y; simp [heatKernel_dx, heatKernel];
grind +splitImp;
exact h_integrable.comp_sub_left x;
refine' h_integrable.norm.mul_const _ |> fun h => h.mono' _ _;
exact hf_bdd.choose;
· exact h_integrable.1.mul ( hf_cont.aestronglyMeasurable );
· filter_upwards [ ] using fun y => by rw [ norm_mul ] ; exact mul_le_mul_of_nonneg_left ( hf_bdd.choose_spec y ) ( norm_nonneg _ ) ;
/-
The time derivative of the heat kernel equals the second spatial derivative.
-/
lemma heatKernel_pde {t : ℝ} (ht : 0 < t) (x : ℝ) :
HasDerivAt (fun s => heatKernel s x) (heatKernel_dxx t x) t := by
convert HasDerivAt.congr_of_eventuallyEq _ ?_ using 1;
exact fun s => ( Real.sqrt ( 4 * Real.pi * s ) ) ⁻¹ * Real.exp ( - ( x ^ 2 / ( 4 * s ) ) );
· convert HasDerivAt.mul ( HasDerivAt.inv ( HasDerivAt.sqrt ( HasDerivAt.const_mul ( 4 * Real.pi ) ( hasDerivAt_id' t ) ) ( by positivity ) ) ( by positivity ) ) ( HasDerivAt.exp ( HasDerivAt.neg ( HasDerivAt.div ( hasDerivAt_const _ _ ) ( HasDerivAt.const_mul 4 ( hasDerivAt_id' t ) ) ( by positivity ) ) ) ) using 1 ; norm_num [ ht.ne', Real.pi_pos.ne', heatKernel_dxx ] ; ring;
grind;
· filter_upwards [ lt_mem_nhds ht ] with s hs using heatKernel_of_pos hs x
/-
The time derivative of heatSolution: differentiate under the integral.
-/
set_option maxHeartbeats 800000 in
lemma heatSolution_hasDerivAt_t (f : ℝ → ℝ) (hf_cont : Continuous f)
(hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) {t : ℝ} (ht : 0 < t) (x : ℝ) :
HasDerivAt (fun s => heatSolution f s x)
(∫ y, heatKernel_dxx t (x - y) * f y) t := by
obtain ⟨ M, hM ⟩ := hf_bdd;
-- Apply the dominated convergence theorem to interchange the derivative and the integral.
have h_dominated : Filter.Tendsto (fun h => ∫ y, (heatKernel (t + h) (x - y) - heatKernel t (x - y)) / h * f y) (nhdsWithin 0 {0}ᶜ) (nhds (∫ y, heatKernel_dxx t (x - y) * f y)) := by
-- To apply the dominated convergence theorem, we need to show that the integrand is dominated by an integrable function.
have h_dominate : ∀ h, abs h < t / 2 → ∀ y, abs ((heatKernel (t + h) (x - y) - heatKernel t (x - y)) / h * f y) ≤ M * (Real.sqrt (4 * Real.pi * (t / 2)))⁻¹ * Real.exp (-(x - y) ^ 2 / (8 * t)) * (1 / (t / 2) + (x - y) ^ 2 / (t / 2) ^ 2) := by
-- By the properties of the heat kernel, we know that its derivative is bounded.
have h_deriv_bound : ∀ h, abs h < t / 2 → ∀ y, abs (deriv (fun s => heatKernel s (x - y)) (t + h)) ≤ (Real.sqrt (4 * Real.pi * (t / 2)))⁻¹ * Real.exp (-(x - y) ^ 2 / (8 * t)) * (1 / (t / 2) + (x - y) ^ 2 / (t / 2) ^ 2) := by
intros h hh y
have h_deriv_bound : deriv (fun s => heatKernel s (x - y)) (t + h) = heatKernel_dxx (t + h) (x - y) := by
exact HasDerivAt.deriv ( heatKernel_pde ( by linarith [ abs_lt.mp hh ] ) _ );
rw [ h_deriv_bound, heatKernel_dxx ];
split_ifs <;> norm_num;
· exact mul_nonneg ( mul_nonneg ( inv_nonneg.2 ( Real.sqrt_nonneg _ ) ) ( Real.exp_nonneg _ ) ) ( add_nonneg ( div_nonneg zero_le_two ht.le ) ( div_nonneg ( sq_nonneg _ ) ( sq_nonneg _ ) ) );
· gcongr;
· rw [ abs_of_nonneg ( Real.sqrt_nonneg _ ) ] ; exact Real.sqrt_le_sqrt <| by nlinarith [ Real.pi_pos, abs_lt.mp hh ] ;
· rw [ neg_div, neg_le_neg_iff ];
rw [ div_le_div_iff₀ ] <;> nlinarith [ abs_lt.mp hh ];
· rw [ abs_le ];
field_simp;
rw [ le_div_iff₀, div_le_iff₀ ] <;> try nlinarith;
constructor <;> nlinarith [ sq_nonneg ( t + h - t / 2 ), sq_nonneg ( t + h + t / 2 ), abs_lt.mp hh, mul_le_mul_of_nonneg_left ( show t + h ≥ t / 2 by linarith [ abs_lt.mp hh ] ) ( sq_nonneg ( x - y ) ) ];
-- By the mean value theorem, there exists some $c$ between $t$ and $t + h$ such that
have h_mean_value : ∀ h, abs h < t / 2 → ∀ y, h ≠ 0 → ∃ c ∈ Set.Icc (t - abs h) (t + abs h), (heatKernel (t + h) (x - y) - heatKernel t (x - y)) / h = deriv (fun s => heatKernel s (x - y)) c := by
intro h hh y hy; cases' lt_or_gt_of_ne hy with hy hy <;> simp_all +decide [ div_eq_inv_mul ] ;
· have := exists_deriv_eq_slope ( f := fun s => heatKernel s ( x - y ) ) ( show t + h < t by linarith );
contrapose! this;
refine' ⟨ _, _, _ ⟩;
· refine' ContinuousOn.congr _ _;
use fun s => ( Real.sqrt ( 4 * Real.pi * s ) ) ⁻¹ * Real.exp ( - ( ( x - y ) ^ 2 / ( 4 * s ) ) );
· exact continuousOn_of_forall_continuousAt fun s hs => ContinuousAt.mul ( ContinuousAt.inv₀ ( Real.continuous_sqrt.continuousAt.comp <| ContinuousAt.mul continuousAt_const continuousAt_id ) <| ne_of_gt <| Real.sqrt_pos.mpr <| mul_pos ( by positivity ) <| by linarith [ hs.1, abs_lt.mp hh ] ) <| Real.continuous_exp.continuousAt.comp <| ContinuousAt.neg <| ContinuousAt.div continuousAt_const ( continuousAt_const.mul continuousAt_id ) <| by linarith [ hs.1, abs_lt.mp hh ] ;
· intro s hs; simp +decide [ heatKernel, hs.1, hs.2 ] ;
exact fun hs' => Real.sqrt_eq_zero_of_nonpos <| mul_nonpos_of_nonneg_of_nonpos ( by positivity ) hs';
· refine' fun s hs => DifferentiableAt.differentiableWithinAt _;
refine' DifferentiableAt.congr_of_eventuallyEq _ _;
use fun s => ( Real.sqrt ( 4 * Real.pi * s ) ) ⁻¹ * Real.exp ( - ( ( x - y ) ^ 2 / ( 4 * s ) ) );
· exact DifferentiableAt.mul ( DifferentiableAt.inv ( DifferentiableAt.sqrt ( differentiableAt_id.const_mul _ ) ( by nlinarith [ Real.pi_pos, hs.1, hs.2, abs_lt.mp hh ] ) ) ( ne_of_gt ( Real.sqrt_pos.mpr ( by nlinarith [ Real.pi_pos, hs.1, hs.2, abs_lt.mp hh ] ) ) ) ) ( DifferentiableAt.exp ( DifferentiableAt.neg ( DifferentiableAt.div ( differentiableAt_const _ ) ( differentiableAt_id.const_mul _ ) ( by nlinarith [ Real.pi_pos, hs.1, hs.2, abs_lt.mp hh ] ) ) ) );
· filter_upwards [ Ioo_mem_nhds hs.1 hs.2 ] with u hu using if_neg ( by linarith [ hu.1, hu.2, abs_lt.mp hh ] );
· intro c hc; specialize this c ⟨ by cases abs_cases h <;> linarith [ hc.1, hc.2 ], by cases abs_cases h <;> linarith [ hc.1, hc.2 ] ⟩ ; ring_nf at *; aesop;
· have := exists_deriv_eq_slope ( f := fun s => heatKernel s ( x - y ) ) ( show t < t + h by linarith );
simp +zetaDelta at *;
refine' this _ _ |> fun ⟨ c, hc₁, hc₂ ⟩ => ⟨ c, ⟨ by linarith [ abs_of_pos hy ], by linarith [ abs_of_pos hy ] ⟩, by rw [ hc₂, inv_mul_eq_div ] ⟩;
· refine' ContinuousOn.congr _ _;
use fun s => ( Real.sqrt ( 4 * Real.pi * s ) ) ⁻¹ * Real.exp ( - ( ( x - y ) ^ 2 / ( 4 * s ) ) );
· exact continuousOn_of_forall_continuousAt fun s hs => ContinuousAt.mul ( ContinuousAt.inv₀ ( Real.continuous_sqrt.continuousAt.comp <| ContinuousAt.mul continuousAt_const continuousAt_id ) <| ne_of_gt <| Real.sqrt_pos.mpr <| mul_pos ( by positivity ) <| by linarith [ hs.1 ] ) <| Real.continuous_exp.continuousAt.comp <| ContinuousAt.neg <| ContinuousAt.div continuousAt_const ( continuousAt_const.mul continuousAt_id ) <| by linarith [ hs.1 ] ;
· intro s hs; simp +decide [ heatKernel, hs.1.trans' ht.le ] ;
exact fun h => Or.inl <| by linarith [ hs.1 ] ;
· refine' DifferentiableOn.congr _ _;
use fun s => ( Real.sqrt ( 4 * Real.pi * s ) ) ⁻¹ * Real.exp ( - ( ( x - y ) ^ 2 / ( 4 * s ) ) );
· exact DifferentiableOn.mul ( DifferentiableOn.inv ( DifferentiableOn.sqrt ( differentiableOn_id.const_mul _ ) fun s hs => by nlinarith [ Real.pi_pos, hs.1 ] ) fun s hs => ne_of_gt <| Real.sqrt_pos.mpr <| by nlinarith [ Real.pi_pos, hs.1 ] ) ( DifferentiableOn.exp <| DifferentiableOn.neg <| DifferentiableOn.div ( differentiableOn_const _ ) ( differentiableOn_id.const_mul _ ) fun s hs => by nlinarith [ Real.pi_pos, hs.1 ] );
· exact fun s hs => if_neg ( by linarith [ hs.1 ] );
intro h hh y; by_cases hh' : h = 0 <;> simp_all +decide [ abs_mul, mul_assoc, mul_comm, mul_left_comm ] ;
· exact mul_nonneg ( le_trans ( abs_nonneg _ ) ( hM x ) ) ( mul_nonneg ( by positivity ) ( by positivity ) );
· obtain ⟨ c, hc₁, hc₂ ⟩ := h_mean_value h hh y hh'; rw [ hc₂ ] ;
gcongr;
· exact le_trans ( abs_nonneg _ ) ( hM 0 );
· exact hM y;
· convert h_deriv_bound ( c - t ) ( abs_lt.mpr ⟨ by linarith [ abs_nonneg h ], by linarith [ abs_nonneg h ] ⟩ ) y using 1 ; ring;
-- The dominating function is integrable.
have h_integrable : MeasureTheory.Integrable (fun y => M * (Real.sqrt (4 * Real.pi * (t / 2)))⁻¹ * Real.exp (-(x - y) ^ 2 / (8 * t)) * (1 / (t / 2) + (x - y) ^ 2 / (t / 2) ^ 2)) MeasureTheory.volume := by
have h_integrable : MeasureTheory.Integrable (fun y => Real.exp (-(x - y) ^ 2 / (8 * t)) * (1 / (t / 2) + (x - y) ^ 2 / (t / 2) ^ 2)) MeasureTheory.volume := by
have h_integrable : MeasureTheory.Integrable (fun y => Real.exp (-y ^ 2 / (8 * t)) * (1 / (t / 2) + y ^ 2 / (t / 2) ^ 2)) MeasureTheory.volume := by
have h_integrable : MeasureTheory.Integrable (fun y => Real.exp (-y ^ 2 / (8 * t)) * y ^ 2) MeasureTheory.volume := by
have := @integrable_rpow_mul_exp_neg_mul_sq;
convert @this ( 1 / ( 8 * t ) ) ( by positivity ) 2 ( by norm_num ) using 1 ; norm_num ; ring;
ac_rfl;
convert h_integrable.div_const ( t ^ 2 / 4 ) |> MeasureTheory.Integrable.add <| MeasureTheory.Integrable.const_mul ( show MeasureTheory.Integrable ( fun y => Real.exp ( -y ^ 2 / ( 8 * t ) ) ) volume from ?_ ) ( 2 / t ) using 2 ; ring;
· norm_num ; ring;
· simpa [ div_eq_inv_mul ] using ( integrable_exp_neg_mul_sq ( by positivity ) );
convert h_integrable.comp_sub_left x using 1;
convert h_integrable.const_mul ( M * ( Real.sqrt ( 4 * Real.pi * ( t / 2 ) ) ) ⁻¹ ) using 2 ; ring;
refine' MeasureTheory.tendsto_integral_filter_of_dominated_convergence _ _ _ _ _;
use fun y => M * ( Real.sqrt ( 4 * Real.pi * ( t / 2 ) ) ) ⁻¹ * Real.exp ( - ( x - y ) ^ 2 / ( 8 * t ) ) * ( 1 / ( t / 2 ) + ( x - y ) ^ 2 / ( t / 2 ) ^ 2 );
· refine' Filter.eventually_of_mem self_mem_nhdsWithin fun n hn => Measurable.aestronglyMeasurable _;
unfold heatKernel;
split_ifs <;> fun_prop;
· filter_upwards [ self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds ( Metric.ball_mem_nhds _ <| half_pos ht ) ] with n hn hn' using Filter.Eventually.of_forall fun y => h_dominate n ( by simpa using hn' ) y;
· exact h_integrable;
· refine' Filter.Eventually.of_forall fun y => _;
have h_deriv : HasDerivAt (fun s => heatKernel s (x - y)) (heatKernel_dxx t (x - y)) t := by
exact?;
simpa [ div_eq_inv_mul ] using h_deriv.tendsto_slope_zero.mul_const ( f y );
rw [ hasDerivAt_iff_tendsto_slope_zero ];
refine' h_dominated.congr' _;
filter_upwards [ self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds ( Metric.ball_mem_nhds _ ht ) ] with h hh hh' ; simp_all +decide [ div_eq_inv_mul, MeasureTheory.integral_const_mul, MeasureTheory.integral_sub, heatSolution ];
rw [ ← MeasureTheory.integral_sub ];
· rw [ ← MeasureTheory.integral_const_mul ] ; congr ; ext ; ring;
· refine' MeasureTheory.Integrable.mono' _ _ _;
refine' fun y => M * heatKernel ( t + h ) ( x - y );
· refine' MeasureTheory.Integrable.const_mul _ _;
exact MeasureTheory.Integrable.comp_sub_left ( heatKernel_integrable ( show 0 < t + h by linarith [ abs_lt.mp hh' ] ) ) x;
· exact Continuous.aestronglyMeasurable ( by unfold heatKernel; split_ifs <;> continuity );
· filter_upwards [ ] with y using by rw [ Real.norm_eq_abs, abs_mul, abs_of_nonneg ( show 0 ≤ heatKernel ( t + h ) ( x - y ) from by unfold heatKernel; split_ifs <;> positivity ) ] ; nlinarith [ hM y, show 0 ≤ heatKernel ( t + h ) ( x - y ) from by unfold heatKernel; split_ifs <;> positivity ] ;
· apply_rules [ heatSolution_integrable ];
use M
-- ============================================================================
-- Main theorem
-- ============================================================================
theorem 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))) := by
constructor
· -- PDE part
intro t ht x
refine ⟨fun z => ∫ y, heatKernel_dx t (z - y) * f y,
∫ y, heatKernel_dxx t (x - y) * f y, ?_, ?_, ?_⟩
· intro y
exact heatSolution_hasDerivAt_x f hf_cont hf_bdd ht y
· exact heatSolution_hasDerivAt_xx f hf_cont hf_bdd ht x
· exact heatSolution_hasDerivAt_t f hf_cont hf_bdd ht x
· -- Initial condition
exact heatSolution_initial f hf_cont hf_bdd
end
end Submission
Raw
WorkspaceTest.lean
import Lean
open Lean
def comparatorExists (comparatorBin : String) : IO Bool := do
if comparatorBin.contains '/' then
return (← System.FilePath.pathExists comparatorBin)
try
let child ← IO.Process.spawn {
cmd := "sh"
args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin]
}
let exitCode ← child.wait
return exitCode == 0
catch _ =>
return false
def main : IO UInt32 := do
let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
if !(← comparatorExists comparatorBin) then
IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
pure 1
else
try
let child ← IO.Process.spawn {
cmd := "lake"
args := #["env", comparatorBin, "config.json"]
}
let exitCode ← child.wait
pure exitCode
catch err =>
IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
IO.eprintln s!"Original error: {err}"
pure 1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment