Project-declaredLean 4.30.0 · mathlib@c5ea00351c28

Has Deriv At heat Kernel x x

Heat.hasDerivAt_heatKernel_x_x

partial differential equations Sobolev spaces analysis heat kernel

Project documentation

Auxiliary lemma: derivative of the first spatial derivative's formula.

Exact Lean statement

lemma hasDerivAt_heatKernel_x_x {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) :
    HasDerivAt
      (fun x' => (1 / Real.sqrt (4 * Real.pi * α * t)) *
                 (-(1 / (4 * α * t)) * (2 * x')) *
                 Real.exp (-(x'^2) / (4 * α * t)))
      ((1 / Real.sqrt (4 * Real.pi * α * t)) *
        ((-(1 / (4 * α * t)) * 2) * Real.exp (-(x^2) / (4 * α * t))
         + (-(1 / (4 * α * t)) * (2 * x)) * (-(1 / (4 * α * t)) * (2 * x)) *
           Real.exp (-(x^2) / (4 * α * t)))) x

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasDerivAt_heatKernel_x_x {α t x : ℝ} (ht : 0 < t) (hα : 0 < α) :    HasDerivAt      (fun x' => (1 / Real.sqrt (4 * Real.pi * α * t)) *                 (-(1 / (4 * α * t)) * (2 * x')) *                 Real.exp (-(x'^2) / (4 * α * t)))      ((1 / Real.sqrt (4 * Real.pi * α * t)) *        ((-(1 / (4 * α * t)) * 2) * Real.exp (-(x^2) / (4 * α * t))         + (-(1 / (4 * α * t)) * (2 * x)) * (-(1 / (4 * α * t)) * (2 * x)) *           Real.exp (-(x^2) / (4 * α * t)))) x := by  have h1 : HasDerivAt (fun x' => (-(1 / (4 * α * t))) * (2 * x'))                        (-(1 / (4 * α * t)) * 2) x := by    simpa using ((hasDerivAt_id x).const_mul 2).const_mul (-(1 / (4 * α * t)))   -- Apply product rule: f(x') * h(x') where f is linear and h is exponential  have hprod : HasDerivAt      (fun x' => ((-(1 / (4 * α * t))) * (2 * x')) * Real.exp (-(x'^2) / (4 * α * t)))      ((-(1 / (4 * α * t)) * 2) * Real.exp (-(x^2) / (4 * α * t))       + ((-(1 / (4 * α * t)) * (2 * x)) *          ((-(1 / (4 * α * t)) * (2 * x)) * Real.exp (-(x^2) / (4 * α * t))))) x :=    h1.mul (deriv_exp_heatKernel ht hα (x := x))   -- Simplify the second term  have hprod' : HasDerivAt      (fun x' => (-(1 / (4 * α * t)) * (2 * x')) * Real.exp (-(x'^2) / (4 * α * t)))      ((-(1 / (4 * α * t)) * 2) * Real.exp (-(x^2) / (4 * α * t))       + (-(1 / (4 * α * t)) * (2 * x)) * (-(1 / (4 * α * t)) * (2 * x)) *         Real.exp (-(x^2) / (4 * α * t))) x := by    simpa [mul_assoc] using hprod   simpa [mul_assoc] using hprod'.const_mul (1 / Real.sqrt (4 * Real.pi * α * t))

Project: PDE
License: Apache-2.0
Commit: 0ab5d79a0d7a
Source: PDE/Basics/Heat/HeatKernel.lean:201-230

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.30.0

Fderiv Ccinfty

FderivCcinfty

Plain-language statement

The Fréchet derivative x ↦ (∂ˢψ(x))(unitSeq s) of a test function ψ ∈ Cc^∞(U) again lies in Cc^∞(U). This is used to compose the weak derivative definition with itself.

partial differential equationsSobolev spacesanalysis

Source project: PDE

Person-level attribution pending.

View proof record

Project-declaredLean 4.30.0

Heat from convolution heat Kernel

heat_from_convolution_heatKernel

Project documentation

Swap the second spatial derivative $\partial_{xx}$ with the integral $\int$ . -/ lemma swap_xx_heatKernel {α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : Integrable g) : HasDerivAt (fun x' => ∫ y, HKx α (x' - y) t * g y ∂volume) (∫ y, HKxx α (x - y) t * g y ∂volume) x := by have mem_nhds : Metric.ball x 1 ∈ 𝓝 x := Metric.ball_mem_nhds x (by...

partial differential equationsSobolev spacesanalysis

Source project: PDE

Person-level attribution pending.

View proof record

Project-declaredLean 4.30.0

Deriv exp heat Kernel

Heat.deriv_exp_heatKernel

Plain-language statement

Derivative of the exponential term exp(-(x²)/(4αt)) with respect to x.

partial differential equationsSobolev spacesanalysis

Source project: PDE

Person-level attribution pending.

View proof record