awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
set :
  let y := ε * x * x;
  ∀ (heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)) (hy : y = ε * x * x),
    rexp (-y) * |1 - 2 * y| ≤ 1
⊢ rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1

Tactic:
set y := ε * x * x with hy
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
rw : 0 ≤ ε * (x * x)
⊢ 0 ≤ y

Tactic:
rw [hy, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ ε * (x * x)

Tactic:
mul_nonneg hε.le (mul_self_nonneg x)

Premises used: mul_self_nonneg, mul_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ ε * (x * x)

Tactic:
exact mul_nonneg hε.le (mul_self_nonneg x)

Premises used: mul_self_nonneg, mul_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ y

Tactic:
have hynonneg : 0 ≤ y := by
    rw [hy, mul_assoc]
    exact mul_nonneg hε.le (mul_self_nonneg x)
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
apply : |1 - 2 * y| ≤ (rexp (-y))⁻¹ * 1
⊢ rexp (-y) * |1 - 2 * y| ≤ 1

Tactic:
apply mul_le_of_le_inv_mul₀ (zero_le_one' ℝ) (exp_nonneg _)

Premises used: Real, zero_le_one', mul_le_of_le_inv_mul₀, Real.exp_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
simp : 2 * y ≤ 1 + rexp y ∧ 1 ≤ rexp y + 2 * y
⊢ |1 - 2 * y| ≤ (rexp (-y))⁻¹ * 1

Tactic:
simp only [← exp_neg (-y), neg_neg, mul_one, abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right]

Premises used: abs_le, neg_neg, tsub_le_iff_right, mul_one, neg_le_sub_iff_le_add, Real.exp_neg, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 2 * y ≤ 1 + rexp y ∧ 1 ≤ rexp y + 2 * y

Tactic:
⟨le_trans two_mul_le_exp ((le_add_iff_nonneg_left (exp y)).mpr zero_le_one), ?_⟩

Premises used: Iff.mpr, Real.two_mul_le_exp, Real.exp, zero_le_one, And.intro, le_add_iff_nonneg_left, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
refine : 1 ≤ rexp y + 2 * y
⊢ 2 * y ≤ 1 + rexp y ∧ 1 ≤ rexp y + 2 * y

Tactic:
refine ⟨le_trans two_mul_le_exp ((le_add_iff_nonneg_left (exp y)).mpr zero_le_one), ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 0 ≤ 2 * y

Tactic:
simp [hynonneg]
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 1 ≤ rexp y + 2 * y

Tactic:
exact le_trans (one_le_exp hynonneg) (le_add_of_nonneg_right (by simp [hynonneg]))

Premises used: le_add_of_nonneg_right, Real.one_le_exp, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ (↑1 : ℝ)

Tactic:
norm_deriv_mulExpNegMulSq_le_one hε x

Premises used: Real.norm_deriv_mulExpNegMulSq_le_one, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ (↑1 : ℝ)

Tactic:
exact norm_deriv_mulExpNegMulSq_le_one hε x

Premises used: Real.norm_deriv_mulExpNegMulSq_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
apply : ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1
⊢ LipschitzWith 1 ε.mulExpNegMulSq

Tactic:
apply lipschitzWith_of_nnnorm_deriv_le differentiable_mulExpNegMulSq

Premises used: Real.differentiable_mulExpNegMulSq, lipschitzWith_of_nnnorm_deriv_le
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
⊢ ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

Tactic:
nnnorm_deriv_mulExpNegMulSq_le_one hε

Premises used: Real.nnnorm_deriv_mulExpNegMulSq_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
⊢ ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

Tactic:
exact nnnorm_deriv_mulExpNegMulSq_le_one hε

Premises used: Real.nnnorm_deriv_mulExpNegMulSq_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ε.mulExpNegMulSq x = (√ε)⁻¹ * mulExpNegMulSq 1 (√ε * x)

Tactic:
grind [mulExpNegMulSq]

Premises used: Real.mulExpNegMulSq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ 0 < (√ε)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
rw : (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹
⊢ |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹

Tactic:
rw [mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one hε x, abs_mul, abs_of_pos (by positivity)]

Premises used: abs_mul, Real.mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
ha : 0 ≤ (√ε)⁻¹
h : |mulExpNegMulSq 1 (√ε * x)| ≤ 1
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹

Tactic:
apply mul_le_of_le_one_right

Premises used: mul_le_of_le_one_right
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ 0 ≤ (√ε)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |mulExpNegMulSq 1 (√ε * x)| ≤ 1

Tactic:
abs_mulExpNegMulSq_one_le_one (√ε * x)

Premises used: HMul.hMul, Real.abs_mulExpNegMulSq_one_le_one, Real.sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |mulExpNegMulSq 1 (√ε * x)| ≤ 1

Tactic:
exact abs_mulExpNegMulSq_one_le_one (√ε * x)

Premises used: HMul.hMul, Real.abs_mulExpNegMulSq_one_le_one, Real.sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
apply : dist (ε.mulExpNegMulSq x) 0 + dist 0 (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

Tactic:
apply le_trans (dist_triangle (mulExpNegMulSq ε x) 0 (mulExpNegMulSq ε y))

Premises used: dist_triangle, Real.mulExpNegMulSq, OfNat.ofNat, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
simp : |ε.mulExpNegMulSq x| + |ε.mulExpNegMulSq y| ≤ (√ε)⁻¹ + (√ε)⁻¹
⊢ dist (ε.mulExpNegMulSq x) 0 + dist 0 (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

Tactic:
simp only [dist_zero_right, norm_eq_abs, dist_zero_left, two_mul]

Premises used: two_mul, dist_zero_left, dist_zero_right, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ |ε.mulExpNegMulSq x| + |ε.mulExpNegMulSq y| ≤ (√ε)⁻¹ + (√ε)⁻¹

Tactic:
add_le_add (abs_mulExpNegMulSq_le hε) (abs_mulExpNegMulSq_le hε)

Premises used: add_le_add, Real.abs_mulExpNegMulSq_le
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ |ε.mulExpNegMulSq x| + |ε.mulExpNegMulSq y| ≤ (√ε)⁻¹ + (√ε)⁻¹

Tactic:
exact add_le_add (abs_mulExpNegMulSq_le hε) (abs_mulExpNegMulSq_le hε)

Premises used: add_le_add, Real.abs_mulExpNegMulSq_le
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ (↑1 : ℝ≥0∞) * edist x y

Tactic:
have h := lipschitzWith_one_mulExpNegMulSq hε x y
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ (↑1 : ℝ≥0∞) * edist x y
rwa :
  ∀ (h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 1 * edist x y),
    dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
rwa₁ :
  ∀ (h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ edist x y),
    dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (h : (edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y)).toReal ≤ (edist x y).toReal),
    dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

Tactic:
rwa [ENNReal.coe_one, one_mul, ← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))] at h

Premises used: ENNReal.coe_one, edist_ne_top, ENNReal.toReal_le_toReal, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
⊢ x = (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0

Tactic:
simp only [mulExpNegMulSq, zero_mul, neg_zero, exp_zero, mul_one]

Premises used: MulZeroClass.zero_mul, Real.mulExpNegMulSq, Real.exp_zero, mul_one, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
⊢ x = (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0

Tactic:
have : x = (fun ε : ℝ => mulExpNegMulSq ε x) 0 := by
    simp only [mulExpNegMulSq, zero_mul, neg_zero, exp_zero, mul_one]
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
this : x = (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0
nth_rw : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 ((fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0))
⊢ Tendsto (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Tactic:
nth_rw 2 [this]
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
x : ℝ
this : x = (fun (ε : ℝ) ↦ ε.mulExpNegMulSq x) 0
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ rexp (-(ε * x * x))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
simp :
  HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
      (rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))) ≤
    ‖g‖
⊢ |(ε.mulExpNegMulSq ∘ (⇑g : (a : E) → ℝ)) x| ≤ ‖g‖

Tactic:
simp only [Function.comp_apply, mulExpNegMulSq, abs_mul, abs_exp]

Premises used: abs_mul, Real.mulExpNegMulSq, Function.comp_apply, Real.abs_exp
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
apply : rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ)) ≤ 1
⊢ HMul.hMul (α := ℝ) (|(g : (a : E) → ℝ) x| : ℝ)
      (rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ))) ≤
    ‖g‖

