Complex.CartanBound.integral_phi_le_Cφ_mul_large

lemma integral_phi_le_Cφ_mul_large {A : ℝ} (hA : (2 : ℝ) ≤ A) :    (∫ (t : ℝ) in A..(2 * A), φ t ∂volume) ≤ Cφ * A := by  have hA_le : A ≤ 2 * A := by nlinarith  have hφ0 : Set.EqOn (fun t : ℝ => φ t) (fun _ => (0 : ℝ)) (Set.uIcc A (2 * A)) := by    intro t ht    have ht' : t ∈ Set.Icc A (2 * A) := by      simpa [Set.uIcc_of_le hA_le] using ht    exact phi_eq_zero_of_two_le (le_trans hA ht'.1)  have hzero : (∫ (t : ℝ) in A..(2 * A), φ t ∂volume) = 0 := by    simpa using intervalIntegral.integral_congr (μ := (volume : MeasureTheory.Measure ℝ)) hφ0  have hnonneg : (0 : ℝ) ≤ Cφ * A := mul_nonneg (le_of_lt Cφ_pos) (by linarith)  simpa [hzero] using hnonneg