Theorem: Perron.bddAbove_square_of_tendsto (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Tactic:
obtain ⟨t, htf, ht⟩ := eventually_smallSets.mp hf.eventually_bddAbove
State after:
case intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))

State before:
case intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Tactic:
obtain ⟨ε, hε0, hε⟩ := nhdsWithin_hasBasis (nhds_hasBasis_square x) {x}ᶜ |>.1 t |>.mp htf
State after:
case intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))

State before:
case intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' hε0] with ε' ⟨hε'0, hε'⟩
State after:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
ε' : ℝ
hε'0 : 0 < ε'
hε' : ε' < ε
⊢ BddAbove (f '' (Square x ε' \ {x}))

State before:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
ε' : ℝ
hε'0 : 0 < ε'
hε' : ε' < ε
⊢ BddAbove (f '' (Square x ε' \ {x}))
Tactic:
exact ht _ <| (diff_subset_diff (square_subset_square hε'0 hε'.le) subset_rfl).trans hε
State after:
no goals