apply tendsto_integral_filter_of_dominated_convergence (bound := bound)
case neg.intro.intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
case neg.intro.intro.intro.hF_meas
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1, AEStronglyMeasurable (fun a => G (↑n + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) volume

case neg.intro.intro.intro.h_bound
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1, ∀ᵐ (a : ℝ), ‖G (↑n + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)‖ ≤ bound a

case neg.intro.intro.intro.bound_integrable
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ Integrable bound volume

case neg.intro.intro.intro.h_lim
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ ∀ᵐ (a : ℝ),
    Tendsto (fun n => G (↑n + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) (𝓝[>] 1)
      (𝓝 (G (1 + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)))