awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ EventuallyEq (β := ℂ) atTop (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) fun (n : ℕ) ↦ f n x
have hl : ∀ᶠ (n : ℕ) in atTop, (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x
Tactic: change ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ∀ᶠ (n : ℕ) in atTop, (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x
have h : ∀ (n : ℕ) (hn : ⌈x⌉₊ ≤ n), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x
Tactic: filter_upwards [eventually_ge_atTop ⌈x⌉₊] with n hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
n : ℕ
hn : ⌈x⌉₊ ≤ n
⊢ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x
have hn₁ : x ≤ (↑n : ℝ)
Tactic: rw [Nat.ceil_le] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
n : ℕ
hn : x ≤ (↑n : ℝ)
⊢ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) =
    indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x
have h : Membership.mem (γ := Set ℝ) (Ioc 0 (↑n : ℝ)) x
Tactic: rw [indicator_of_mem]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Tendsto (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
have h : Tendsto (fun (n : ℕ) ↦ (↑x : ℂ) ^ (s - 1) * (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) atTop
  (𝓝 ((↑x : ℂ) ^ (s - 1) * (↑(rexp (-x)) : ℂ)))
Tactic: simp_rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Tendsto (fun (n : ℕ) ↦ (↑x : ℂ) ^ (s - 1) * (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) atTop
    (𝓝 ((↑x : ℂ) ^ (s - 1) * (↑(rexp (-x)) : ℂ)))
have h : Tendsto (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) atTop (𝓝 (rexp (-x)))
Tactic: refine (Tendsto.comp (continuous_ofReal.tendsto _) ?_).const_mul _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Tendsto (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) atTop (𝓝 (rexp (-x)))
have h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) fun (n : ℕ) ↦ (1 + -x / (↑n : ℝ)) ^ n
Tactic: convert! Real.tendsto_one_add_div_pow_exp (-x) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) fun (n : ℕ) ↦ (1 + -x / (↑n : ℝ)) ^ n
have h : ∀ (n : ℕ), (1 - x / (↑n : ℝ)) ^ n = (1 + -x / (↑n : ℝ)) ^ n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
n : ℕ
⊢ (1 - x / (↑n : ℝ)) ^ n = (1 + -x / (↑n : ℝ)) ^ n
have h : (1 - x / (↑n : ℝ)) ^ n = (1 + -(x / (↑n : ℝ))) ^ n
Tactic: rw [neg_div, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
n : ℕ
h : (1 - x / (↑n : ℝ)) ^ n = (1 + -(x / (↑n : ℝ))) ^ n
⊢ (1 - x / (↑n : ℝ)) ^ n = (1 + -x / (↑n : ℝ)) ^ n
have h₁ : (1 - x / (↑n : ℝ)) ^ n = (1 - x / (↑n : ℝ)) ^ n
Tactic: rw [neg_div, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 s.GammaIntegral)
have f_tends : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 s.GammaIntegral)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
  fun (n : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a
Tactic: 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    fun (n : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 s.GammaIntegral)
have tendsto_integral_of_dominated_convergence : ∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)
Tactic: 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    fun (n : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a
have h : ∀ (n : ℕ),
  Eq (α := ℂ) (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a)
have h : Eq (α := ℂ) (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioi 0)) (Ioc 0 (↑n : ℝ)))
    fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
h :
  Eq (α := ℂ) (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioi 0)) (Ioc 0 (↑n : ℝ)))
      fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a)
have h₁ : Eq (α := ℂ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (↑n : ℝ))) fun (x : ℝ) ↦
    (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioi 0)) (Ioc 0 (↑n : ℝ)))
    fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
h :
  Eq (α := ℂ) (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioi 0)) (Ioc 0 (↑n : ℝ)))
      fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
h₁ :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (↑n : ℝ))) fun (x : ℝ) ↦
      (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioi 0)) (Ioc 0 (↑n : ℝ)))
      fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a)
have h₂ : Eq (α := ℂ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (↑n : ℝ))) fun (x : ℝ) ↦
    (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (↑n : ℝ))) fun (x : ℝ) ↦
    (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)
have rw : ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)
Tactic: rw [ae_restrict_iff' measurableSet_Ioi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
⊢ ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)
have h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)
Tactic: filter_upwards with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)
have h : ∀ (hx : 0 < x),
  Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)
Tactic: simp only [mem_Ioi, f] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
⊢ Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)
have h : ∀ (hxn : (↑n : ℝ) < x),
  Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)
Tactic: rcases lt_or_ge (n : ℝ) x with (hxn | hxn)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
h :
  ∀ (hxn : (↑n : ℝ) < x),
    Norm.norm (E := ℂ)
        (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
      rexp (-x) * x ^ (s.re - 1)
⊢ Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)
have h₁ : ∀ (hxn : x ≤ (↑n : ℝ)),
  Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)
Tactic: rcases lt_or_ge (n : ℝ) x with (hxn | hxn)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : (↑n : ℝ) < x
⊢ Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)
have h : 0 ≤ x ^ (s.re - 1)
Tactic: rw [indicator_of_notMem (notMem_Ioc_of_gt hxn), norm_zero,
        mul_nonneg_iff_right_nonneg_of_pos (exp_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ (↑n : ℝ)
⊢ Norm.norm (E := ℂ)
      (indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x) ≤
    rexp (-x) * x ^ (s.re - 1)
have h : (1 - x / (↑n : ℝ)) ^ n * x ^ (s.re - 1) ≤ rexp (-x) * x ^ (s.re - 1)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
f_tends :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ (↑n : ℝ)
⊢ (1 - x / (↑n : ℝ)) ^ n * x ^ (s.re - 1) ≤ rexp (-x) * x ^ (s.re - 1)
have h : (1 - x / (↑n : ℝ)) ^ n ≤ rexp (-x)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this : ∀ (m : ℕ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have tauto : ∀ ⦃U : Set ℂ⦄, U ∈ 𝓝 (Gamma s) → U ∈ map s.GammaSeq atTop
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have suffices : ∀ (m : ℕ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Tactic: suffices ∀ m : ℕ, ⌊1 - s.re⌋₊ = m → Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) by tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : ⌊1 - s.re⌋₊ = 0
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have hs₁ : 0 < s.re
Tactic: rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have zero : (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) =ᶠ[atTop] s.GammaSeq
Tactic: apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) =ᶠ[atTop] s.GammaSeq
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                (fun (n : ℕ) ↦ (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) : ℂ)) x =
                  s.GammaSeq x)
              x}
          x}
    a
Tactic: filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm