English
If ε > 0 and x ∈ ℝ, then ∥deriv (mulExpNegMulSq ε) x∥ ≤ 1.
Русский
Если ε > 0 и x ∈ ℝ, то ∥d/dx [mulExpNegMulSq ε] (x)∥ ≤ 1.
LaTeX
$$$\\forall \\varepsilon > 0, \\; \\forall x \\in \\mathbb{R},\\; \\|\\dfrac{d}{dx} (mulExpNegMulSq\\,\\varepsilon)(x)\\| \\le 1$$$
Lean4
theorem norm_deriv_mulExpNegMulSq_le_one (hε : 0 < ε) (x : ℝ) : ‖deriv (mulExpNegMulSq ε) x‖ ≤ 1 :=
by
rw [norm_eq_abs, deriv_mulExpNegMulSq]
have heq :
exp (-(ε * x * x)) + x * (exp (-(ε * x * x)) * (-2 * ε * x)) = exp (-(ε * x * x)) * (1 - 2 * (ε * x * x)) := by ring
rw [heq, abs_mul, abs_exp]
set y := ε * x * x with hy
have hynonneg : 0 ≤ y := by
rw [hy, mul_assoc]
exact mul_nonneg hε.le (mul_self_nonneg x)
apply mul_le_of_le_inv_mul₀ (zero_le_one' ℝ) (exp_nonneg _)
simp only [← exp_neg (-y), neg_neg, mul_one, abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right]
refine ⟨le_trans two_mul_le_exp ((le_add_iff_nonneg_left (exp y)).mpr zero_le_one), ?_⟩
exact le_trans (one_le_exp hynonneg) (le_add_of_nonneg_right (by simp [hynonneg]))
