English
A technical lemma: given a family Λ with differentiability away from 0 and 1, and a limiting behavior sΛ(s) near 0, the differentiated/updated function is differentiable away from s = 1 after a Gamma-adjusted normalization.
Русский
Техническая лемма: при наличии семейства Λ, дифференцируемого вне точек 0 и 1, и заданного предела для s Λ(s) около 0, модифицированная функция остаётся дифференцируемой вне точки 1 после нормализации на Gamma(s).
LaTeX
$$$\\forall \\Lambda,\\ hf: \\forall s\\,(s\\neq0),\\ (s\\neq1) \\Rightarrow \\text{DifferentiableAt}_{\\mathbb{C}}(\\mathrm{update}(\\lambda s.\\Lambda(s)/\\Gamma\\!\\mathbb{R}(s))\\ 0\\ (L/2), s).$$$
Lean4
/-- Technical lemma which will give us differentiability of Hurwitz zeta at `s = 0`. -/
theorem differentiableAt_update_of_residue {Λ : ℂ → ℂ} (hf : ∀ (s : ℂ) (_ : s ≠ 0) (_ : s ≠ 1), DifferentiableAt ℂ Λ s)
{L : ℂ} (h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)) (s : ℂ) (hs' : s ≠ 1) :
DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / Gammaℝ s) 0 (L / 2)) s :=
by
have claim (t) (ht : t ≠ 0) (ht' : t ≠ 1) : DifferentiableAt ℂ (fun u : ℂ ↦ Λ u / Gammaℝ u) t :=
(hf t ht ht').mul differentiable_Gammaℝ_inv.differentiableAt
have claim2 : Tendsto (fun s : ℂ ↦ Λ s / Gammaℝ s) (𝓝[≠] 0) (𝓝 <| L / 2) :=
by
refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)
filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)
rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]
rcases ne_or_eq s 0 with hs | rfl
· -- Easy case : `s ≠ 0`
refine (claim s hs hs').congr_of_eventuallyEq ?_
filter_upwards [isOpen_compl_singleton.mem_nhds hs] with x hx
simp [Function.update_of_ne hx]
· -- Hard case : `s = 0`
simp_rw [← claim2.limUnder_eq]
have S_nhds : {(1 : ℂ)}ᶜ ∈ 𝓝 (0 : ℂ) := isOpen_compl_singleton.mem_nhds hs'
refine
((Complex.differentiableOn_update_limUnder_of_isLittleO S_nhds
(fun t ht ↦ (claim t ht.2 ht.1).differentiableWithinAt) ?_)
0 hs').differentiableAt
S_nhds
simp only [Gammaℝ, zero_div, div_zero, Complex.Gamma_zero, mul_zero, sub_zero]
-- Remains to show completed zeta is `o (s ^ (-1))` near 0.
refine (isBigO_const_of_tendsto claim2 <| one_ne_zero' ℂ).trans_isLittleO ?_
rw [isLittleO_iff_tendsto']
· exact Tendsto.congr (fun x ↦ by rw [← one_div, one_div_one_div]) nhdsWithin_le_nhds
· exact eventually_of_mem self_mem_nhdsWithin fun x hx hx' ↦ (hx <| inv_eq_zero.mp hx').elim
