internlm/Lean-Github huggingface dataset:
Theorem: Perron.isIntegrable
Proof state before:
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖
Tactic:
have : (↑σ + ↑(-y) * I) = conj (↑σ + ↑y * I) := Complex.ext (by simp) (by simp)
Proof state after:
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this✝ : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
this : ↑σ + ↑(-y) * I = (starRingEnd ℂ) (↑σ + ↑y * I)
⊢ ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖
Theorem: Perron.isIntegrable
Proof state before:
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this✝ : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
this : ↑σ + ↑(-y) * I = (starRingEnd ℂ) (↑σ + ↑y * I)
⊢ ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖
Tactic:
simp_rw [this, map_conj xpos.le, Complex.norm_eq_abs, abs_conj]
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ (↑σ + ↑(-y) * I).re = ((starRingEnd ℂ) (↑σ + ↑y * I)).re
Tactic:
simp
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ (↑σ + ↑(-y) * I).im = ((starRingEnd ℂ) (↑σ + ↑y * I)).im
Tactic:
simp
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
case refine_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ IntegrableOn (fun y => 1 / y ^ 2) (Ioi 1) volume
Tactic:
refine integrableOn_Ioi_rpow_of_lt (show (-2 : ℝ) < -1 by norm_num)
  (show (0 : ℝ) < 1 by norm_num) |>.congr_fun (fun y hy ↦ ?_) measurableSet_Ioi
Proof state after:
case refine_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
hy : y ∈ Ioi 1
⊢ y ^ (-2) = 1 / y ^ 2
Theorem: Perron.isIntegrable
Proof state before:
case refine_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
hy : y ∈ Ioi 1
⊢ y ^ (-2) = 1 / y ^ 2
Tactic:
rw [rpow_neg (show (0 : ℝ) < 1 by norm_num |>.trans hy |>.le), inv_eq_one_div, rpow_two]
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ -2 < -1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
hy : y ∈ Ioi 1
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.horizontal_integral_isBigO
Proof state before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ (fun y => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑y * I) ∂μ) =O[atBot ⊔ atTop] fun y => 1 / y ^ 2
Tactic:
let g := fun ((σ, y) : ℝ × ℝ) ↦ f x (σ + y * I)
Proof state after:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
g : ℝ × ℝ → ℂ :=
  fun x_1 =>
    match x_1 with
    | (σ, y) => f x (↑σ + ↑y * I)
⊢ (fun y => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑y * I) ∂μ) =O[atBot ⊔ atTop] fun y => 1 / y ^ 2
Theorem: Perron.horizontal_integral_isBigO
Proof state before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
g : ℝ × ℝ → ℂ :=
  fun x_1 =>
    match x_1 with
    | (σ, y) => f x (↑σ + ↑y * I)
⊢ (fun y => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑y * I) ∂μ) =O[atBot ⊔ atTop] fun y => 1 / y ^ 2
Tactic:
calc
  _ =Θ[atBot ⊔ atTop] fun (y : ℝ) ↦ ∫ (σ : ℝ) in uIoc σ' σ'', g (σ, y) ∂μ :=
      isTheta_of_norm_eventuallyEq <| univ_mem'
        fun _ ↦ intervalIntegral.norm_intervalIntegral_eq _ _ _ _
  _ =O[atBot ⊔ atTop] _ :=
    (isTheta_uniformlyOn_uIoc xpos σ' σ'').isBigO.set_integral_isBigO
      measurableSet_uIoc measure_Ioc_lt_top
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Lower
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atBot (𝓝 0)
Tactic:
have hcast : (fun (y : ℝ) ↦ 1 / y ^ 2) =ᶠ[atBot] fun y ↦ (-y) ^ (-2 : ℝ) := by
  filter_upwards [Iic_mem_atBot 0] with y hy using
    by rw [rpow_neg (neg_nonneg.mpr hy), inv_eq_one_div, rpow_two, neg_sq]
Proof state after:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atBot] fun y => (-y) ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atBot (𝓝 0)
Theorem: Perron.tendsto_zero_Lower
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atBot] fun y => (-y) ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atBot (𝓝 0)
Tactic:
exact isBigO_sup.mp (horizontal_integral_isBigO xpos σ' σ'' volume)
  |>.1.trans_eventuallyEq hcast |>.trans_tendsto
  <| tendsto_rpow_neg_atTop (by norm_num) |>.comp tendsto_neg_atBot_atTop
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Lower
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ (fun y => 1 / y ^ 2) =ᶠ[atBot] fun y => (-y) ^ (-2)
Tactic:
filter_upwards [Iic_mem_atBot 0] with y hy using
  by rw [rpow_neg (neg_nonneg.mpr hy), inv_eq_one_div, rpow_two, neg_sq]
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Lower
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' y : ℝ
hy : y ∈ Iic 0
⊢ 1 / y ^ 2 = (-y) ^ (-2)
Tactic:
rw [rpow_neg (neg_nonneg.mpr hy), inv_eq_one_div, rpow_two, neg_sq]
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Lower
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atBot] fun y => (-y) ^ (-2)
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Upper
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)
Tactic:
have hcast : (fun (y : ℝ) ↦ 1 / y ^ 2) =ᶠ[atTop] fun y ↦ y ^ (-2 : ℝ) := by
  filter_upwards [Ici_mem_atTop 0] with y hy using by rw [rpow_neg hy, inv_eq_one_div, rpow_two]
