Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.cartan_majorant_four_term_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanMajorantBound.lean:178 to 191

Mathematical statement

Exact Lean statement

lemma cartan_majorant_four_term_bound
    {xφ x0 xm xt Cφ m q Y T : ℝ}
    (hφ : xφ ≤ Cφ * q * Y * T)
    (h0 : x0 ≤ m * q * Y * T)
    (hm : xm ≤ m * q * Y * T)
    (ht : xt ≤ (2 : ℝ) * Y * T) :
    xφ + x0 + xm + xt ≤ (Cφ + (2 : ℝ) * m) * q * Y * T + (2 : ℝ) * Y * T

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cartan_majorant_four_term_bound    {xφ x0 xm xt Cφ m q Y T : ℝ}    (hφ : xφ ≤ Cφ * q * Y * T)    (h0 : x0 ≤ m * q * Y * T)    (hm : xm ≤ m * q * Y * T)    (ht : xt ≤ (2 : ℝ) * Y * T) :    xφ + x0 + xm + xt ≤ (Cφ + (2 : ℝ) * m) * q * Y * T + (2 : ℝ) * Y * T := by  have h :=    add_four_le_add_two_mul_of_le hφ h0 hm ht  have hring :      Cφ * (q * (Y * T)) + 2 * (m * (q * (Y * T))) + 2 * (Y * T)        = (Cφ + (2 : ℝ) * m) * (q * (Y * T)) + (2 : ℝ) * (Y * T) := by    ring  simpa [mul_assoc, hring] using h