Tactic:
apply le_trans (mul_le_of_le_one_right (abs_nonneg (g x)) _) (g.norm_coe_le_norm x)

Premises used: mul_le_of_le_one_right, BoundedContinuousFunction.norm_coe_le_norm, DFunLike.coe, abs_nonneg, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
rw : 0 ≤ ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ)
⊢ rexp (-HMul.hMul (β := ℝ) (HMul.hMul (β := ℝ) ε ((g : (a : E) → ℝ) x : ℝ)) ((g : (a : E) → ℝ) x : ℝ)) ≤ 1

Tactic:
rw [exp_le_one_iff, Left.neg_nonpos_iff, mul_assoc]

Premises used: mul_assoc, Left.neg_nonpos_iff, Real.exp_le_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ 0 ≤ ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ)

Tactic:
mul_nonneg hε (mul_self_nonneg (g x))

Premises used: mul_self_nonneg, mul_nonneg, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Goal:
ε : ℝ
E : Type u_1
inst : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ 0 ≤ ε * HMul.hMul (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g : (a : E) → ℝ) x : ℝ)

Tactic:
exact mul_nonneg hε (mul_self_nonneg (g x))

Premises used: mul_self_nonneg, mul_nonneg, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ Continuous[inst, _] fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
apply :
  ∀ (x y : E),
    dist
        (ContinuousMap.toFun
          { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := ⋯ : C(E, ℝ) } x)
        (ContinuousMap.toFun
          { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := ⋯ : C(E, ℝ) } y) ≤
      2 * (√ε)⁻¹
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x)) P

