Theorem: Perron.diffBddAtNegOne (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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
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)) - -↑x⁻¹ / (s + 1)) (𝓝[≠] (-1)) (𝓝 ?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)) - -↑x⁻¹ / (s + 1)) (𝓝[≠] (-1)) (𝓝 ?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 ^ s / (s + 1) - x⁻¹ / (s + 1))))
    (𝓝[≠] (-1)) (𝓝 (‖x ^ (-1 : ℂ) / -1 - (deriv (fun (s : ℂ) ↦ (x : ℂ) ^ s) (-1))‖)) by
  apply this.congr'
  filter_upwards [diff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds
    (Set.mem_compl_singleton_iff.mpr (by norm_num : (-1 : ℂ) ≠ 0))) {-1}] with s hs
  rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.1 hs.2]
  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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)

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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)

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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
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) (𝓝 (-1)) (𝓝 (↑x ^ (-1) / -1))

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 / (x_1 + 1) - ↑x⁻¹ / (x_1 + 1)) (𝓝[≠] (-1)) (𝓝 (deriv (fun s => ↑x ^ s) (-1)))

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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) (𝓝[≠] (-1)) (𝓝 ?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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) =ᶠ[𝓝[≠] (-1)]
    Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)

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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) =ᶠ[𝓝[≠] (-1)]
    Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)
Tactic:
filter_upwards [diff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds
  (Set.mem_compl_singleton_iff.mpr (by norm_num : (-1 : ℂ) ≠ 0))) {-1}] 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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
s : ℂ
hs : s ∈ {0}ᶜ \ {-1}
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) s =
    (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
s : ℂ
hs : s ∈ {0}ᶜ \ {-1}
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) s =
    (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) s
Tactic:
rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.1 hs.2]
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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
s : ℂ
hs : s ∈ {0}ᶜ \ {-1}
⊢ ‖↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))‖ = ‖↑x ^ s / s - ↑x ^ s / (s + 1) - -↑x⁻¹ / (s + 1)‖

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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
s : ℂ
hs : s ∈ {0}ᶜ \ {-1}
⊢ ‖↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))‖ = ‖↑x ^ s / s - ↑x ^ s / (s + 1) - -↑x⁻¹ / (s + 1)‖
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 ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)
⊢ -1 ≠ 0
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) (𝓝 (-1)) (𝓝 (↑x ^ (-1) / -1))
Tactic:
exact ((continuous_id.const_cpow (.inl hx0)).tendsto _).div 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
Tactic:
norm_num
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 / (x_1 + 1) - ↑x⁻¹ / (x_1 + 1)) (𝓝[≠] (-1)) (𝓝 (deriv (fun s => ↑x ^ s) (-1)))
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✝ + 1) - ↑x⁻¹ / (x✝ + 1) = slope (fun x_1 => ↑x ^ x_1) (-1) 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✝ + 1) - ↑x⁻¹ / (x✝ + 1) = slope (fun x_1 => ↑x ^ x_1) (-1) x✝
Tactic:
rw [slope_def_field, cpow_neg_one, ofReal_inv]
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✝ + 1) - (↑x)⁻¹ / (x✝ + 1) = (↑x ^ x✝ - (↑x)⁻¹) / (x✝ - -1)

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✝ + 1) - (↑x)⁻¹ / (x✝ + 1) = (↑x ^ x✝ - (↑x)⁻¹) / (x✝ - -1)
Tactic:
ring
State after:
no goals