Complex.CartanBound.integral_sqrt_two_div_abs_one_sub_le_K_dyadic_middle

lemma integral_sqrt_two_div_abs_one_sub_le_K_dyadic_middle {A : ℝ}    (hA_lower : (1 / 4 : ℝ) ≤ A) (hA_upper : A ≤ (2 : ℝ)) :    (∫ (t : ℝ) in A..(2 * A), Real.sqrt (2 / |1 - t|) ∂volume) ≤ K := by  let s (t : ℝ) : ℝ := Real.sqrt (2 / |1 - t|)  have hA_le : A ≤ 2 * A := by nlinarith [hA_lower]  have hA_upper' : (2 * A : ℝ) ≤ 4 := by nlinarith [hA_upper]  have hsqrt_big : IntervalIntegrable s volume (1 / 4 : ℝ) (4 : ℝ) := by    simpa [s] using intervalIntegrable_sqrt_two_div_abs_one_sub_Icc  have hle_K :      (∫ (t : ℝ) in A..(2 * A), s t ∂volume)        ≤ ∫ (t : ℝ) in (1 / 4 : ℝ)..(4 : ℝ), s t ∂volume := by    refine intervalIntegral.integral_mono_interval (μ := (volume : MeasureTheory.Measure ℝ))      (c := (1 / 4 : ℝ)) (d := (4 : ℝ)) (a := A) (b := (2 * A))      hA_lower hA_le hA_upper' ?_ hsqrt_big    exact Filter.Eventually.of_forall (fun _t => Real.sqrt_nonneg _)  simpa [K, s] using hle_K