Complex.CartanBound.intervalIntegrable_phi_dyadic_large

lemma intervalIntegrable_phi_dyadic_large {A : ℝ} (hA : (2 : ℝ) ≤ A) :    IntervalIntegrable φ volume A (2 * A) := by  have hA_le : A ≤ 2 * A := by nlinarith  have hEq : Set.EqOn (fun t : ℝ => φ t) (fun _ => (0 : ℝ)) (Set.uIoc A (2 * A)) := by    intro t ht    have htIoc : t ∈ Set.Ioc A (2 * A) := by      simpa [Set.uIoc_of_le hA_le] using ht    exact phi_eq_zero_of_two_le (le_trans hA (le_of_lt htIoc.1))  have hz : IntervalIntegrable (fun _ : ℝ => (0 : ℝ)) volume A (2 * A) :=    intervalIntegrable_const  exact (IntervalIntegrable.congr (a := A) (b := (2 * A))    (μ := (volume : MeasureTheory.Measure ℝ))    (f := fun _ => (0 : ℝ)) (g := fun t => φ t) (by      intro t ht      simpa using (hEq (x := t) ht).symm)) hz