internlm/Lean-Github huggingface dataset:
Theorem: Perron.residueAtNegOne
Proof state before:
case h.intro.intro.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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square (-1) c \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Square (-1) c ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Square (-1) c)
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I - 1) (↑c + ↑c * I - 1) = -↑x⁻¹
Tactic:
simp_rw [Square] at fHolo gHolo RectMemNhds
Proof state after:
case h.intro.intro.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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I - 1) (↑c + ↑c * I - 1) = -↑x⁻¹
Theorem: Perron.residueAtNegOne
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
⊢ 0 < 1 / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
s : ℂ
hs : s ∈ Square (-1) c
⊢ -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
Tactic:
rw [Square, mem_Rect (by simpa using by linarith) (by simp [cpos.le])] at hs
Proof state after:
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
s : ℂ
hs :
  (-↑c - ↑c * I + -1).re ≤ s.re ∧
    s.re ≤ (↑c + ↑c * I + -1).re ∧ (-↑c - ↑c * I + -1).im ≤ s.im ∧ s.im ≤ (↑c + ↑c * I + -1).im
⊢ -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
s : ℂ
hs :
  (-↑c - ↑c * I + -1).re ≤ s.re ∧
    s.re ≤ (↑c + ↑c * I + -1).re ∧ (-↑c - ↑c * I + -1).im ≤ s.im ∧ s.im ≤ (↑c + ↑c * I + -1).im
