-- 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:
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‖

Tactic:
exact norm_coe_le_norm g x

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 + -((↑n)⁻¹ * (ε * g x * g x))| ^ n ≤ 1

Tactic:
apply pow_le_one₀ (abs_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))| ≤ 1

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 : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ ‖g‖

Tactic:
rw [eventually_atTop]

Result:
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
⊢ ∃ a, ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑b)⁻¹ • -(ε • g * g)) ^ b) ω‖ ≤ ‖g‖

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
⊢ ∀ b ≥ N, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑b)⁻¹ • -(ε • g * g)) ^ b) ω‖ ≤ ‖g‖

Tactic:
intro n hn

Result:
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
⊢ ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ ‖g‖

Proof state:
case h_meas.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 : ℕ), AEStronglyMeasurable (⇑(g * (1 + (↑x)⁻¹ • -(ε • g * g)) ^ x)) P

Tactic:
exact fun n => StronglyMeasurable.aestronglyMeasurable (Continuous.stronglyMeasurable
    (Continuous.mul g.continuous ((1 + ((n : ℝ)⁻¹ • -(ε • g * g))) ^ n).continuous))

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 k => (1 + -(ε * (g x * g x)) / ↑k) ^ k) atTop (𝓝 (rexp (-(ε * (g x * g x)))))

Tactic:
exact tendsto_one_plus_div_pow_exp (-(ε * (g x * g x)))

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)

Tactic:
apply le_trans (by linarith) (sub_nonneg_of_le ((div_le_one hnpos).mpr _))

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) ≤ ↑n

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

Tactic:
apply Eventually.of_forall

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_meas
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (⇑(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n)) P

Tactic:
apply Eventually.of_forall

Result:
case h_meas.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 : ℕ), AEStronglyMeasurable (⇑(g * (1 + (↑x)⁻¹ • -(ε • g * g)) ^ x)) P

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:
apply Tendsto.const_mul (g 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 k => ((1 + (↑k)⁻¹ • -(ε • g * g)) ^ k) x) atTop (𝓝 (rexp (-(ε * g x * g x))))

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
⊢ ∃ a, ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑b)⁻¹ • -(ε • g * g)) ^ b) ω‖ ≤ ‖g‖

Tactic:
use N

Result:
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
⊢ ∀ b ≥ N, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑b)⁻¹ • -(ε • g * g)) ^ b) ω‖ ≤ ‖g‖

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 * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x‖ ≤ ‖g‖

Tactic:
simp only [smul_neg, BoundedContinuousFunction.coe_mul, Pi.mul_apply, pow_apply,
  BoundedContinuousFunction.coe_add, BoundedContinuousFunction.coe_one, coe_neg,
  BoundedContinuousFunction.coe_smul, smul_eq_mul, Pi.add_apply, Pi.one_apply, Pi.neg_apply,
  norm_mul, norm_eq_abs, norm_pow]

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 x| * |1 + -((↑n)⁻¹ * (ε * g x * g x))| ^ n ≤ ‖g‖

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 * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x‖ ≤ ‖g‖

Tactic:
intro x

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‖