Complex.CartanBound.integral_phi_div_le_Cφ_mul

lemma integral_phi_div_le_Cφ_mul {a R : ℝ} (ha : 0 < a) (hR : 0 ≤ R) :    (∫ (r : ℝ) in R..(2 * R), φ (r / a) ∂volume) ≤ Cφ * R := by  have ha0 : a ≠ 0 := ne_of_gt ha  have hrew :      (∫ (r : ℝ) in R..(2 * R), φ (r / a) ∂volume)        = a * (∫ (t : ℝ) in (R / a)..(2 * R / a), φ t ∂volume) := by    simp [smul_eq_mul, mul_left_comm, mul_comm, div_eq_mul_inv, ha0]  rw [hrew]  have hA : 0 ≤ R / a := by    exact div_nonneg hR ha.le  have hle : (∫ (t : ℝ) in (R / a)..(2 * (R / a)), φ t ∂volume) ≤ Cφ * (R / a) :=    integral_phi_le_Cφ_mul (A := R / a) hA  have hEq : (2 * R / a) = 2 * (R / a) := by ring  have hle' :      (∫ (t : ℝ) in (R / a)..(2 * R / a), φ t ∂volume) ≤ Cφ * (R / a) := by    simpa [hEq] using hle  have ha_nonneg : 0 ≤ a := ha.le  have := mul_le_mul_of_nonneg_left hle' ha_nonneg  have hRHS : a * (Cφ * (R / a)) = Cφ * R := by    field_simp [ha0]  simpa [hRHS, mul_assoc, mul_left_comm, mul_comm] using this