-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem tendsto_integral_mulExpNegMulSq_comp (g : E →ᵇ ℝ) :
    Tendsto (fun ε => ∫ x, mulExpNegMulSq ε (g x) ∂P) (𝓝[>] 0) (𝓝 (∫ x, g x ∂P))

Proof state:
case a.intro
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ Tendsto ((fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))

Tactic:
apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim

Result:
case h_meas
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (fun ω => (u n).mulExpNegMulSq (g ω)) P

case h_bound
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ C

case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n => (u n).mulExpNegMulSq (g ω)) atTop (𝓝 (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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∃ a, ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq (g ω)‖ ≤ ‖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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ b ≥ N, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq (g ω)‖ ≤ ‖g‖

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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n => (u n).mulExpNegMulSq (g ω)) atTop (𝓝 (g ω))

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

Result:
no goals

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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ C

Tactic:
use norm g

Result:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ ‖g‖

Proof state:
case a
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
⊢ ∀ (x : ℕ → ℝ),
    Tendsto x atTop (𝓝[>] 0) →
      Tendsto ((fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ x) atTop (𝓝 (∫ (x : E), g x ∂P))

Tactic:
intro u hu

Result:
case a
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
⊢ Tendsto ((fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ b ≥ N, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq (g ω)‖ ≤ ‖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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (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 →ᵇ ℝ
⊢ Tendsto (fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) (𝓝[>] 0) (𝓝 (∫ (x : E), g x ∂P))

Tactic:
apply tendsto_of_seq_tendsto

Result:
case a
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
⊢ ∀ (x : ℕ → ℝ),
    Tendsto x atTop (𝓝[>] 0) →
      Tendsto ((fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ x) atTop (𝓝 (∫ (x : E), g x ∂P))

Proof state:
case a
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
⊢ Tendsto ((fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))

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

Result:
case a.intro
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ Tendsto ((fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), 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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ ‖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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∃ a, ∀ b ≥ a, ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq (g ω)‖ ≤ ‖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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ ‖g‖

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

Result:
no goals

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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ b ≥ N, u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (fun ω => (u n).mulExpNegMulSq (g ω)) P

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

Result:
no goals