Perron.integralPosAux'_of_le

lemma integralPosAux'_of_le (c₁ c₂ : ℝ) (c₁_pos : 0 < c₁) (hle : c₁ ≤ c₂) :    0 < ∫ (t : ℝ), 1 / ((c₁ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt) := by  have c₂_pos : 0 < c₂ := by linarith  have hlower (t : ℝ) :      1 / (c₂ + t ^ 2) ≤ 1 / ((c₁ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt) := by    gcongr    calc      _ ≤ (c₂ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt := by gcongr      _ ≤ c₂ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity  have hupper (t : ℝ) :      1 / ((c₁ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt) ≤ 1 / (c₁ + t ^ 2) := by      gcongr      calc        _ ≥ (c₁ + t ^ 2).sqrt * (c₁ + t ^ 2).sqrt := by gcongr        _ ≥ c₁ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity  calc 0 < ∫ t, 1 / (c₂ + t^2) := integral_one_div_const_add_sq_pos c₂ c₂_pos       _ ≤ ∫ t, 1 / (Real.sqrt (c₁ + t^2) * Real.sqrt (c₂ + t^2)) := ?_  refine integral_mono (Integrable.one_div_const_add_sq c₂ c₂_pos) ?_ hlower  apply MeasureTheory.Integrable.mono (g := fun t : ℝ ↦ 1 / (c₁ + t ^ 2))    <| Integrable.one_div_const_add_sq c₁ c₁_pos  · refine (measurable_const.div <| Measurable.mul ?_ ?_).aestronglyMeasurable <;>      exact (measurable_const.add <| measurable_id'.pow_const 2).sqrt  · refine ae_of_all _ (fun x ↦ ?_)    repeat rewrite [norm_of_nonneg (by positivity)]    exact hupper x