Complex.CartanBound.intervalIntegrable_phi_div

lemma intervalIntegrable_phi_div {a R : ℝ} (ha : 0 < a) (hR : 0 ≤ R) :    IntervalIntegrable (fun r : ℝ => φ (r / a)) volume R (2 * R) := by  have ha0 : a ≠ 0 := ne_of_gt ha  have hRa_nonneg : 0 ≤ R / a := by    exact div_nonneg hR (le_of_lt ha)  have hφ : IntervalIntegrable φ volume (R / a) (2 * (R / a)) :=    intervalIntegrable_phi_dyadic (A := (R / a)) hRa_nonneg  have := (hφ.comp_mul_right (c := (a⁻¹ : ℝ)))  have hupper : a * (R * (a⁻¹ * 2)) = (2 * R) := by    field_simp [ha0]  simpa [div_eq_mul_inv, ha0, hupper, mul_assoc, mul_left_comm, mul_comm] using this