Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.phi_bound_upwards

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3201 to 3207

Mathematical statement

Exact Lean statement

theorem phi_bound_upwards (ν ε : ℝ) (hν : ν > 0) :
    ∃ C, ∀ (z : ℂ), z.im ≥ 1 → z.re ∈ Set.Icc (-1 : ℝ) 1 →
      ‖Phi_circ ν ε z‖ + ‖Phi_star ν ε z‖ ≤ C * (z.im + 1)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem phi_bound_upwards (ν ε : ℝ) (hν : ν > 0) :    ∃ C, ∀ (z : ℂ), z.im ≥ 1 → z.re ∈ Set.Icc (-1 : ℝ) 1 →      ‖Phi_circ ν ε z‖ + ‖Phi_star ν ε z‖ ≤ C * (z.im + 1) := by  have h_safe : 1 > -ν / (2 * π) := by    rw [neg_div]; apply lt_trans (neg_neg_of_pos (by positivity)) zero_lt_one  obtain ⟨C, hC⟩ := phi_sum_norm_le_linear_halfplane ν ε hν 1 le_rfl true h_safe  exact ⟨C, fun z hz hz_re ↦ by simpa [abs_of_pos (by linarith : 0 < z.im)] using hC z hz hz_re⟩