mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one

English

For ε > 0 and x ∈ ℝ, mulExpNegMulSq ε x = ε^{−1/2} · mulExpNegMulSq 1 (√ε x).

Русский

Для ε > 0 и x ∈ ℝ имеем mulExpNegMulSq ε x = ε^{−1/2} · mulExpNegMulSq 1 (√ε x).

LaTeX

$$$\\forall \\varepsilon > 0,\\; \\forall x\\in\\mathbb{R},\\; mulExpNegMulSq\\,\\varepsilon\\, x = (\\sqrt{\\varepsilon})^{-1} \\cdot mulExpNegMulSq\\,1\\, (\\sqrt{\\varepsilon}\\, x)$$$

Lean4

theorem mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one (hε : 0 < ε) (x : ℝ) :
    mulExpNegMulSq ε x = (√ε)⁻¹ * mulExpNegMulSq 1 (sqrt ε * x) :=
  by
  simp only [mulExpNegMulSq, one_mul]
  have h : √ε * x * (√ε * x) = ε * x * x := by
    ring_nf
    rw [sq_sqrt hε.le, mul_comm]
  rw [h, eq_inv_mul_iff_mul_eq₀ _]
  · ring_nf
  · intro h
    rw [← pow_eq_zero_iff (Ne.symm (Nat.zero_ne_add_one 1)), sq_sqrt hε.le] at h
    linarith

Похожие утверждения