Theorem: Perron.integralPosAux' (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
by_cases hc : c₁ ≤ c₂
State after:
case pos
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))

case neg
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))

State before:
case pos
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
exact integralPosAux'_of_le c₁ c₂ c₁_pos hc
State after:
no goals

State before:
case neg
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
Tactic:
convert integralPosAux'_of_le c₂ c₁ c₂_pos (by linarith) using 4
State after:
case h.e'_4.h.e'_7.h.h.e'_6
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
x✝ : ℝ
⊢ √(c₁ + x✝ ^ 2) * √(c₂ + x✝ ^ 2) = √(c₂ + x✝ ^ 2) * √(c₁ + x✝ ^ 2)

State before:
case h.e'_4.h.e'_7.h.h.e'_6
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
x✝ : ℝ
⊢ √(c₁ + x✝ ^ 2) * √(c₂ + x✝ ^ 2) = √(c₂ + x✝ ^ 2) * √(c₁ + x✝ ^ 2)
Tactic:
rw [mul_comm]
State after:
no goals

State before:
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
c₂_pos : 0 < c₂
hc : ¬c₁ ≤ c₂
⊢ c₂ ≤ c₁
Tactic:
linarith
State after:
no goals