Source indexedlemma · leanprover/lean4:v4.32.0

Complex.CartanBound.integral_phi_le_Cφ_mul

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:570 to 583

Mathematical statement

Exact Lean statement

lemma integral_phi_le_Cφ_mul {A : ℝ} (hA : 0 ≤ A) :
    (∫ (t : ℝ) in A..(2 * A), φ t ∂volume) ≤ Cφ * A

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_phi_le_Cφ_mul {A : ℝ} (hA : 0 ≤ A) :    (∫ (t : ℝ) in A..(2 * A), φ t ∂volume) ≤ Cφ * A := by  by_cases hA0 : A = 0  · subst hA0    simp [Cφ, φ, K]  cases le_total A (1 / 4 : ℝ) with  | inl hsmall =>      exact integral_phi_le_Cφ_mul_small hA hsmall  | inr hge_quarter =>      cases le_total (2 : ℝ) A with      | inl hbig =>          exact integral_phi_le_Cφ_mul_large hbig      | inr hA_le_two =>          exact integral_phi_le_Cφ_mul_middle hge_quarter hA_le_two