internlm/Lean-Github huggingface dataset:
Theorem: Perron.vertIntBound
Proof state before:
case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
conv => rhs; rhs; intro a; rhs
Proof state after:
case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (a : ℝ), 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (a : ℝ), 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
apply integral_mono hint
Proof state after:
case pos.hg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ Integrable (fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))) volume

case pos.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) ≤ fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case pos.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) ≤ fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
rw [Pi.le_def]
Proof state after:
case pos.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∀ (i : ℝ), 1 / (‖↑σ + ↑i * I‖ * ‖↑σ + ↑i * I + 1‖) ≤ 1 / (√(1 + i ^ 2) * √(2 + i ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case pos.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∀ (i : ℝ), 1 / (‖↑σ + ↑i * I‖ * ‖↑σ + ↑i * I + 1‖) ≤ 1 / (√(1 + i ^ 2) * √(2 + i ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
intro t
Proof state after:
case pos.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case pos.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
gcongr <;> apply sqrt_le_sqrt
Proof state after:
case pos.h.h.h₁.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 + t ^ 2 ≤ normSq (↑σ + ↑t * I)

case pos.h.h.h₂.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 2 + t ^ 2 ≤ normSq (↑σ + ↑t * I + 1)

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Theorem: Perron.vertIntBound
Proof state before:
case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
rfl
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
case calc_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ‖VerticalIntegral (f x) σ‖ = ‖∫ (t : ℝ), ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖
Tactic:
simp [VerticalIntegral]
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
case calc_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ =
    ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖
Tactic:
simp [Complex.abs_cpow_eq_rpow_re_of_pos xpos]
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
case calc_3
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖ = x ^ σ * ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖)
Tactic:
simp [integral_mul_left, div_eq_mul_inv]
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 0 t ≤ 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
positivity
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
case pos.hg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ Integrable (fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))) volume
Tactic:
have := integralPosAux
Proof state after:
case pos.hg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : 0 < ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
⊢ Integrable (fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))) volume
Theorem: Perron.vertIntBound
Proof state before:
case pos.hg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : 0 < ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
⊢ Integrable (fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))) volume
Tactic:
contrapose! this
Proof state after:
case pos.hg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : ¬Integrable (fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))) volume
⊢ ∫ (a : ℝ), 1 / (√(1 + a ^ 2) * √(2 + a ^ 2)) ≤ 0
Theorem: Perron.vertIntBound
Proof state before:
case pos.hg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : ¬Integrable (fun a => 1 / (√(1 + a ^ 2) * √(2 + a ^ 2))) volume
⊢ ∫ (a : ℝ), 1 / (√(1 + a ^ 2) * √(2 + a ^ 2)) ≤ 0
Tactic:
simp_rw [integral_undef this, le_rfl]
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
case pos.h.h.h₁.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 + t ^ 2 ≤ normSq (↑σ + ↑t * I)
Tactic:
simp_rw [normSq_add_mul_I, add_le_add_iff_right, one_le_pow_of_one_le σ_gt_one.le _]
Proof state after:
no goals
Theorem: Perron.vertIntBound
Proof state before:
case pos.h.h.h₂.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 2 + t ^ 2 ≤ normSq (↑σ + ↑t * I + 1)
Tactic:
rw [add_right_comm, ← ofReal_one, ← ofReal_add, normSq_add_mul_I, add_le_add_iff_right]
Proof state after:
case pos.h.h.h₂.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 2 ≤ (σ + 1) ^ 2
Theorem: Perron.vertIntBound
Proof state before:
case pos.h.h.h₂.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 2 ≤ (σ + 1) ^ 2
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ ∃ C, ∀ σ < -3 / 2, ‖VerticalIntegral' (f x) σ‖ ≤ C * x ^ σ
Tactic:
use 1 / (2 * π) *  ‖(∫ (t : ℝ), 1 / ((4⁻¹ + t ^ 2).sqrt * (4⁻¹ + t ^ 2).sqrt : ℂ))‖
Proof state after:
case h
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ ∀ σ < -3 / 2, ‖VerticalIntegral' (f x) σ‖ ≤ 1 / (2 * π) * ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h
x σ σ' σ'' T : ℝ
xpos : 0 < x
⊢ ∀ σ < -3 / 2, ‖VerticalIntegral' (f x) σ‖ ≤ 1 / (2 * π) * ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Tactic:
intro σ hσ
Proof state after:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral' (f x) σ‖ ≤ 1 / (2 * π) * ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral' (f x) σ‖ ≤ 1 / (2 * π) * ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Tactic:
simp only [VerticalIntegral', abs_of_pos Real.pi_pos, smul_eq_mul, norm_mul, f]
Proof state after:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖1 / (2 * ↑π * I)‖ * ‖VerticalIntegral (f x) σ‖ ≤
    1 / (2 * π) * ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖1 / (2 * ↑π * I)‖ * ‖VerticalIntegral (f x) σ‖ ≤
    1 / (2 * π) * ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Tactic:
rw [(by simp [pi_nonneg] : ‖1 / (2 * ↑π * I)‖ = 1 / (2 * π)), mul_assoc]
Proof state after:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ 1 / (2 * π) * ‖VerticalIntegral (f x) σ‖ ≤
    1 / (2 * π) * (‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ)
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ 1 / (2 * π) * ‖VerticalIntegral (f x) σ‖ ≤
    1 / (2 * π) * (‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ)
Tactic:
apply (mul_le_mul_left (by simp [pi_pos])).mpr
Proof state after:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral (f x) σ‖ ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral (f x) σ‖ ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Tactic:
calc
  _ = ‖∫ (t : ℝ), x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ := ?_
  _ ≤ ∫ (t : ℝ), ‖x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ := norm_integral_le_integral_norm _
  _ = ∫ (t : ℝ), x ^ σ / ‖((σ + t * I) * (σ + t * I + 1))‖ := ?_
  _ = x ^ σ * ∫ (t : ℝ), 1 / (‖σ + t * I‖ * ‖σ + t * I + 1‖) := ?_
  _ ≤ x ^ σ * ∫ (t : ℝ), 1 / ((4⁻¹ + t ^ 2).sqrt * (4⁻¹ + t ^ 2).sqrt) := ?_
  _ ≤ _ := ?_
Proof state after:
case h.calc_1
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral (f x) σ‖ = ‖∫ (t : ℝ), ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖

case h.calc_2
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ =
    ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖

case h.calc_3
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖ = x ^ σ * ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖)

