approx_Gamma_integral_tendsto_Gamma_integral

English

Let s ∈ ℂ with Re(s) > 0. The sequence F_n(s) := ∫_0^n (1 − x/n)^n x^{s−1} dx converges to Γ(s) as n → ∞.

Русский

Пусть s ∈ ℂ с Re(s) > 0. Последовательность F_n(s) := ∫_0^n (1 − x/n)^n x^{s−1} dx сходится к Γ(s) при n → ∞.

LaTeX

$$$$ \lim_{n\to\infty} \int_{0}^{n} \bigl(1 - \frac{x}{n}\bigr)^{n} x^{s-1} \, dx = \Gamma(s). $$$$

Lean4

/-- The main technical lemma for `GammaSeq_tendsto_Gamma`, expressing the integral defining the
Gamma function for `0 < re s` as the limit of a sequence of integrals over finite intervals. -/
theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) :
    Tendsto (fun n : ℕ => ∫ x : ℝ in 0..n, ((1 - x / n) ^ n : ℝ) * (x : ℂ) ^ (s - 1)) atTop (𝓝 <| Gamma s) :=
  by
  rw [Gamma_eq_integral hs]
    -- We apply dominated convergence to the following function, which we will show is uniformly
      -- bounded above by the Gamma integrand `exp (-x) * x ^ (re s - 1)`.

  let f : ℕ → ℝ → ℂ := fun n =>
    indicator (Ioc 0 (n : ℝ)) fun x : ℝ =>
      ((1 - x / n) ^ n : ℝ) *
        (x : ℂ) ^
          (s - 1)
            -- integrability of f

  have f_ible : ∀ n : ℕ, Integrable (f n) (volume.restrict (Ioi 0)) :=
    by
    intro n
    rw [integrable_indicator_iff (measurableSet_Ioc : MeasurableSet (Ioc (_ : ℝ) _)), IntegrableOn,
      Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self, ← IntegrableOn, ←
      intervalIntegrable_iff_integrableOn_Ioc_of_le (by positivity : (0 : ℝ) ≤ n)]
    apply IntervalIntegrable.continuousOn_mul
    · refine intervalIntegral.intervalIntegrable_cpow' ?_
      rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
    · apply Continuous.continuousOn
      continuity
        -- pointwise limit of f

  have f_tends :
    ∀ x : ℝ, x ∈ Ioi (0 : ℝ) → Tendsto (fun n : ℕ => f n x) atTop (𝓝 <| ↑(Real.exp (-x)) * (x : ℂ) ^ (s - 1)) :=
    by
    intro x hx
    apply Tendsto.congr'
    · change ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x
      filter_upwards [eventually_ge_atTop ⌈x⌉₊] with n hn
      rw [Nat.ceil_le] at hn
      dsimp only [f]
      rw [indicator_of_mem]
      exact ⟨hx, hn⟩
    · simp_rw [mul_comm]
      refine (Tendsto.comp (continuous_ofReal.tendsto _) ?_).const_mul _
      convert Real.tendsto_one_add_div_pow_exp (-x) using 1
      ext1 n
      rw [neg_div, ← sub_eq_add_neg]
        -- let `convert` identify the remaining goals

  convert
    tendsto_integral_of_dominated_convergence _ (fun n => (f_ible n).1) (Real.GammaIntegral_convergent hs) _
      ((ae_restrict_iff' measurableSet_Ioi).mpr (ae_of_all _ f_tends)) using
    1
    -- limit of f is the integrand we want

  · ext1 n
    rw [MeasureTheory.integral_indicator (measurableSet_Ioc : MeasurableSet (Ioc (_ : ℝ) _)),
      intervalIntegral.integral_of_le (by positivity : 0 ≤ (n : ℝ)),
      Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self]
      -- f is uniformly bounded by the Gamma integrand

  · intro n
    rw [ae_restrict_iff' measurableSet_Ioi]
    filter_upwards with x hx
    simp only [mem_Ioi, f] at hx ⊢
    rcases lt_or_ge (n : ℝ) x with (hxn | hxn)
    · rw [indicator_of_notMem (notMem_Ioc_of_gt hxn), norm_zero, mul_nonneg_iff_right_nonneg_of_pos (exp_pos _)]
      exact rpow_nonneg (le_of_lt hx) _
    · rw [indicator_of_mem (mem_Ioc.mpr ⟨mem_Ioi.mp hx, hxn⟩), norm_mul,
        Complex.norm_of_nonneg (pow_nonneg (sub_nonneg.mpr <| div_le_one_of_le₀ hxn <| by positivity) _),
        norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
      gcongr
      exact one_sub_div_pow_le_exp_neg hxn

Похожие утверждения