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

State before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
Tactic:
apply bddAbove_square_of_tendsto
State after:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) (𝓝[≠] 0) (𝓝 ?y)

case y
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ ℝ

State before:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) (𝓝[≠] 0) (𝓝 ?y)

case y
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ ℝ
Tactic:
suffices Tendsto (norm ∘ (fun (s : ℂ) ↦ ↑x ^ s / s - ↑x ^ (0 : ℂ) / s - ↑x ^ s / (1 + s)))
    (𝓝[≠] 0) (𝓝 (‖(deriv (fun (s : ℂ) ↦ (x : ℂ) ^ s) 0) - x ^ (0 : ℂ) / (1 + 0)‖)) by
  apply this.congr'
  filter_upwards [diff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds
    (Set.mem_compl_singleton_iff.mpr (by norm_num : (0 : ℂ) ≠ -1))) {0}] with s hs
  rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.2 hs.1, cpow_zero]; ring_nf
State after:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)

State before:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
Tactic:
have hx0 : (x : ℂ) ≠ 0 := slitPlane_ne_zero (.inl xpos)
State after:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)

State before:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
Tactic:
refine (Tendsto.sub ?_ (tendsto_nhdsWithin_of_tendsto_nhds ?_)).norm
State after:
case hf.refine_1
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / x_1 - ↑x ^ 0 / x_1) (𝓝[≠] 0) (𝓝 (deriv (fun s => ↑x ^ s) 0))

case hf.refine_2
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / (1 + x_1)) (𝓝 0) (𝓝 (↑x ^ 0 / (1 + 0)))

State before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) (𝓝[≠] 0) (𝓝 ?y)
Tactic:
apply this.congr'
State after:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) =ᶠ[𝓝[≠] 0]
    Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s

State before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) =ᶠ[𝓝[≠] 0]
    Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s
Tactic:
filter_upwards [diff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds
  (Set.mem_compl_singleton_iff.mpr (by norm_num : (0 : ℂ) ≠ -1))) {0}] with s hs
State after:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
s : ℂ
hs : s ∈ {-1}ᶜ \ {0}
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) s =
    (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) s

State before:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
s : ℂ
hs : s ∈ {-1}ᶜ \ {0}
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) s =
    (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) s
Tactic:
rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.2 hs.1, cpow_zero]
State after:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
s : ℂ
hs : s ∈ {-1}ᶜ \ {0}
⊢ ‖↑x ^ s / s - 1 / s - ↑x ^ s / (1 + s)‖ = ‖↑x ^ s / s - ↑x ^ s / (s + 1) - 1 / s‖

State before:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
s : ℂ
hs : s ∈ {-1}ᶜ \ {0}
⊢ ‖↑x ^ s / s - 1 / s - ↑x ^ s / (1 + s)‖ = ‖↑x ^ s / s - ↑x ^ s / (s + 1) - 1 / s‖
Tactic:
ring_nf
State after:
no goals

State before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
⊢ 0 ≠ -1
Tactic:
norm_num
State after:
no goals

State before:
case hf.refine_1
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / x_1 - ↑x ^ 0 / x_1) (𝓝[≠] 0) (𝓝 (deriv (fun s => ↑x ^ s) 0))
Tactic:
convert hasDerivAt_iff_tendsto_slope.mp
  (differentiableAt_id'.const_cpow (.inl hx0)).hasDerivAt using 2
State after:
case h.e'_3.h
x✝¹ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
x✝ : ℂ
⊢ ↑x ^ x✝ / x✝ - ↑x ^ 0 / x✝ = slope (fun x_1 => ↑x ^ x_1) 0 x✝

State before:
case h.e'_3.h
x✝¹ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
x✝ : ℂ
⊢ ↑x ^ x✝ / x✝ - ↑x ^ 0 / x✝ = slope (fun x_1 => ↑x ^ x_1) 0 x✝
Tactic:
rw [slope_def_field]
State after:
case h.e'_3.h
x✝¹ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
x✝ : ℂ
⊢ ↑x ^ x✝ / x✝ - ↑x ^ 0 / x✝ = (↑x ^ x✝ - ↑x ^ 0) / (x✝ - 0)

State before:
case h.e'_3.h
x✝¹ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
x✝ : ℂ
⊢ ↑x ^ x✝ / x✝ - ↑x ^ 0 / x✝ = (↑x ^ x✝ - ↑x ^ 0) / (x✝ - 0)
Tactic:
ring
State after:
no goals

State before:
case hf.refine_2
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / (1 + x_1)) (𝓝 0) (𝓝 (↑x ^ 0 / (1 + 0)))
Tactic:
exact (continuous_id.const_cpow (.inl hx0)).tendsto 0
  |>.div (tendsto_const_nhds.add tendsto_id) (by norm_num)
State after:
no goals

State before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ 1 + 0 ≠ 0
Tactic:
norm_num
State after:
no goals