Complex.CartanBound.integral_phi_le_Cφ_mul_small

lemma integral_phi_le_Cφ_mul_small {A : ℝ} (hA0 : 0 ≤ A) (hA : A ≤ (1 / 4 : ℝ)) :    (∫ (t : ℝ) in A..(2 * A), φ t ∂volume) ≤ Cφ * A := by  have hA_le : A ≤ 2 * A := by nlinarith  have hφ_int : IntervalIntegrable φ volume A (2 * A) :=    intervalIntegrable_phi_dyadic_small hA0 hA  have hconst : IntervalIntegrable (fun _ : ℝ => (Real.log 2 : ℝ)) volume A (2 * A) :=    intervalIntegrable_const  have hle_int :      (∫ (t : ℝ) in A..(2 * A), φ t ∂volume)        ≤ ∫ (t : ℝ) in A..(2 * A), (Real.log 2 : ℝ) ∂volume := by    refine intervalIntegral.integral_mono_on (μ := (volume : MeasureTheory.Measure ℝ))      hA_le hφ_int hconst ?_    intro t ht    exact phi_le_log_two_on_dyadic_of_le_quarter hA ht  have hRHS :      (∫ (t : ℝ) in A..(2 * A), (Real.log 2 : ℝ) ∂volume) = A * Real.log 2 := by    simp [intervalIntegral.integral_const, sub_eq_add_neg, add_assoc, two_mul]  have hcoef : A * Real.log 2 ≤ Cφ * A := by    have := mul_le_mul_of_nonneg_left log_two_le_Cφ hA0    simpa [mul_assoc, mul_left_comm, mul_comm] using this  exact le_trans (by simpa [hRHS] using hle_int) hcoef