Proof state after:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)
Theorem: Perron.tendsto_zero_Upper
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)
Tactic:
refine isBigO_sup.mp (horizontal_integral_isBigO xpos σ' σ'' volume)
  |>.2.trans_eventuallyEq hcast |>.trans_tendsto <| tendsto_rpow_neg_atTop (by norm_num)
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Upper
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
Tactic:
filter_upwards [Ici_mem_atTop 0] with y hy using by rw [rpow_neg hy, inv_eq_one_div, rpow_two]
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Upper
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' y : ℝ
hy : y ∈ Ici 0
⊢ 1 / y ^ 2 = y ^ (-2)
Tactic:
rw [rpow_neg hy, inv_eq_one_div, rpow_two]
Proof state after:
no goals
Theorem: Perron.tendsto_zero_Upper
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.contourPull
Proof state before:
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
Tactic:
refine verticalIntegral_eq_verticalIntegral ((isHolomorphicOn xpos).mono ?_)
  (tendsto_zero_Lower xpos σ' σ'') (tendsto_zero_Upper xpos σ' σ'')
  (isIntegrable xpos (fun h ↦ hσ0 (h ▸ left_mem_uIcc)) (fun h ↦ hσ1 (h ▸ left_mem_uIcc)))
  (isIntegrable xpos (fun h ↦ hσ0 (h ▸ right_mem_uIcc)) (fun h ↦ hσ1 (h ▸ right_mem_uIcc)))
Proof state after:
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ [[σ', σ'']] ×ℂ univ ⊆ {0, -1}ᶜ
Theorem: Perron.contourPull
Proof state before:
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ [[σ', σ'']] ×ℂ univ ⊆ {0, -1}ᶜ
Tactic:
rintro ⟨x, y⟩ ⟨hx, hy⟩ ⟨hc | hc⟩ <;> simp_all [Complex.ext_iff]
Proof state after:
no goals
Theorem: Perron.formulaLtOne
Proof 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))
Proof 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
Theorem: Perron.formulaLtOne
Proof 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⟩
Proof 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
Theorem: Perron.formulaLtOne
Proof 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
Proof 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
Theorem: Perron.formulaLtOne
Proof 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
Proof state after:
no goals
Theorem: Perron.formulaLtOne
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
σ' σ'' : ℝ
σ'pos : 0 < σ'
σ''pos : 0 < σ''
⊢ -1 < σ'
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.formulaLtOne
Proof state before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
σ' σ'' : ℝ
σ'pos : 0 < σ'
σ''pos : 0 < σ''
⊢ -1 < σ''
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.formulaLtOne
Proof 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)
Proof 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
Theorem: Perron.formulaLtOne
Proof 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⟩
Proof state after:
no goals
Theorem: Perron.formulaLtOne
Proof 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
Proof 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)
Theorem: Perron.formulaLtOne
Proof 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
Proof 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)
Theorem: Perron.formulaLtOne
Proof 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
Proof 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
Theorem: Perron.formulaLtOne
Proof 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
Proof 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
Theorem: Perron.formulaLtOne
Proof 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' _
Proof state after:
no goals
Theorem: Perron.formulaLtOne
Proof 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]
Proof 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
Theorem: Perron.formulaLtOne
Proof 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
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ UpperUIntegral f σ σ' T = 0
Tactic:
apply tendsto_nhds_unique (RectangleIntegral_tendsTo_UpperU htop hleft hright)
Proof state after:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 0)
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 0)
Tactic:
apply EventuallyEq.tendsto
Proof state after:
case hf
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) =ᶠ[atTop] fun x => 0
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
case hf
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) =ᶠ[atTop] fun x => 0
Tactic:
filter_upwards [eventually_ge_atTop T]
Proof state after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑a) = 0
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑a) = 0
Tactic:
refine fun _ hTU ↦ hf.vanishesOnRectangle fun _ ↦ ?_
Proof state after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ x✝ ∈ Rectangle (↑σ + I * ↑T) (↑σ' + I * ↑x✝¹) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ x✝ ∈ Rectangle (↑σ + I * ↑T) (↑σ' + I * ↑x✝¹) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
Tactic:
rw [mem_Rect (by simp [hσ]) (by simp [hTU])]
Proof state after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ + I * ↑T).re ≤ x✝.re ∧ x✝.re ≤ (↑σ' + I * ↑x✝¹).re ∧ (↑σ + I * ↑T).im ≤ x✝.im ∧ x✝.im ≤ (↑σ' + I * ↑x✝¹).im →
    x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ + I * ↑T).re ≤ x✝.re ∧ x✝.re ≤ (↑σ' + I * ↑x✝¹).re ∧ (↑σ + I * ↑T).im ≤ x✝.im ∧ x✝.im ≤ (↑σ' + I * ↑x✝¹).im →
    x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
Tactic:
simpa using by tauto
Proof state after:
no goals