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

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 : ℂ))‖
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 ^ σ

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

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]
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 ^ σ

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

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
State after:
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral (f x) σ‖ ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ

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) := ?_
  _ ≤ _ := ?_
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 ^ σ

State before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖1 / (2 * ↑π * I)‖ = 1 / (2 * π)
Tactic:
simp [pi_nonneg]
State after:
no goals

State before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ 0 < 1 / (2 * π)
Tactic:
simp [pi_pos]
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 + 1)
Tactic:
rw [(by push_cast; ring : σ + t * I + 1 = ofReal' (σ + 1) + t * I),
  normSq_add_mul_I, add_le_add_iff_right]
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⁻¹ ≤ (σ + 1) ^ 2

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⁻¹ ≤ (σ + 1) ^ 2
Tactic:
ring_nf
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 ≤ 1 + σ * 2 + σ ^ 2

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 ≤ 1 + σ * 2 + σ ^ 2
Tactic:
nlinarith
State after:
no goals

State before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ ↑σ + ↑t * I + 1 = ↑(σ + 1) + ↑t * I
Tactic:
push_cast
State after:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ ↑σ + ↑t * I + 1 = ↑σ + 1 + ↑t * I

State before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ ↑σ + ↑t * I + 1 = ↑σ + 1 + ↑t * I
Tactic:
ring
State after:
no goals

State before:
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 ^ σ
Tactic:
rw [mul_comm]
State after:
case h.calc_5
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ (∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) * x ^ σ ≤
    ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ

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

State before:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
have : 0 ≤ ∫ (t : ℝ), 1 / (sqrt (4⁻¹ + t ^ 2) * sqrt (4⁻¹ + t ^ 2)) := by positivity
State after:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖

State before:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
rw [← _root_.abs_of_nonneg this, ← Complex.abs_ofReal]
State after:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖

State before:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
apply le_of_eq
State after:
case h.calc_5.h.a
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖

State before:
case h.calc_5.h.a
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
congr
State after:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))

State before:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))
Tactic:
norm_cast
State after:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), ↑(1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)))

State before:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), ↑(1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)))
Tactic:
exact integral_ofReal.symm
State after:
no goals

State before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
positivity
State after:
no goals