⊢ -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
Tactic:
simpa using hs
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
s : ℂ
hs : s ∈ Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1)
⊢ (-↑c - ↑c * I + -1).re ≤ (↑c + ↑c * I + -1).re
Tactic:
simpa using by linarith
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
s : ℂ
hs : s ∈ Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1)
⊢ 0 ≤ c
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
s : ℂ
hs : s ∈ Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1)
⊢ (-↑c - ↑c * I + -1).im ≤ (↑c + ↑c * I + -1).im
Tactic:
simp [cpos.le]
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
⊢ Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
Tactic:
refine fun s ⟨hs, hs1⟩ ↦ not_or.mpr ⟨?_, hs1⟩
Proof state after:
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
s : ℂ
x✝ : s ∈ Square (-1) c \ {-1}
hs : s ∈ Square (-1) c
hs1 : s ∉ {-1}
⊢ ¬s = 0
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
s : ℂ
x✝ : s ∈ Square (-1) c \ {-1}
hs : s ∈ Square (-1) c
hs1 : s ∉ {-1}
⊢ ¬s = 0
Tactic:
simpa [Complex.ext_iff] using fun _ _ ↦ by linarith [h_mem hs]
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
s : ℂ
x✝² : s ∈ Square (-1) c \ {-1}
hs : s ∈ Square (-1) c
hs1 : s ∉ {-1}
x✝¹ : s.re = 0
x✝ : s.im = 0
⊢ False
Tactic:
linarith [h_mem hs]
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square (-1) c \ {-1})
⊢ HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
Tactic:
refine fHolo.sub <| (differentiableOn_const _).neg.div ?_ fun x hx ↦ sPlusOneNeZero hx.2
Proof state after:
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square (-1) c \ {-1})
⊢ DifferentiableOn ℂ (fun y => y + 1) (Square (-1) c \ {-1})
Theorem: Perron.residueAtNegOne
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 : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Square (-1) c \ {-1})
⊢ DifferentiableOn ℂ (fun y => y + 1) (Square (-1) c \ {-1})
Tactic:
exact differentiableOn_id.add (differentiableOn_const 1)
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
Proof state before:
case h.intro.intro.intro.refine_1
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ (-↑c - ↑c * I - 1).re ≤ (↑c + ↑c * I - 1).re
Tactic:
simpa using cpos.le
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
Proof state before:
case h.intro.intro.intro.refine_2
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ (-↑c - ↑c * I - 1).im ≤ (↑c + ↑c * I - 1).im
Tactic:
simpa using cpos.le
Proof state after:
no goals
Theorem: Perron.residueAtNegOne
Proof state before:
case h.intro.intro.intro.refine_3
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
⊢ EqOn (f x - fun s => -↑x⁻¹ / (s - -1)) g (Rectangle (-↑c - ↑c * I - 1) (↑c + ↑c * I - 1) \ {-1})
Tactic:
convert g_eq_fDiff using 3
Proof state after:
case h.e'_3.h.e'_6.h
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
x✝ : ℂ
⊢ -↑x⁻¹ / (x✝ - -1) = -↑x⁻¹ / (x✝ + 1)
Theorem: Perron.residueAtNegOne
Proof state before:
case h.e'_3.h.e'_6.h
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)) - -↑x⁻¹ / (s + 1)) '' (Square (-1) c \ {-1}))
cpos : 0 < c
right✝ : c < 1 / 2
h_mem : ∀ {s : ℂ}, s ∈ Square (-1) c → -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) \ {-1})
f1Holo : HolomorphicOn (f x - fun s => -↑x⁻¹ / (s + 1)) (Square (-1) c \ {-1})
RectMemNhds : Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1) ∈ 𝓝 (-1)
g : ℂ → ℂ
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I + -1) (↑c + ↑c * I + -1))
g_eq_fDiff : EqOn (f x - fun s => -↑x⁻¹ / (s + 1)) g (Square (-1) c \ {-1})
x✝ : ℂ
⊢ -↑x⁻¹ / (x✝ - -1) = -↑x⁻¹ / (x✝ + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Perron.residuePull1
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
⊢ VerticalIntegral' (f x) σ = 1 + VerticalIntegral' (f x) (-1 / 2)
Tactic:
apply eq_add_of_sub_eq
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_gt_one : 1 < x
σ_pos : 0 < σ
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Theorem: Perron.residuePull1
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_gt_one : 1 < x
σ_pos : 0 < σ
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Tactic:
have xpos : 0 < x := zero_lt_one.trans x_gt_one
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Theorem: Perron.residuePull1
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Tactic:
have hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0}) :=
  (isHolomorphicOn xpos).mono fun s ⟨⟨⟨_, _⟩, _⟩, hs0⟩ hc ↦ hc.casesOn
    (fun hc ↦ hs0 hc) (fun hc ↦ by linarith [show s.re = -1 from congrArg _ hc])
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Theorem: Perron.residuePull1
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Tactic:
have := (residueAtZero xpos).and <| verticalIntegral_sub_verticalIntegral_eq_squareIntegral
  (by simpa using ⟨by linarith, by linarith⟩) hf
  (tendsto_zero_Lower xpos _ _) (tendsto_zero_Upper xpos _ _)
  (isIntegrable xpos (by norm_num) (by norm_num)) (isIntegrable xpos (by linarith) (by linarith))
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I) (↑x_1 + ↑x_1 * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + 0) (↑x_1 + ↑x_1 * I + 0)
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Theorem: Perron.residuePull1
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I) (↑x_1 + ↑x_1 * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + 0) (↑x_1 + ↑x_1 * I + 0)
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Tactic:
obtain ⟨c, hcf, hc⟩ := this.exists_mem
Proof state after:
case h.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I) (↑x_1 + ↑x_1 * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + 0) (↑x_1 + ↑x_1 * I + 0)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I) (↑y + ↑y * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + 0) (↑y + ↑y * I + 0)
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Theorem: Perron.residuePull1
Proof state before:
case h.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I) (↑x_1 + ↑x_1 * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + 0) (↑x_1 + ↑x_1 * I + 0)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I) (↑y + ↑y * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + 0) (↑y + ↑y * I + 0)
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Tactic:
obtain ⟨ε, hε, hεc⟩ := Metric.mem_nhdsWithin_iff.mp hcf
Proof state after:
case h.intro.intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I) (↑x_1 + ↑x_1 * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + 0) (↑x_1 + ↑x_1 * I + 0)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I) (↑y + ↑y * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + 0) (↑y + ↑y * I + 0)
ε : ℝ
hε : ε > 0
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Theorem: Perron.residuePull1
Proof state before:
case h.intro.intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I) (↑x_1 + ↑x_1 * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + 0) (↑x_1 + ↑x_1 * I + 0)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I) (↑y + ↑y * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + 0) (↑y + ↑y * I + 0)
ε : ℝ
hε : ε > 0
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1
Tactic:
obtain hε := hc (ε/2) (hεc ⟨mem_ball_iff_norm.mpr (by simp [abs_of_pos hε, hε]), half_pos hε⟩)
Proof state after:
case h.intro.intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I) (↑x_1 + ↑x_1 * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + 0) (↑x_1 + ↑x_1 * I + 0)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I) (↑y + ↑y * I) = 1 ∧
      VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + 0) (↑y + ↑y * I + 0)
ε : ℝ
hε✝ : ε > 0
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
hε :
  RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I) (↑(ε / 2) + ↑(ε / 2) * I) = 1 ∧
    VerticalIntegral (f x) σ - VerticalIntegral (f x) (-1 / 2) =
      RectangleIntegral (f x) (-↑(ε / 2) - ↑(ε / 2) * I + 0) (↑(ε / 2) + ↑(ε / 2) * I + 0)
⊢ VerticalIntegral' (f x) σ - VerticalIntegral' (f x) (-1 / 2) = 1