Plain-language statement
Swap the spatial derivative with the integral .
Exact Lean statement
lemma swap_x_heatKernel
{α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α)
(hg : Integrable g) :
HasDerivAt
(fun x' => ∫ y, heatKernel α (x' - y) t * g y ∂volume)
(∫ y, HKx α (x - y) t * g y ∂volume) xFormal artifact
Lean source
lemma swap_x_heatKernel {α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : Integrable g) : HasDerivAt (fun x' => ∫ y, heatKernel α (x' - y) t * g y ∂volume) (∫ y, HKx α (x - y) t * g y ∂volume) x := by have t_pos: t/2 > 0 := by positivity have mem_nhds : Metric.ball x 1 ∈ 𝓝 x := Metric.ball_mem_nhds x (by norm_num) have meas_HK_mul : ∀ᶠ x' in 𝓝 x, AEStronglyMeasurable (fun y : ℝ => heatKernel α (x' - y) t * g y) volume := by filter_upwards [mem_nhds] with τ hτ exact aestronglyMeasurable_heatKernel_mul hα ht g hg have integ_HK_mul : Integrable (fun y : ℝ => heatKernel α (x - y) t * g y) := integrable_heatKernel_mul_of_L1 g hα ht hg have integ_HKx_mul : Integrable (fun y : ℝ => HKx α (x - y) t * g y) := by simpa using integ_HKx_mul_of_L1 g hα ht hg have meas_HKx_mul: AEStronglyMeasurable (fun y : ℝ => HKx α (x - y) t * g y) volume := aestronglyMeasurable_HKx_mul g hg hα ht have diff_HK_mul' : ∀ᵐ y ∂volume, ∀ x' ∈ Metric.ball x 1, HasDerivAt (fun x'' => heatKernel α (x'' - y) t * g y) (HKx α (x' - y) t * g y) x' := by filter_upwards [diff_HKx_mul (α := α) (t := t) (x := x) g ht hα] with y hy intro x' hx' have h := hy x' hx' exact h have dominate_fun : ∀ᵐ y ∂volume, ∀ x' ∈ Metric.ball x 1, |HKx α (x' - y) t * g y| ≤ 1 / (2 * Real.sqrt Real.pi * α * t) * |g y| := by filter_upwards with y intro x' hx' calc |HKx α (x' - y) t * g y| ≤ |HKx α (x' - y) t| * |g y| := by rw [abs_mul] _ ≤ Kx α t * |g y| := by gcongr exact pointwise_bound_HKx ht hα _ = 1 / (2 * Real.sqrt Real.pi * α * t) * |g y| := by dsimp [Kx] have Integ_dominate_fun : Integrable (fun y : ℝ => (1 / (2 * Real.sqrt Real.pi * α * t)) * |g y|) := (hg.abs.const_mul (1 / (2 * Real.sqrt Real.pi * α * t))) have result := hasDerivAt_integral_of_dominated_loc_of_deriv_le mem_nhds meas_HK_mul integ_HK_mul meas_HKx_mul dominate_fun Integ_dominate_fun diff_HK_mul' exact result.2- Project
- PDE
- License
- Apache-2.0
- Commit
- 0ab5d79a0d7a
- Source
- PDE/Basics/Heat/HeatSolution.lean:666-727
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
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.
Source project: PDE
Person-level attribution pending.
Heat from convolution heat Kernel
heat_from_convolution_heatKernel
Project documentation
Swap the second spatial derivative with the integral . -/ 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...
Source project: PDE
Person-level attribution pending.
Deriv exp heat Kernel
Heat.deriv_exp_heatKernel
Plain-language statement
Derivative of the exponential term exp(-(x²)/(4αt)) with respect to x.
Source project: PDE
Person-level attribution pending.