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

State before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ‖VerticalIntegral (f x) σ‖ ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
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 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt) :=
      mul_le_mul_of_nonneg_left ?_ (rpow_nonneg xpos.le _)
State after:
case calc_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ‖VerticalIntegral (f x) σ‖ = ‖∫ (t : ℝ), ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖

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

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

case calc_4
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (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))

State before:
case calc_4
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (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:
by_cases hint : Integrable fun (a : ℝ) ↦ 1 / (‖σ + a * I‖ * ‖σ + a * I + 1‖)
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‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

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

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 neg
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:
swap
State after:
case neg
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 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))

State before:
case neg
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 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:
rw [integral_undef hint]
State after:
case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

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

State before:
case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

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:
exact integral_nonneg <| fun t ↦ by positivity
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‖) ≤ ∫ (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))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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