Complex.CartanBound.intervalIntegrable_phi_dyadic_middle

lemma intervalIntegrable_phi_dyadic_middle {A : ℝ}    (hA_lower : (1 / 4 : ℝ) ≤ A) (hA_upper : A ≤ (2 : ℝ)) :    IntervalIntegrable φ volume A (2 * A) := by  have hA_le : A ≤ 2 * A := by nlinarith [hA_lower]  have hsqrt :      IntervalIntegrable (fun t : ℝ => Real.sqrt (2 / |1 - t|)) volume A (2 * A) :=    intervalIntegrable_sqrt_two_div_abs_one_sub_dyadic_middle hA_lower hA_upper  have hmeas :      AEStronglyMeasurable (fun t : ℝ => φ t) (volume.restrict (Set.uIoc A (2 * A))) :=    (measurable_phi.aestronglyMeasurable : _)  have hdom :      (fun t : ℝ => ‖φ t‖) ≤ᶠ[ae (volume.restrict (Set.uIoc A (2 * A)))]        fun t => ‖Real.sqrt (2 / |1 - t|)‖ := by    refine ae_restrict_norm_phi_le_of_forall_mem (A := A) (B := 2 * A) hA_le      (g := fun t => Real.sqrt (2 / |1 - t|)) (hg := fun _ => Real.sqrt_nonneg _) ?_    intro t _ht    exact φ_le_sqrt t  exact IntervalIntegrable.mono_fun hsqrt hmeas hdom