-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem tendsto_integral_mul_one_plus_inv_smul_sq_pow (g : E →ᵇ ℝ) (hε : 0 < ε) :
    Tendsto (fun (n : ℕ) => ∫ x, (g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n) x ∂ P)
    atTop (𝓝 (∫ x, mulExpNegMulSq ε (g x) ∂P))

Proof state:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
⊢ ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ ‖g‖

Tactic:
apply Eventually.of_forall

Result:
case h.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
⊢ ∀ (x : E), ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x‖ ≤ ‖g‖

Proof state:
case h_bound
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ C

Tactic:
obtain ⟨N, hgN⟩ := exists_nat_gt (ε * (norm g * norm g))

Result:
case h_bound.intro
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ C

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ g x * g x ≤ ‖g‖ * ‖g‖

Tactic:
rw [← abs_le_iff_mul_self_le, abs_norm]

Result:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ |g x| ≤ ‖g‖

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ ε * (g x * g x) ≤ ↑n

Tactic:
apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)

Result:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ ε * (g x * g x) ≤ ε * (‖g‖ * ‖g‖)

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
⊢ 0 ≤ ε * (‖g‖ * ‖g‖)

Tactic:
exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))

Result:
no goals

Proof state:
case h_lim.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ (x : E), Tendsto (fun n => (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x) atTop (𝓝 (ε.mulExpNegMulSq (g x)))

Tactic:
intro x

Result:
case h_lim.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
x : E
⊢ Tendsto (fun n => (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x) atTop (𝓝 (ε.mulExpNegMulSq (g x)))

Proof state:
case h.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ |g x| * |1 + -((↑n)⁻¹ * (ε * g x * g x))| ^ n ≤ ‖g‖

Tactic:
refine (mul_le_mul_of_nonneg_right (norm_coe_le_norm g x) (pow_nonneg (abs_nonneg _) n)).trans
  <| mul_le_of_le_one_right (norm_nonneg _) ?_

Result:
case h.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ |1 + -((↑n)⁻¹ * (ε * g x * g x))| ^ n ≤ 1

Proof state:
case h_lim.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
x : E
⊢ Tendsto (fun k => ((1 + (↑k)⁻¹ • -(ε • g * g)) ^ k) x) atTop (𝓝 (rexp (-(ε * g x * g x))))

Tactic:
simp [mul_assoc, inv_mul_eq_div, ← neg_div]

Result:
case h_lim.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
x : E
⊢ Tendsto (fun k => (1 + -(ε * (g x * g x)) / ↑k) ^ k) atTop (𝓝 (rexp (-(ε * (g x * g x)))))

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 0

Tactic:
linarith

Result:
no goals

Proof state:
case h.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 1 + -(ε * (g x * g x) / ↑n) ∧ 1 + -(ε * (g x * g x) / ↑n) ≤ 1

Tactic:
refine ⟨?_, (add_le_iff_nonpos_right 1).mpr (Left.neg_nonpos_iff.mpr
  (div_nonneg (mul_nonneg (le_of_lt hε) (mul_self_nonneg (g x))) (le_of_lt hnpos)))⟩

Result:
case h.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 1 + -(ε * (g x * g x) / ↑n)

Proof state:
case h.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ |1 + -((↑n)⁻¹ * (ε * g x * g x))| ≤ 1

Tactic:
rw [mul_assoc, inv_mul_eq_div, abs_le]

Result:
case h.hp
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 1 + -(ε * (g x * g x) / ↑n) ∧ 1 + -(ε * (g x * g x) / ↑n) ≤ 1

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ ε * (g x * g x) ≤ ε * (‖g‖ * ‖g‖)

Tactic:
apply mul_le_mul (Preorder.le_refl ε) _ (mul_self_nonneg (g x)) (le_of_lt hε)

Result:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : n ≥ N
hnpos : 0 < ↑n
x : E
⊢ g x * g x ≤ ‖g‖ * ‖g‖