refine integral_mono (Integrable.one_div_const_add_sq c₂ c₂_pos) ?_ hlower
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ ∫ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ Integrable (fun t => 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))) volume