Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.norm_Phi_lambda_one_add_I_mul_le_of_pos

PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3294 to 3304

Source documentation

For positive λ, Phi_lambda on 1 + i y is bounded by y.

Exact Lean statement

theorem norm_Phi_lambda_one_add_I_mul_le_of_pos (lam ε y : ℝ) (hlam : 0 < lam)
    (hε : ε = 1 ∨ ε = -1) (hy : 0 ≤ y) :
    ‖Phi_lambda lam ε (1 + I * (y : ℂ))‖ ≤ y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_Phi_lambda_one_add_I_mul_le_of_pos (lam ε y : ℝ) (hlam : 0 < lam)    (hε : ε = 1 ∨ ε = -1) (hy : 0 ≤ y) :    ‖Phi_lambda lam ε (1 + I * (y : ℂ))‖ ≤ y := by  have hν : 0 < |lam| := abs_pos.mpr (ne_of_gt hlam)  have hphi :      Phi_lambda lam ε (1 + I * (y : ℂ)) = Phi_star |lam| ε (I * (y : ℂ)) := by    rw [Phi_lambda]    simp [Real.sign_of_pos hlam, Real.sign_of_pos (by norm_num : (0 : ℝ) < 1),      shift_upwards_phi_sum |lam| ε hν y hy]  rw [hphi]  exact (norm_Phi_star_I_mul_le |lam| ε y hε).trans_eq (abs_of_nonneg hy)