Gaussian tail bound by weighted
Heat.gaussian_tail_bound_by_weighted
Plain-language statement
Key Gaussian tail bound: This is the analytical estimate that allows us to bound Gaussian tail integrals and prove convergence as t → 0.
Exact Lean statement
lemma gaussian_tail_bound_by_weighted {R : ℝ} (hR : 0 < R) :
∫ z in Set.Ici R, Real.exp (-z^2) ≤ (1 / R) * ∫ z in Set.Ici 0, z * Real.exp (-z^2)Formal artifact
Lean source
lemma gaussian_tail_bound_by_weighted {R : ℝ} (hR : 0 < R) : ∫ z in Set.Ici R, Real.exp (-z^2) ≤ (1 / R) * ∫ z in Set.Ici 0, z * Real.exp (-z^2) := by have h_gauss_int : Integrable (fun z => Real.exp (-z^2)) := by have := integrable_exp_neg_mul_sq (by norm_num : (0:ℝ) < 1) convert this using 1 ext z; ring_nf have h_weighted_gauss_int : IntegrableOn (fun z => z * Real.exp (-z^2)) (Set.Ici 0) := by have h_full : Integrable (fun z : ℝ => z * Real.exp (-z^2)) := by have := integrable_mul_exp_neg_mul_sq (by norm_num : (0:ℝ) < 1) convert this using 1 ext z ring_nf exact h_full.integrableOn have h_extend : ∫ z in Set.Ici R, z * Real.exp (-z^2) ≤ ∫ z in Set.Ici 0, z * Real.exp (-z^2) := by apply setIntegral_mono_set h_weighted_gauss_int · filter_upwards [self_mem_ae_restrict (measurableSet_Ici : MeasurableSet (Set.Ici (0:ℝ)))] with z hz exact mul_nonneg hz (by positivity) · exact Eventually.of_forall (Set.Ici_subset_Ici.mpr (le_of_lt hR)) have h_main : ∫ z in Set.Ici R, Real.exp (-z^2) ≤ (1 / R) * ∫ z in Set.Ici R, z * Real.exp (-z^2) := by have h_pointwise : ∀ z ∈ Set.Ici R, Real.exp (-z^2) ≤ (1 / R) * (z * Real.exp (-z^2)) := by intro z hz simp only [Set.mem_Ici] at hz have h_div : 1 ≤ z / R := by rw [le_div_iff₀ hR]; linarith calc Real.exp (-z^2) = 1 * Real.exp (-z^2) := by ring _ ≤ (z / R) * Real.exp (-z^2) := mul_le_mul_of_nonneg_right h_div (by positivity) _ = (1 / R) * (z * Real.exp (-z^2)) := by field_simp have h_int_right : IntegrableOn (fun z => (1 / R) * (z * Real.exp (-z^2))) (Set.Ici R) := by exact (h_weighted_gauss_int.mono_set (Set.Ici_subset_Ici.mpr (le_of_lt hR))).const_mul (1 / R) calc ∫ z in Set.Ici R, Real.exp (-z^2) ≤ ∫ z in Set.Ici R, (1 / R) * (z * Real.exp (-z^2)) := setIntegral_mono_on h_gauss_int.integrableOn h_int_right measurableSet_Ici h_pointwise _ = (1 / R) * ∫ z in Set.Ici R, z * Real.exp (-z^2) := by rw [integral_const_mul] calc ∫ z in Set.Ici R, Real.exp (-z^2) ≤ (1 / R) * ∫ z in Set.Ici R, z * Real.exp (-z^2) := h_main _ ≤ (1 / R) * ∫ z in Set.Ici 0, z * Real.exp (-z^2) := by gcongr- Project
- PDE
- License
- Apache-2.0
- Commit
- 0ab5d79a0d7a
- Source
- PDE/Basics/Heat/HeatSolutionProperty.lean:312-354
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.