case h.calc_4
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ x ^ σ * ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))

case h.calc_5
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤
    ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖1 / (2 * ↑π * I)‖ = 1 / (2 * π)
Tactic:
simp [pi_nonneg]
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ 0 < 1 / (2 * π)
Tactic:
simp [pi_pos]
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_1
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral (f x) σ‖ = ‖∫ (t : ℝ), ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖
Tactic:
simp [VerticalIntegral, Real.pi_nonneg]
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_2
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ =
    ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖
Tactic:
congr with t
Proof state after:
case h.calc_2.e_f.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
t : ℝ
⊢ ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ = x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_2.e_f.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
t : ℝ
⊢ ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ = x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖
Tactic:
rw [norm_div, Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos xpos, add_re, ofReal_re,
  re_ofReal_mul, I_re, mul_zero, add_zero]
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_3
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖ = x ^ σ * ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖)
Tactic:
simp_rw [div_eq_mul_inv, integral_mul_left, one_mul, Complex.norm_eq_abs, map_mul]
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_4
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ x ^ σ * ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
gcongr
Proof state after:
case h.calc_4.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_4.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
by_cases hint : Integrable fun (a : ℝ) ↦ 1 / (‖σ + ↑a * I‖ * ‖σ + ↑a * I + 1‖)
Proof state after:
case pos
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))

case neg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))

case neg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
swap
Proof state after:
case neg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))

case pos
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
apply integral_mono hint
Proof state after:
case pos.hg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ Integrable (fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))) volume

case pos.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) ≤ fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) ≤ fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))
Tactic:
rw [Pi.le_def]
Proof state after:
case pos.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∀ (i : ℝ), 1 / (‖↑σ + ↑i * I‖ * ‖↑σ + ↑i * I + 1‖) ≤ 1 / (√(4⁻¹ + i ^ 2) * √(4⁻¹ + i ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∀ (i : ℝ), 1 / (‖↑σ + ↑i * I‖ * ‖↑σ + ↑i * I + 1‖) ≤ 1 / (√(4⁻¹ + i ^ 2) * √(4⁻¹ + i ^ 2))
Tactic:
intro t
Proof state after:
case pos.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
gcongr <;> apply sqrt_le_sqrt
Proof state after:
case pos.h.h.h₁.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ + t ^ 2 ≤ normSq (↑σ + ↑t * I)

case pos.h.h.h₂.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ + t ^ 2 ≤ normSq (↑σ + ↑t * I + 1)
Theorem: Perron.vertIntBoundLeft
Proof state before:
case neg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
rw [integral_undef hint]
Proof state after:
case neg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case neg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
exact integral_nonneg <| fun t ↦ by simp only [Pi.le_def, Pi.zero_apply]; positivity
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 0 t ≤ 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
simp only [Pi.le_def, Pi.zero_apply]
Proof state after:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 0 ≤ 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 0 ≤ 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
positivity
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.hg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ Integrable (fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))) volume
Tactic:
have := integralPosAux' (4⁻¹) (4⁻¹) (by norm_num) (by norm_num)
Proof state after:
case pos.hg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : 0 < ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Integrable (fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))) volume
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.hg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : 0 < ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Integrable (fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))) volume
Tactic:
contrapose! this
Proof state after:
case pos.hg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : ¬Integrable (fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))) volume
⊢ ∫ (a : ℝ), 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2)) ≤ 0
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.hg
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
this : ¬Integrable (fun a => 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2))) volume
⊢ ∫ (a : ℝ), 1 / (√(4⁻¹ + a ^ 2) * √(4⁻¹ + a ^ 2)) ≤ 0
Tactic:
simp_rw [integral_undef this, le_rfl]
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ 0 < 4⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h.h.h₁.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ + t ^ 2 ≤ normSq (↑σ + ↑t * I)
Tactic:
rw [normSq_add_mul_I, add_le_add_iff_right]
Proof state after:
case pos.h.h.h₁.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ ≤ σ ^ 2
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h.h.h₁.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ ≤ σ ^ 2
Tactic:
ring_nf
Proof state after:
case pos.h.h.h₁.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / 4 ≤ σ ^ 2
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h.h.h₁.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / 4 ≤ σ ^ 2
Tactic:
nlinarith
Proof state after:
no goals