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

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume
Tactic:
have : Continuous (fun (y : ℝ) ↦ f x (σ + y * I)) := by
  refine (isHolomorphicOn xpos).continuousOn.comp_continuous (by continuity) fun x ↦ not_or.mpr ?_
  simp [Complex.ext_iff, σ_ne_zero, σ_ne_neg_one]
State after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume
Tactic:
refine this.locallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
  (univ_mem' fun y ↦ ?_) (isTheta xpos).2.isBigO ⟨Ioi 1, Ioi_mem_atTop 1, ?_⟩
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 : ℝ
⊢ y ∈
    {x_1 |
      (fun x_2 =>
          (Norm.norm ∘ fun y => f x (↑σ + ↑y * I)) x_2 = (Norm.norm ∘ (fun y => f x (↑σ + ↑y * I)) ∘ Neg.neg) x_2)
        x_1}

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

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
⊢ Continuous fun y => f x (↑σ + ↑y * I)
Tactic:
refine (isHolomorphicOn xpos).continuousOn.comp_continuous (by continuity) fun x ↦ not_or.mpr ?_
State after:
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
x : ℝ
⊢ ¬↑σ + ↑x * I = 0 ∧ ↑σ + ↑x * I ∉ {-1}

State before:
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
x : ℝ
⊢ ¬↑σ + ↑x * I = 0 ∧ ↑σ + ↑x * I ∉ {-1}
Tactic:
simp [Complex.ext_iff, σ_ne_zero, σ_ne_neg_one]
State after:
no goals

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
⊢ Continuous fun y => ↑σ + ↑y * I
Tactic:
continuity
State after:
no goals

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 : ℝ
⊢ y ∈
    {x_1 |
      (fun x_2 =>
          (Norm.norm ∘ fun y => f x (↑σ + ↑y * I)) x_2 = (Norm.norm ∘ (fun y => f x (↑σ + ↑y * I)) ∘ Neg.neg) x_2)
        x_1}
Tactic:
show ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖
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 : ℝ
⊢ ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖

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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals