internlm/Lean-Github huggingface dataset:
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
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
Tactic:
rw [VerticalIntegral', ← smul_sub, hε.2, ← RectangleIntegral', add_zero, add_zero, hε.1]
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 < σ
xpos : 0 < x
s : ℂ
x✝ : s ∈ Icc (-1 / 2) σ ×ℂ univ \ {0}
hc✝ : s ∈ {0, -1}
left✝ : -1 / 2 ≤ s.re
right✝¹ : s.re ≤ σ
right✝ : s ∈ im ⁻¹' univ
hs0 : s ∉ {0}
hc : s ∈ {-1}
⊢ False
Tactic:
linarith [show s.re = -1 from congrArg _ hc]
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 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ -1 / 2 < re 0 ∧ re 0 < σ
Tactic:
simpa using ⟨by linarith, by linarith⟩
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 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ -1 / 2 < 0
Tactic:
linarith
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 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ 0 < σ
Tactic:
linarith
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 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ -1 / 2 ≠ 0
Tactic:
norm_num
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 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ -1 / 2 ≠ -1
Tactic:
norm_num
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 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ σ ≠ 0
Tactic:
linarith
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 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ σ ≠ -1
Tactic:
linarith
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 < σ
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
⊢ ‖ε / 2 - 0‖ < ε
Tactic:
simp [abs_of_pos hε, hε]
Proof state after:
no goals
Theorem: Perron.residuePull2
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
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) =
    -1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 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
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Theorem: Perron.residuePull2
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
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
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
xpos : 0 < x
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Theorem: Perron.residuePull2
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
xpos : 0 < x
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Tactic:
have hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1}) :=
  (isHolomorphicOn xpos).mono fun s ⟨⟨⟨_, _⟩, _⟩, hs1⟩ hc ↦ hc.casesOn
    (fun hc ↦ by linarith [show s.re = 0 from congrArg _ hc]) (fun hc ↦ hs1 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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Tactic:
have := (residueAtNegOne 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 norm_num) (by norm_num))
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hε : ε > 0
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hε : ε > 0
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Tactic:
replace hε := hc (ε/2) (hεc ⟨mem_ball_iff_norm.mpr (by simp [abs_of_pos, 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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
hε :
  RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I - 1) (↑(ε / 2) + ↑(ε / 2) * I - 1) = -↑x⁻¹ ∧
    VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
      RectangleIntegral (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1)
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
hε :
  RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I - 1) (↑(ε / 2) + ↑(ε / 2) * I - 1) = -↑x⁻¹ ∧
    VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
      RectangleIntegral (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1)
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
Tactic:
rw [VerticalIntegral', ← smul_sub, hε.2, ← RectangleIntegral', neg_div, one_div, ← ofReal_inv]
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
hε :
  RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I - 1) (↑(ε / 2) + ↑(ε / 2) * I - 1) = -↑x⁻¹ ∧
    VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
      RectangleIntegral (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1)
⊢ RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1) = -↑x⁻¹
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
hε :
  RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I - 1) (↑(ε / 2) + ↑(ε / 2) * I - 1) = -↑x⁻¹ ∧
    VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
      RectangleIntegral (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1)
⊢ RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1) = -↑x⁻¹
Tactic:
exact hε.1
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
s : ℂ
x✝ : s ∈ Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1}
hc✝ : s ∈ {0, -1}
left✝ : -3 / 2 ≤ s.re
right✝¹ : s.re ≤ -1 / 2
right✝ : s ∈ im ⁻¹' univ
hs1 : s ∉ {-1}
hc : s = 0
⊢ False
Tactic:
linarith [show s.re = 0 from congrArg _ hc]
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ -3 / 2 < (-1).re ∧ (-1).re < -1 / 2
Tactic:
simpa using ⟨by linarith, by linarith⟩
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ -3 / 2 < -1
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ -1 < -1 / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ -3 / 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ -3 / 2 ≠ -1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ -1 / 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ -1 / 2 ≠ -1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.residuePull2
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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hε : ε > 0
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
⊢ ‖ε / 2 - 0‖ < ε
Tactic:
simp [abs_of_pos, hε]
Proof state after:
no goals