Source indexedlemma · leanprover/lean4:v4.32.0

Complex.CartanBound.intervalIntegrable_phi_dyadic

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:450 to 463

Mathematical statement

Exact Lean statement

lemma intervalIntegrable_phi_dyadic {A : ℝ} (hA : 0 ≤ A) :
    IntervalIntegrable φ volume A (2 * A)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_phi_dyadic {A : ℝ} (hA : 0 ≤ A) :    IntervalIntegrable φ volume A (2 * A) := by  by_cases hA0 : A = 0  · subst hA0    simp  cases le_total A (1 / 4 : ℝ) with  | inl hsmall =>      exact intervalIntegrable_phi_dyadic_small hA hsmall  | inr hge_quarter =>      cases le_total (2 : ℝ) A with      | inl hbig =>          exact intervalIntegrable_phi_dyadic_large hbig      | inr hA_le_two =>          exact intervalIntegrable_phi_dyadic_middle hge_quarter hA_le_two