Theorem: Perron.formulaLtOne (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
⊢ VerticalIntegral (f x) σ = 0
Tactic:
have h_contourPull (σ' σ'' : ℝ) (σ'pos : 0 < σ') (σ''pos : 0 < σ'') :
    VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ'' :=
  contourPull xpos (not_mem_uIcc_of_lt σ'pos σ''pos)
    (not_mem_uIcc_of_lt (by linarith) (by linarith))
State after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
⊢ VerticalIntegral (f x) σ = 0

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
⊢ VerticalIntegral (f x) σ = 0
Tactic:
have VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x^σ' * C := by
  let C := ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt)
  exact ⟨C, integralPosAux, fun _ ↦ vertIntBound xpos⟩
State after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
⊢ VerticalIntegral (f x) σ = 0

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
⊢ VerticalIntegral (f x) σ = 0
Tactic:
have VertIntTendsto : Tendsto (VerticalIntegral (f x)) atTop (𝓝 0) :=
  tendsto_zero_iff_norm_tendsto_zero.mpr AbsVertIntTendsto
State after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
VertIntTendsto : Tendsto (VerticalIntegral (f x)) atTop (𝓝 0)
⊢ VerticalIntegral (f x) σ = 0

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
VertIntTendsto : Tendsto (VerticalIntegral (f x)) atTop (𝓝 0)
⊢ VerticalIntegral (f x) σ = 0
Tactic:
exact limitOfConstant σ_pos h_contourPull VertIntTendsto
State after:
no goals

State before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
σ' σ'' : ℝ
σ'pos : 0 < σ'
σ''pos : 0 < σ''
⊢ -1 < σ'
Tactic:
linarith
State after:
no goals

State before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
σ' σ'' : ℝ
σ'pos : 0 < σ'
σ''pos : 0 < σ''
⊢ -1 < σ''
Tactic:
linarith
State after:
no goals

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
⊢ ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
Tactic:
let C := ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt)
State after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ := ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
⊢ ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ := ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
⊢ ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
Tactic:
exact ⟨C, integralPosAux, fun _ ↦ vertIntBound xpos⟩
State after:
no goals

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
Tactic:
obtain ⟨C, _, hC⟩ := VertIntBound
State after:
case intro.intro
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)

State before:
case intro.intro
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
Tactic:
have := tendsto_rpow_atTop_nhds_zero_of_norm_lt_one xpos x_lt_one C
State after:
case intro.intro
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)

State before:
case intro.intro
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds this
State after:
case intro.intro.hgf
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atTop, 0 ≤ (⇑Complex.abs ∘ VerticalIntegral (f x)) b

case intro.intro.hfh
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atTop, (⇑Complex.abs ∘ VerticalIntegral (f x)) b ≤ x ^ b * C

State before:
case intro.intro.hgf
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atTop, 0 ≤ (⇑Complex.abs ∘ VerticalIntegral (f x)) b
Tactic:
filter_upwards
State after:
case intro.intro.hgf.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ (a : ℝ), 0 ≤ (⇑Complex.abs ∘ VerticalIntegral (f x)) a

State before:
case intro.intro.hgf.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ (a : ℝ), 0 ≤ (⇑Complex.abs ∘ VerticalIntegral (f x)) a
Tactic:
exact fun _ ↦ Complex.abs.nonneg' _
State after:
no goals

State before:
case intro.intro.hfh
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atTop, (⇑Complex.abs ∘ VerticalIntegral (f x)) b ≤ x ^ b * C
Tactic:
filter_upwards [eventually_gt_atTop 1]
State after:
case h
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ (a : ℝ), 1 < a → (⇑Complex.abs ∘ VerticalIntegral (f x)) a ≤ x ^ a * C

State before:
case h
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ ∀ (a : ℝ), 1 < a → (⇑Complex.abs ∘ VerticalIntegral (f x)) a ≤ x ^ a * C
Tactic:
exact hC
State after:
no goals