Complex.CartanBound.integral_sum_mul_phi_div_le_Cφ_mul_sum

lemma integral_sum_mul_phi_div_le_Cφ_mul_sum    {ι : Type} (s : Finset ι) (w : ι → ℝ) (a : ι → ℝ)    (hw : ∀ i ∈ s, 0 ≤ w i) (ha : ∀ i ∈ s, 0 < a i) {R : ℝ} (hR : 0 ≤ R) :    (∫ r in R..(2 * R), (∑ i ∈ s, fun r : ℝ => w i * φ (r / a i)) r ∂volume)      ≤ Cφ * (∑ i ∈ s, w i) * R := by  have hint : ∀ i ∈ s, IntervalIntegrable (fun r : ℝ => w i * φ (r / a i))      volume R (2 * R) := by    intro i hi    have hφi : IntervalIntegrable (fun r : ℝ => φ (r / a i)) volume R (2 * R) :=      intervalIntegrable_phi_div (a := a i) (R := R) (ha i hi) hR    simpa [mul_assoc] using hφi.const_mul (w i)  have hsum_int :      (∫ r in R..(2 * R), (∑ i ∈ s, fun r : ℝ => w i * φ (r / a i)) r ∂volume)        = ∑ i ∈ s, ∫ r in R..(2 * R), (fun r : ℝ => w i * φ (r / a i)) r            ∂volume := by    simpa using      (intervalIntegral.integral_finsetSum (μ := volume) (a := R) (b := 2 * R)        (s := s) (f := fun i : ι => fun r : ℝ => w i * φ (r / a i)) hint)  rw [hsum_int]  have hsum_le :      (∑ i ∈ s, ∫ r in R..(2 * R), (fun r : ℝ => w i * φ (r / a i)) r ∂volume)        ≤ ∑ i ∈ s, w i * (Cφ * R) := by    refine Finset.sum_le_sum ?_    intro i hi    have hphi :        (∫ r in R..(2 * R), φ (r / a i) ∂volume) ≤ Cφ * R :=      integral_phi_div_le_Cφ_mul (a := a i) (R := R) (ha i hi) hR    have := mul_le_mul_of_nonneg_left hphi (hw i hi)    simpa [mul_assoc, mul_left_comm, mul_comm] using this  refine le_trans hsum_le ?_  have : (∑ i ∈ s, w i * (Cφ * R)) = Cφ * (∑ i ∈ s, w i) * R := by    calc      (∑ i ∈ s, w i * (Cφ * R)) = (∑ i ∈ s, w i) * (Cφ * R) := by        simp [Finset.sum_mul]      _ = Cφ * (∑ i ∈ s, w i) * R := by        ac_rfl  exact le_of_eq this