Source indexedlemma · leanprover/lean4:v4.32.0

ZetaBnd_aux1

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1032 to 1052

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "ZetaBnd-aux1")
  (statement := /--
  For any $N\ge1$ and $s = \sigma + tI \in \C$, $\sigma=\in(0,2], 2 < |t|$,
  $$
  \left| s\int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right|
  \le 2 |t| \frac{N^{-\sigma}}{\sigma}.
  $$
  -/)
  (proof := /-- Apply Lemma \ref{ZetaBnd_aux1b} and estimate $|s|\ll |t|$. -/)
  (latexEnv := "lemma")]
lemma ZetaBnd_aux1 (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (hσ : σ ∈ Ioc 0 2) (ht : 2 ≤ |t|) :
    ‖(σ + t * I) * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖
    ≤ 2 * |t| * N ^ (-σ) / σ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "ZetaBnd-aux1")  (statement := /--  For any $N\ge1$ and $s = \sigma + tI \in \C$, $\sigma=\in(0,2], 2 < |t|$,  $$  \left| s\int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right|  \le 2 |t| \frac{N^{-\sigma}}{\sigma}.  $$  -/)  (proof := /-- Apply Lemma \ref{ZetaBnd_aux1b} and estimate $|s|\ll |t|$. -/)  (latexEnv := "lemma")]lemma ZetaBnd_aux1 (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (hσ : σ ∈ Ioc 0 2) (ht : 2 ≤ |t|) :    ‖(σ + t * I) * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖    ≤ 2 * |t| * N ^ (-σ) / σ := by  rw [norm_mul, mul_div_assoc]  rw [Set.mem_Ioc] at hσ  apply mul_le_mul ?_ (ZetaBnd_aux1b N Npos hσ.1) (norm_nonneg _) (by positivity)  refine le_trans (by apply norm_add_le) ?_  simp only [Complex.norm_of_nonneg hσ.1.le, Complex.norm_mul, norm_real, Real.norm_eq_abs, norm_I,    mul_one]  linarith [hσ.2]