English
If the coefficients f(m) vanish for all m ≤ n and the L-series of f converges, then the limit of (n+1)^x · LSeries f x as x → ∞ equals f(n+1).
Русский
Если коэффициенты f(m) равны нулю для всех m ≤ n и L-порядок f сходится, то предел (n+1)^x · LSeries f x при x → ∞ равен f(n+1).
LaTeX
$$$$ \text{If } \forall m \le n,\; f(m)=0 \quad\text{and}\quad \operatorname{abscissaOfAbsConv}(f) < \infty, \\quad \lim_{x \to \infty} (n+1)^x \cdot \mathrm{LSeries} f x = f(n+1). $$$$
Lean4
/-- If the coefficients `f m` of an L-series are zero for `m ≤ n` and the L-series converges
at some point, then `f (n+1)` is the limit of `(n+1)^x * LSeries f x` as `x → ∞`. -/
theorem tendsto_cpow_mul_atTop {f : ℕ → ℂ} {n : ℕ} (h : ∀ m ≤ n, f m = 0) (ha : abscissaOfAbsConv f < ⊤) :
Tendsto (fun x : ℝ ↦ (n + 1) ^ (x : ℂ) * LSeries f x) atTop (nhds (f (n + 1))) :=
by
obtain ⟨y, hay, hyt⟩ := exists_between ha
lift y to ℝ using
⟨hyt.ne, ((OrderBot.bot_le _).trans_lt hay).ne'⟩
-- `F x m` is the `m`th term of `(n+1)^x * LSeries f x`, except that `F x (n+1) = 0`
let F := fun (x : ℝ) ↦ {m | n + 1 < m}.indicator (fun m ↦ f m / (m / (n + 1) : ℂ) ^ (x : ℂ))
have hF₀ (x : ℝ) {m : ℕ} (hm : m ≤ n + 1) : F x m = 0 := by simp [F, not_lt_of_ge hm]
have hF (x : ℝ) {m : ℕ} (hm : m ≠ n + 1) : F x m = ((n + 1) ^ (x : ℂ)) * term f x m :=
by
rcases lt_trichotomy m (n + 1) with H | rfl | H
· simp [Nat.not_lt_of_gt H, term, h m <| Nat.lt_succ_iff.mp H, F]
· exact (hm rfl).elim
· simp [H, term, (n.zero_lt_succ.trans H).ne', F, cpow_mul_div_cpow_eq_div_div_cpow]
have hs {x : ℝ} (hx : x ≥ y) : Summable fun m ↦ (n + 1) ^ (x : ℂ) * term f x m :=
by
refine
(summable_mul_left_iff <| natCast_add_one_cpow_ne_zero n _).mpr <| LSeriesSummable_of_abscissaOfAbsConv_lt_re ?_
simpa only [ofReal_re] using hay.trans_le <| EReal.coe_le_coe_iff.mpr hx
have key : ∀ x ≥ y, (n + 1) ^ (x : ℂ) * LSeries f x = f (n + 1) + ∑' m : ℕ, F x m :=
by
intro x hx
rw [LSeries, ← tsum_mul_left, (hs hx).tsum_eq_add_tsum_ite (n + 1), pow_mul_term_eq f x n]
congr
ext1 m
rcases eq_or_ne m (n + 1) with rfl | hm
· simp [hF₀ x le_rfl]
·
simp [hm, hF]
-- reduce to showing that `∑' m, F x m → 0` as `x → ∞`
conv => enter [3, 1]; rw [← add_zero (f _)]
refine
Tendsto.congr' (eventuallyEq_of_mem (s := {x | y ≤ x}) (mem_atTop y) key).symm <|
tendsto_const_nhds.add
?_
-- get the prerequisites for applying dominated convergence
have hys : Summable (F y) :=
by
refine ((hs le_rfl).indicator {m | n + 1 < m}).congr fun m ↦ ?_
by_cases hm : n + 1 < m
· simp [hF, hm, hm.ne']
· simp [hm, hF₀ _ (le_of_not_gt hm)]
have hc (k : ℕ) : Tendsto (F · k) atTop (nhds 0) :=
by
rcases lt_or_ge (n + 1) k with H | H
· have H₀ : (0 : ℝ) ≤ k / (n + 1) := by positivity
have H₀' : (0 : ℝ) ≤ (n + 1) / k := by positivity
have H₁ : (k / (n + 1) : ℂ) = (k / (n + 1) : ℝ) := by push_cast; rfl
have H₂ : (n + 1) / k < (1 : ℝ) := (div_lt_one <| mod_cast n.succ_pos.trans H).mpr <| mod_cast H
simp only [Set.mem_setOf_eq, H, Set.indicator_of_mem, F]
conv =>
enter [1, x]
rw [div_eq_mul_inv, H₁, ← ofReal_cpow H₀, ← ofReal_inv, ← Real.inv_rpow H₀, inv_div]
conv => enter [3, 1]; rw [← mul_zero (f k)]
exact (tendsto_rpow_atTop_of_base_lt_one _ (neg_one_lt_zero.trans_le H₀') H₂).ofReal.const_mul _
· simp [hF₀ _ H]
rw [show (0 : ℂ) = tsum (fun _ : ℕ ↦ 0) from tsum_zero.symm]
refine tendsto_tsum_of_dominated_convergence hys.norm hc <| eventually_iff.mpr ?_
filter_upwards [mem_atTop y] with y' hy' k
rcases lt_or_ge (n + 1) k with H | H
· simp only [Set.mem_setOf_eq, H, Set.indicator_of_mem, norm_div, norm_cpow_real, Complex.norm_natCast, F]
rw [← Nat.cast_one, ← Nat.cast_add, Complex.norm_natCast]
have hkn : 1 ≤ (k / (n + 1 :) : ℝ) := (one_le_div (by positivity)).mpr <| mod_cast Nat.le_of_succ_le H
gcongr
assumption
· simp [hF₀ _ H]