Tactic:
apply integrable P ⟨⟨fun x => mulExpNegMulSq ε (f x), by fun_prop⟩, ⟨2 * (√ε)⁻¹, _⟩⟩

Premises used: HMul.hMul, ContinuousMap.mk, BoundedContinuousFunction.integrable, Inv.inv, BoundedContinuousFunction.mk, Exists.intro, Real.mulExpNegMulSq, Real.sqrt, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ ∀ (x y : E),
    dist
        (ContinuousMap.toFun
          { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := ⋯ : C(E, ℝ) } x)
        (ContinuousMap.toFun
          { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := ⋯ : C(E, ℝ) } y) ≤
      2 * (√ε)⁻¹

Tactic:
fun x y => dist_mulExpNegMulSq_le_two_mul_sqrt hε (f x) (f y)

Premises used: Real.dist_mulExpNegMulSq_le_two_mul_sqrt, Real.mulExpNegMulSq, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ ∀ (x y : E),
    dist
        (ContinuousMap.toFun
          { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := ⋯ : C(E, ℝ) } x)
        (ContinuousMap.toFun
          { toFun := fun (x : E) ↦ ε.mulExpNegMulSq ((f : (a : E) → ℝ) x), continuous_toFun := ⋯ : C(E, ℝ) } y) ≤
      2 * (√ε)⁻¹

Tactic:
exact fun x y => dist_mulExpNegMulSq_le_two_mul_sqrt hε (f x) (f y)

Premises used: Real.dist_mulExpNegMulSq_le_two_mul_sqrt, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
g : C(E, ℝ)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ε.mulExpNegMulSq ((g : (a : E) → ℝ) x)) (P.restrict K)

Tactic:
g.continuous.mulExpNegMulSq.continuousOn.integrableOn_compact' hK hKmeas

