Complex.CartanBound.intervalIntegrable_phi_dyadic_small

lemma intervalIntegrable_phi_dyadic_small {A : ℝ} (hA0 : 0 ≤ A)    (hA : A ≤ (1 / 4 : ℝ)) :    IntervalIntegrable φ volume A (2 * A) := by  have hA_le : A ≤ 2 * A := by nlinarith  have hconst : IntervalIntegrable (fun _ : ℝ => (Real.log 2 : ℝ)) volume A (2 * A) :=    intervalIntegrable_const  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 _ => ‖(Real.log 2 : ℝ)‖ := by    refine ae_restrict_norm_phi_le_of_forall_mem (A := A) (B := 2 * A) hA_le      (g := fun _ => (Real.log 2 : ℝ)) (hg := fun _ => ?_) ?_    · simpa using (Real.log_nonneg (by norm_num : (1 : ℝ) ≤ 2))    · intro t ht      exact phi_le_log_two_on_dyadic_of_le_quarter hA ht  exact IntervalIntegrable.mono_fun hconst hmeas hdom