internlm/Lean-Github huggingface dataset:
Theorem: Perron.diffBddAtZero
Proof 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]
Proof 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‖
Theorem: Perron.diffBddAtZero
Proof 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
Proof state after:
no goals
Theorem: Perron.diffBddAtZero
Proof 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
Proof state after:
no goals
Theorem: Perron.diffBddAtZero
Proof 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
Proof 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✝
Theorem: Perron.diffBddAtZero
Proof 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]
Proof 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)
Theorem: Perron.diffBddAtZero
Proof 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
Proof state after:
no goals
Theorem: Perron.diffBddAtZero
Proof 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)
Proof state after:
no goals
Theorem: Perron.diffBddAtZero
Proof 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
Proof state after:
no goals
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof 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
⊢ ℝ
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof 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)‖)
Theorem: Perron.diffBddAtNegOne
Proof 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)
Proof 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)‖)
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof 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)))
Theorem: Perron.diffBddAtNegOne
Proof 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'
Proof 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)
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof 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
Theorem: Perron.diffBddAtNegOne
Proof 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]
Proof 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)‖
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof state after:
no goals
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof state after:
no goals
Theorem: Perron.diffBddAtNegOne
Proof 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)
Proof state after:
no goals
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof state after:
no goals
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof 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✝
Theorem: Perron.diffBddAtNegOne
Proof 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]
Proof 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)
Theorem: Perron.diffBddAtNegOne
Proof 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
Proof state after:
no goals
Theorem: Perron.residueAtZero
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' (by linarith : (0 : ℝ) < 1 / 2), diffBddAtZero xpos]
Proof state after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
⊢ ∀ a ∈ Ioo 0 (1 / 2),
    BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 a \ {0})) →
      RectangleIntegral' (f x) (-↑a - ↑a * I) (↑a + ↑a * I) = 1
Theorem: Perron.residueAtZero
Proof state before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
⊢ ∀ a ∈ Ioo 0 (1 / 2),
    BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 a \ {0})) →
      RectangleIntegral' (f x) (-↑a - ↑a * I) (↑a + ↑a * I) = 1
Tactic:
intro c hc bddAbove
Proof state after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
hc : c ∈ Ioo 0 (1 / 2)
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Theorem: Perron.residueAtZero
Proof state before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
hc : c ∈ Ioo 0 (1 / 2)
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
obtain ⟨cpos, _⟩ := hc
Proof state after:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Theorem: Perron.residueAtZero
Proof state before:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ := by
  refine fun s ⟨hs, hs0⟩ ↦ not_or.mpr ⟨hs0, ?_⟩
  rw [Square, mem_Rect (by simpa using by linarith) (by simp [cpos.le])] at hs
  replace hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c := by simpa using hs
  simpa [Complex.ext_iff] using fun h ↦ by linarith
Proof state after:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Theorem: Perron.residueAtZero
Proof state before:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have fHolo : HolomorphicOn (f x) (Square 0 c \ {0}) := (isHolomorphicOn xpos).mono RectSub
Proof state after:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Theorem: Perron.residueAtZero
Proof state before:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have f1Holo : HolomorphicOn ((f x) - (fun (s : ℂ) ↦ 1 / s)) (Square 0 c \ {0}) :=
  fHolo.sub (by simpa using differentiableOn_inv.mono fun s hs ↦ hs.2)
Proof state after:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Theorem: Perron.residueAtZero
Proof state before:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have RectMemNhds : Square 0 c ∈ 𝓝 0 := square_mem_nhds 0 (ne_of_gt cpos)
Proof state after:
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
RectMemNhds : Square 0 c ∈ 𝓝 0
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1