Premises used: ContinuousMap.continuous, Continuous.continuousOn, MeasureTheory.IntegrableOn, Continuous.mulExpNegMulSq, ContinuousOn.integrableOn_compact'
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
a :
  ∀ (x : ℕ → ℝ),
    Tendsto x atTop (𝓝[>] 0) →
      Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ x) atTop
        (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
⊢ Tendsto (β := ℝ) (fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) (𝓝[>] 0)
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))

Tactic:
apply tendsto_of_seq_tendsto

Premises used: Filter.tendsto_of_seq_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
a :
  ∀ (N : ℕ) (hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)),
    Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
      (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))
⊢ Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))

Tactic:
obtain ⟨N, hupos⟩ := eventually_atTop.mp (tendsto_nhdsWithin_iff.mp hu).2

Premises used: tendsto_nhdsWithin_iff, And.right, Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
h_meas : ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (ω : E) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) P
h_bound : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ C
h_lim :
  ∀ᵐ (ω : E) ∂P,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) atTop
      (𝓝 ((g : (a : E) → ℝ) ω) : Filter ℝ)
⊢ Tendsto (β := ℝ) ((fun (ε : ℝ) ↦ ∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P) ∘ u) atTop
    (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂P))

Tactic:
apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim

Premises used: MeasureTheory.tendsto_integral_filter_of_norm_le_const
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (ω : E) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) P

Tactic:
Eventually.of_forall (fun n => g.continuous.mulExpNegMulSq.aestronglyMeasurable)

Premises used: Filter.Eventually.of_forall, BoundedContinuousFunction.continuous, Continuous.mulExpNegMulSq, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (ω : E) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) P

Tactic:
exact Eventually.of_forall (fun n => g.continuous.mulExpNegMulSq.aestronglyMeasurable)

Premises used: Filter.Eventually.of_forall, BoundedContinuousFunction.continuous, Continuous.mulExpNegMulSq, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
h : ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
⊢ ∃ (C : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ C

Tactic:
use norm g

Premises used: Norm.norm
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
h : ∃ (a : ℕ), ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
h : ∀ b ≥ N, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖
⊢ ∃ (a : ℕ), ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖

Tactic:
use N
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖

Tactic:
Eventually.of_forall
      (fun _ => abs_mulExpNegMulSq_comp_le_norm g (le_of_lt (Set.mem_Ioi.mp (hupos n hn))))

Premises used: le_of_lt, Real.abs_mulExpNegMulSq_comp_le_norm, Set.mem_Ioi, Filter.Eventually.of_forall, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)‖ ≤ ‖g‖

Tactic:
exact Eventually.of_forall
      (fun _ => abs_mulExpNegMulSq_comp_le_norm g (le_of_lt (Set.mem_Ioi.mp (hupos n hn))))

Premises used: le_of_lt, Real.abs_mulExpNegMulSq_comp_le_norm, Set.mem_Ioi, Filter.Eventually.of_forall, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ ∀ᵐ (ω : E) ∂P,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) atTop
      (𝓝 ((g : (a : E) → ℝ) ω) : Filter ℝ)

Tactic:
Eventually.of_forall (fun _ => (tendsto_nhdsWithin_of_tendsto_nhds
        tendsto_mulExpNegMulSq).comp hu)

Premises used: Filter.Eventually.of_forall, tendsto_nhdsWithin_of_tendsto_nhds, Filter.Tendsto.comp, Real.tendsto_mulExpNegMulSq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, Membership.mem (γ := Set ℝ) (Set.Ioi 0) (u b)
⊢ ∀ᵐ (ω : E) ∂P,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ (u n).mulExpNegMulSq ((g : (a : E) → ℝ) ω)) atTop
      (𝓝 ((g : (a : E) → ℝ) ω) : Filter ℝ)

Tactic:
exact Eventually.of_forall (fun _ => (tendsto_nhdsWithin_of_tendsto_nhds
        tendsto_mulExpNegMulSq).comp hu)

Premises used: Filter.Eventually.of_forall, tendsto_nhdsWithin_of_tendsto_nhds, Filter.Tendsto.comp, Real.tendsto_mulExpNegMulSq