Complex.CartanBound.integral_phi_le_Cφ_mul_middle

lemma integral_phi_le_Cφ_mul_middle {A : ℝ}    (hA_lower : (1 / 4 : ℝ) ≤ A) (hA_upper : A ≤ (2 : ℝ)) :    (∫ (t : ℝ) in A..(2 * A), φ t ∂volume) ≤ Cφ * A := by  let s (t : ℝ) : ℝ := Real.sqrt (2 / |1 - t|)  have hA_le : A ≤ 2 * A := by nlinarith [hA_lower]  have hφ_int : IntervalIntegrable φ volume A (2 * A) :=    intervalIntegrable_phi_dyadic_middle hA_lower hA_upper  have hsqrt : IntervalIntegrable s volume A (2 * A) := by    simpa [s] using      intervalIntegrable_sqrt_two_div_abs_one_sub_dyadic_middle hA_lower hA_upper  have hle_int :      (∫ (t : ℝ) in A..(2 * A), φ t ∂volume)        ≤ ∫ (t : ℝ) in A..(2 * A), s t ∂volume := by    refine intervalIntegral.integral_mono_on      (μ := (volume : MeasureTheory.Measure ℝ)) hA_le hφ_int hsqrt ?_    intro t _ht    exact φ_le_sqrt t  have hsqrt_le : (∫ (t : ℝ) in A..(2 * A), s t ∂volume) ≤ (4 * K + 1) * A := by    have hK : (∫ (t : ℝ) in A..(2 * A), s t ∂volume) ≤ K := by      simpa [s] using integral_sqrt_two_div_abs_one_sub_le_K_dyadic_middle hA_lower hA_upper    exact le_trans hK (K_le_four_mul_K_add_one_mul_of_quarter_le hA_lower)  have hcoef : (4 * K + 1 : ℝ) * A ≤ Cφ * A :=    mul_le_mul_of_nonneg_right four_mul_K_add_one_le_Cφ (by nlinarith [hA_lower])  exact le_trans hle_int (le_trans hsqrt_le hcoef)