Theorem: Perron.residuePull1 (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_gt_one : 1 < x
σ_pos : 0 < σ
⊢ VerticalIntegral' (f x) σ = 1 + VerticalIntegral' (f x) (-1 / 2)
Tactic:
apply eq_add_of_sub_eq
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

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
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

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])
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

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))
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

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
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

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
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

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ε⟩)
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

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]
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_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]
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_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⟩
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ -1 / 2 < 0
Tactic:
linarith
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ 0 < σ
Tactic:
linarith
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ -1 / 2 ≠ 0
Tactic:
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ -1 / 2 ≠ -1
Tactic:
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ σ ≠ 0
Tactic:
linarith
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_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-1 / 2) σ ×ℂ univ \ {0})
⊢ σ ≠ -1
Tactic:
linarith
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_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ε]
State after:
no goals