awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
rw : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))

Tactic:
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)]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, MeasureTheory.IntegrableOn, Set.Ioc_subset_Ioi_self, MeasureTheory.Measure.restrict_restrict_of_subset, measurableSet_Ioc, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
hg : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) (uIcc 0 (↑n : ℝ))
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)

Tactic:
apply IntervalIntegrable.continuousOn_mul

Premises used: IntervalIntegrable.continuousOn_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)

Tactic:
intervalIntegral.intervalIntegrable_cpow' ?_

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
hf : -1 < (s - 1).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)

Tactic:
refine intervalIntegral.intervalIntegrable_cpow' ?_

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
hf : -1 < s.re - re 1
hf₁ : -1 < s.re - 1
hf₂ : HSub.hSub (α := ℝ) 0 1 < s.re - 1
hf₃ hf₄ hf₅ hf₆ : 0 < s.re
⊢ -1 < (s - 1).re

Tactic:
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]

Premises used: Complex.sub_re, sub_lt_sub_iff_right, Complex.one_re, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
funProp : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (uIcc 0 (↑n : ℝ)) x → Ne (α := ℝ) (↑n : ℝ) 0
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) (uIcc 0 (↑n : ℝ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
⊢ ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))

Tactic:
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]
    · fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
hl :
  EventuallyEq (β := ℂ) atTop (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) fun (n : ℕ) ↦ f n x
h :
  Tendsto (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
f₁ : ℕ → ℂ
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))

Tactic:
apply Tendsto.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
hl : ∀ᶠ (n : ℕ) in atTop, (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x
⊢ EventuallyEq (β := ℂ) atTop (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) fun (n : ℕ) ↦ f n x

Tactic:
change ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x

Premises used: HSub.hSub, Complex.ofReal, Filter.atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
h : ∀ (n : ℕ) (hn : ⌈x⌉₊ ≤ n), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x
⊢ ∀ᶠ (n : ℕ) in atTop, (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x

Tactic:
filter_upwards [eventually_ge_atTop ⌈x⌉₊] with n hn

Premises used: Nat.ceil, Filter.eventually_ge_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ x ≤ (↑n : ℝ)

Tactic:
rw [Nat.ceil_le] at hn

Premises used: Nat.ceil_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ)
h :
  (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) =
    indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x
⊢ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) = f n x

Tactic:
dsimp only [f]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ)
h : Membership.mem (γ := Set ℝ) (Ioc 0 (↑n : ℝ)) x
⊢ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) =
    indicator (Ioc 0 (↑n : ℝ)) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) x

Tactic:
rw [indicator_of_mem]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ)
⊢ Membership.mem (γ := Set ℝ) (Ioc 0 (↑n : ℝ)) x

Tactic:
⟨hx, hn⟩

Premises used: Set.Ioc, Set.Mem, setOf, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ)
⊢ Membership.mem (γ := Set ℝ) (Ioc 0 (↑n : ℝ)) x

Tactic:
exact ⟨hx, hn⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
h :
  Tendsto (fun (n : ℕ) ↦ (↑x : ℂ) ^ (s - 1) * (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) atTop
    (𝓝 ((↑x : ℂ) ^ (s - 1) * (↑(rexp (-x)) : ℂ)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)) : ℂ)))

Tactic:
(Tendsto.comp (continuous_ofReal.tendsto _) ?_).const_mul _

Premises used: Filter.Tendsto.const_mul, Continuous.tendsto, Complex.continuous_ofReal, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
h : Tendsto (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) atTop (𝓝 (rexp (-x)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑x : ℂ) ^ (s - 1) * (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) atTop
    (𝓝 ((↑x : ℂ) ^ (s - 1) * (↑(rexp (-x)) : ℂ)))

Tactic:
refine (Tendsto.comp (continuous_ofReal.tendsto _) ?_).const_mul _

Premises used: Filter.Tendsto.const_mul, Continuous.tendsto, Complex.continuous_ofReal, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)))

Tactic:
Real.tendsto_one_add_div_pow_exp (-x)

Premises used: Neg.neg, Real.tendsto_one_add_div_pow_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) fun (n : ℕ) ↦ (1 + -x / (↑n : ℝ)) ^ n
⊢ Tendsto (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) atTop (𝓝 (rexp (-x)))

Tactic:
convert! Real.tendsto_one_add_div_pow_exp (-x) using 1

Premises used: Neg.neg, Real.tendsto_one_add_div_pow_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
h : ∀ (n : ℕ), (1 - x / (↑n : ℝ)) ^ n = (1 + -x / (↑n : ℝ)) ^ n
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ (1 - x / (↑n : ℝ)) ^ n) fun (n : ℕ) ↦ (1 + -x / (↑n : ℝ)) ^ n

Tactic:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
h₁ h₂ : (1 - x / (↑n : ℝ)) ^ n = (1 - x / (↑n : ℝ)) ^ n
⊢ (1 - x / (↑n : ℝ)) ^ n = (1 + -x / (↑n : ℝ)) ^ n

Tactic:
rw [neg_div, ← sub_eq_add_neg]

Premises used: neg_div, sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ),
    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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f n a)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)))

Tactic:
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))

Premises used: Iff.mpr, Real.GammaIntegral_convergent, MeasureTheory.tendsto_integral_of_dominated_convergence, measurableSet_Ioi, And.left, MeasureTheory.ae_of_all, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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_integral_of_dominated_convergence :
  ∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 s.GammaIntegral)

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

Premises used: Iff.mpr, Real.GammaIntegral_convergent, MeasureTheory.tendsto_integral_of_dominated_convergence, measurableSet_Ioi, And.left, MeasureTheory.ae_of_all, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 :
  ∀ (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)
⊢ 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:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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))
h₂ 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))
⊢ 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:
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]

Premises used: MeasureTheory.integral_indicator, Set.Ioc_subset_Ioi_self, intervalIntegral.integral_of_le, MeasureTheory.Measure.restrict_restrict_of_subset, measurableSet_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℕ
rw : ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)

Tactic:
rw [ae_restrict_iff' measurableSet_Ioi]

Premises used: measurableSet_Ioi, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)
⊢ ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
filter_upwards with x hx
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
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)
⊢ ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
simp only [mem_Ioi, f] at hx ⊢

Premises used: Set.mem_Ioi