Source indexedlemma · leanprover/lean4:v4.32.0

Perron.diffBddAtZero

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:849 to 891

Mathematical statement

Exact Lean statement

@[blueprint
  "diffBddAtZero"
  (title := "diffBddAtZero")
  (statement := /--
  Let $x>0$. Then for $0 < c < 1 /2$, we have that the function
  $$
  s ↦ \frac{x^s}{s(s+1)} - \frac1s
  $$
  is bounded above on the rectangle with corners at $-c-i*c$ and $c+i*c$ (except at $s=0$).
  -/)
  (proof := /--
  Applying Lemma \ref{keyIdentity}, the
   function $s ↦ x^s/s(s+1) - 1/s = x^s/s - x^0/s - x^s/(1+s)$. The last term is bounded for $s$
   away from $-1$. The first two terms are the difference quotient of the function $s ↦ x^s$ at
   $0$; since it's differentiable, the difference remains bounded as $s\to 0$.
  -/)
  (latexEnv := "lemma")]
lemma diffBddAtZero {x : ℝ} (xpos : 0 < x) :
    ∀ᶠ (c : ℝ) in 𝓝[>] 0,
      BddAbove ((norm ∘ (fun (s : ℂ) ↦ (x : ℂ) ^ s / (s * (s + 1)) - 1 / s)) ''
        (Square 0 c \ {0}))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "diffBddAtZero"  (title := "diffBddAtZero")  (statement := /--  Let $x>0$. Then for $0 < c < 1 /2$, we have that the function  $$  s ↦ \frac{x^s}{s(s+1)} - \frac1s  $$  is bounded above on the rectangle with corners at $-c-i*c$ and $c+i*c$ (except at $s=0$).  -/)  (proof := /--  Applying Lemma \ref{keyIdentity}, the   function $s ↦ x^s/s(s+1) - 1/s = x^s/s - x^0/s - x^s/(1+s)$. The last term is bounded for $s$   away from $-1$. The first two terms are the difference quotient of the function $s ↦ x^s$ at   $0$; since it's differentiable, the difference remains bounded as $s\to 0$.  -/)  (latexEnv := "lemma")]lemma diffBddAtZero {x : ℝ} (xpos : 0 < x) :    ∀ᶠ (c : ℝ) in 𝓝[>] 0,      BddAbove ((norm ∘ (fun (s : ℂ) ↦ (x : ℂ) ^ s / (s * (s + 1)) - 1 / s)) ''        (Square 0 c \ {0})) := by   apply bddAbove_square_of_tendsto  suffices      Tendsto        (norm ∘ (fun (s : ℂ) ↦ ↑x ^ s / s - ↑x ^ (0 : ℂ) / s - ↑x ^ s / (1 + s)))        (𝓝[≠] 0)        (𝓝 (‖(deriv (fun (s : ℂ) ↦ (x : ℂ) ^ s) 0) -          x ^ (0 : ℂ) / (1 + 0)‖))    by    apply this.congr'    filter_upwards      [sdiff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds        (Set.mem_compl_singleton_iff.mpr (by norm_num : (0 : ℂ) ≠ -1))) {0}]    with s hs    rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.2 hs.1, cpow_zero]; ring_nf  have hx0 : (x : ℂ) ≠ 0 := slitPlane_ne_zero (.inl xpos)  refine (Tendsto.sub ?_ (tendsto_nhdsWithin_of_tendsto_nhds ?_)).norm  · convert hasDerivAt_iff_tendsto_slope.mp      (differentiableAt_fun_id.const_cpow (.inl hx0)).hasDerivAt using 2    rw [slope_def_field]; ring  · exact (continuous_id.const_cpow (.inl hx0)).tendsto 0      |>.div (tendsto_const_nhds.add tendsto_id) (by norm_num)