[GOAL]
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 (1 / 2)
[PROOFSTEP]
apply IntervalIntegrable.mul_continuousOn
[GOAL]
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1)) volume 0 (1 / 2)
[PROOFSTEP]
refine' intervalIntegral.intervalIntegrable_cpow' _
[GOAL]
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ -1 < (u - 1).re
[PROOFSTEP]
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
[GOAL]
case hg
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ContinuousOn (fun x => (1 - ↑x) ^ (v - 1)) (uIcc 0 (1 / 2))
[PROOFSTEP]
apply ContinuousAt.continuousOn
[GOAL]
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ∀ (x : ℝ), x ∈ uIcc 0 (1 / 2) → ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x
[PROOFSTEP]
intro x hx
[GOAL]
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x
[PROOFSTEP]
rw [uIcc_of_le (by positivity : (0 : ℝ) ≤ 1 / 2)] at hx
[GOAL]
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ 0 ≤ 1 / 2
[PROOFSTEP]
positivity
[GOAL]
case hg.hcont
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => (1 - ↑x) ^ (v - 1)) x
[PROOFSTEP]
apply ContinuousAt.cpow
[GOAL]
case hg.hcont.hf
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => 1 - ↑x) x
[PROOFSTEP]
exact (continuous_const.sub continuous_ofReal).continuousAt
[GOAL]
case hg.hcont.hg
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ ContinuousAt (fun x => v - 1) x
[PROOFSTEP]
exact continuousAt_const
[GOAL]
case hg.hcont.h0
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ 0 < (1 - ↑x).re ∨ (1 - ↑x).im ≠ 0
[PROOFSTEP]
rw [sub_re, one_re, ofReal_re, sub_pos]
[GOAL]
case hg.hcont.h0
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ x < 1 ∨ (1 - ↑x).im ≠ 0
[PROOFSTEP]
exact Or.inl (hx.2.trans_lt (by norm_num : (1 / 2 : ℝ) < 1))
[GOAL]
u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ Icc 0 (1 / 2)
⊢ 1 / 2 < 1
[PROOFSTEP]
norm_num
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 1
[PROOFSTEP]
refine' (betaIntegral_convergent_left hu v).trans _
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume (1 / 2) 1
[PROOFSTEP]
rw [IntervalIntegrable.iff_comp_neg]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) volume (-(1 / 2)) (-1)
[PROOFSTEP]
convert ((betaIntegral_convergent_left hv u).comp_add_right 1).symm using 1
[GOAL]
case h.e'_3
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ (fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) = fun x => ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_3.h
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1) = ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)
[PROOFSTEP]
conv_lhs => rw [mul_comm]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
| ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
| ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
| ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case h.e'_3.h
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ (1 - ↑(-x)) ^ (v - 1) * ↑(-x) ^ (u - 1) = ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_3.h.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - ↑(-x) = ↑(x + 1)
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.h.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - -↑x = ↑x + 1
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ ↑(-x) = 1 - ↑(x + 1)
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.h.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ -↑x = 1 - (↑x + 1)
[PROOFSTEP]
ring
[GOAL]
case h.e'_5
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -(1 / 2) = 1 / 2 - 1
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = 0 - 1
[PROOFSTEP]
norm_num
[GOAL]
u v : ℂ
⊢ betaIntegral v u = betaIntegral u v
[PROOFSTEP]
rw [betaIntegral, betaIntegral]
[GOAL]
u v : ℂ
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
[PROOFSTEP]
have :=
  intervalIntegral.integral_comp_mul_add (a := 0) (b := 1) (c := -1)
    (fun x : ℝ => (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1)) neg_one_lt_zero.ne 1
[GOAL]
u v : ℂ
this :
  ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) =
    (-1)⁻¹ • ∫ (x : ℝ) in -1 * 0 + 1 ..-1 * 1 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
[PROOFSTEP]
rw [inv_neg, inv_one, neg_one_smul, ← intervalIntegral.integral_symm] at this
[GOAL]
u v : ℂ
this :
  ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) =
    ∫ (x : ℝ) in -1 * 1 + 1 ..-1 * 0 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
[PROOFSTEP]
simp at this
[GOAL]
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
[PROOFSTEP]
conv_lhs at this => arg 1; intro x; rw [add_comm, ← sub_eq_add_neg, mul_comm]
[GOAL]
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
| ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1)
[PROOFSTEP]
arg 1; intro x; rw [add_comm, ← sub_eq_add_neg, mul_comm]
[GOAL]
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
| ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1)
[PROOFSTEP]
arg 1; intro x; rw [add_comm, ← sub_eq_add_neg, mul_comm]
[GOAL]
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
| ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1)
[PROOFSTEP]
arg 1
[GOAL]
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
| fun x => (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1)
[PROOFSTEP]
intro x
[GOAL]
case h
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
x : ℝ
| (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1)
[PROOFSTEP]
rw [add_comm, ← sub_eq_add_neg, mul_comm]
[GOAL]
u v : ℂ
this : ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
[PROOFSTEP]
exact this
[GOAL]
u : ℂ
hu : 0 < u.re
⊢ betaIntegral u 1 = 1 / u
[PROOFSTEP]
simp_rw [betaIntegral, sub_self, cpow_zero, mul_one]
[GOAL]
u : ℂ
hu : 0 < u.re
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) = 1 / u
[PROOFSTEP]
rw [integral_cpow (Or.inl _)]
[GOAL]
u : ℂ
hu : 0 < u.re
⊢ (↑1 ^ (u - 1 + 1) - ↑0 ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u
[PROOFSTEP]
rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]
[GOAL]
u : ℂ
hu : 0 < u.re
⊢ u - 1 + 1 ≠ 0
[PROOFSTEP]
rw [sub_add_cancel]
[GOAL]
u : ℂ
hu : 0 < u.re
⊢ u ≠ 0
[PROOFSTEP]
contrapose! hu
[GOAL]
u : ℂ
hu : u = 0
⊢ u.re ≤ 0
[PROOFSTEP]
rw [hu, zero_re]
[GOAL]
u : ℂ
hu : 0 < u.re
⊢ -1 < (u - 1).re
[PROOFSTEP]
rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * betaIntegral s t
[PROOFSTEP]
have ha' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha.ne'
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * betaIntegral s t
[PROOFSTEP]
rw [betaIntegral]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a ^ (s + t - 1) * ∫ (x : ℝ) in 0 ..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1)
[PROOFSTEP]
have A : (a : ℂ) ^ (s + t - 1) = a * ((a : ℂ) ^ (s - 1) * (a : ℂ) ^ (t - 1)) := by
  rw [(by abel : s + t - 1 = 1 + (s - 1) + (t - 1)), cpow_add _ _ ha', cpow_add 1 _ ha', cpow_one, mul_assoc]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
[PROOFSTEP]
rw [(by abel : s + t - 1 = 1 + (s - 1) + (t - 1)), cpow_add _ _ ha', cpow_add 1 _ ha', cpow_one, mul_assoc]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ s + t - 1 = 1 + (s - 1) + (t - 1)
[PROOFSTEP]
abel
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ s + t - 1 = 1 + (s - 1) + (t - 1)
[PROOFSTEP]
abel
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ↑a ^ (s + t - 1) * ∫ (x : ℝ) in 0 ..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (t - 1)
[PROOFSTEP]
rw [A, mul_assoc, ← intervalIntegral.integral_const_mul, ← real_smul, ← zero_div a, ← div_self ha.ne', ←
  intervalIntegral.integral_comp_div _ ha.ne', zero_div]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ∫ (x : ℝ) in 0 ..a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))
[PROOFSTEP]
simp_rw [intervalIntegral.integral_of_le ha.le]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in Ioc 0 a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ∫ (x : ℝ) in Ioc 0 a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))
[PROOFSTEP]
refine' set_integral_congr measurableSet_Ioc fun x hx => _
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))
[PROOFSTEP]
rw [mul_mul_mul_comm]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1) * (↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1)
[PROOFSTEP]
rw [← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le, ofReal_div, mul_div_cancel' _ ha']
[GOAL]
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = ↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1)
[PROOFSTEP]
rw [(by norm_cast : (1 : ℂ) - ↑(x / a) = ↑(1 - x / a)), ←
  mul_cpow_ofReal_nonneg ha.le (sub_nonneg.mpr <| (div_le_one ha).mpr hx.2)]
[GOAL]
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ 1 - ↑(x / a) = ↑(1 - x / a)
[PROOFSTEP]
norm_cast
[GOAL]
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * ↑(1 - x / a)) ^ (t - 1)
[PROOFSTEP]
push_cast
[GOAL]
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * (1 - ↑x / ↑a)) ^ (t - 1)
[PROOFSTEP]
rw [mul_sub, mul_one, mul_div_cancel' _ ha']
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
⊢ Gamma s * Gamma t = Gamma (s + t) * betaIntegral s t
[PROOFSTEP]
have conv_int :=
  integral_posConvolution (GammaIntegral_convergent hs) (GammaIntegral_convergent ht) (ContinuousLinearMap.mul ℝ ℂ)
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x,
        ↑(↑(ContinuousLinearMap.mul ℝ ℂ) (↑(rexp (-t_1)) * ↑t_1 ^ (s - 1)))
          (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ↑(↑(ContinuousLinearMap.mul ℝ ℂ) (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)))
      (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1))
⊢ Gamma s * Gamma t = Gamma (s + t) * betaIntegral s t
[PROOFSTEP]
simp_rw [ContinuousLinearMap.mul_apply'] at conv_int
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
⊢ Gamma s * Gamma t = Gamma (s + t) * betaIntegral s t
[PROOFSTEP]
have hst : 0 < re (s + t) := by rw [add_re]; exact add_pos hs ht
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
⊢ 0 < (s + t).re
[PROOFSTEP]
rw [add_re]
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
⊢ 0 < s.re + t.re
[PROOFSTEP]
exact add_pos hs ht
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
⊢ Gamma s * Gamma t = Gamma (s + t) * betaIntegral s t
[PROOFSTEP]
rw [Gamma_eq_integral hs, Gamma_eq_integral ht, Gamma_eq_integral hst, GammaIntegral, GammaIntegral, GammaIntegral, ←
  conv_int, ← integral_mul_right (betaIntegral _ _)]
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
⊢ ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ∫ (a : ℝ) in Ioi 0, ↑(rexp (-a)) * ↑a ^ (s + t - 1) * betaIntegral s t
[PROOFSTEP]
refine' set_integral_congr measurableSet_Ioi fun x hx => _
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
⊢ ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ↑(rexp (-x)) * ↑x ^ (s + t - 1) * betaIntegral s t
[PROOFSTEP]
rw [mul_assoc, ← betaIntegral_scaled s t hx, ← intervalIntegral.integral_const_mul]
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
⊢ ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ∫ (x_1 : ℝ) in 0 ..x, ↑(rexp (-x)) * (↑x_1 ^ (s - 1) * (↑x - ↑x_1) ^ (t - 1))
[PROOFSTEP]
congr 1 with y : 1
[GOAL]
case e_f.h
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ ↑(rexp (-y)) * ↑y ^ (s - 1) * (↑(rexp (-(x - y))) * ↑(x - y) ^ (t - 1)) =
    ↑(rexp (-x)) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))
[PROOFSTEP]
push_cast
[GOAL]
case e_f.h
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ cexp (-↑y) * ↑y ^ (s - 1) * (cexp (-(↑x - ↑y)) * (↑x - ↑y) ^ (t - 1)) =
    cexp (-↑x) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))
[PROOFSTEP]
suffices Complex.exp (-x) = Complex.exp (-y) * Complex.exp (-(x - y)) by rw [this]; ring
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
this : cexp (-↑x) = cexp (-↑y) * cexp (-(↑x - ↑y))
⊢ cexp (-↑y) * ↑y ^ (s - 1) * (cexp (-(↑x - ↑y)) * (↑x - ↑y) ^ (t - 1)) =
    cexp (-↑x) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))
[PROOFSTEP]
rw [this]
[GOAL]
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
this : cexp (-↑x) = cexp (-↑y) * cexp (-(↑x - ↑y))
⊢ cexp (-↑y) * ↑y ^ (s - 1) * (cexp (-(↑x - ↑y)) * (↑x - ↑y) ^ (t - 1)) =
    cexp (-↑y) * cexp (-(↑x - ↑y)) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))
[PROOFSTEP]
ring
[GOAL]
case e_f.h
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ cexp (-↑x) = cexp (-↑y) * cexp (-(↑x - ↑y))
[PROOFSTEP]
rw [← Complex.exp_add]
[GOAL]
case e_f.h
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ cexp (-↑x) = cexp (-↑y + -(↑x - ↑y))
[PROOFSTEP]
congr 1
[GOAL]
case e_f.h.e_z
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ -↑x = -↑y + -(↑x - ↑y)
[PROOFSTEP]
abel
[GOAL]
case e_f.h.e_z
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1)
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ -↑x = -↑y + -(↑x - ↑y)
[PROOFSTEP]
abel
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
let F : ℝ → ℂ := fun x => (x : ℂ) ^ u * (1 - (x : ℂ)) ^ v
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have hu' : 0 < re (u + 1) := by rw [add_re, one_re]; positivity
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
⊢ 0 < (u + 1).re
[PROOFSTEP]
rw [add_re, one_re]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
⊢ 0 < u.re + 1
[PROOFSTEP]
positivity
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have hv' : 0 < re (v + 1) := by rw [add_re, one_re]; positivity
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
⊢ 0 < (v + 1).re
[PROOFSTEP]
rw [add_re, one_re]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
⊢ 0 < v.re + 1
[PROOFSTEP]
positivity
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have hc : ContinuousOn F (Icc 0 1) :=
  by
  refine' (ContinuousAt.continuousOn fun x hx => _).mul (ContinuousAt.continuousOn fun x hx => _)
  · refine' (continuousAt_cpow_const_of_re_pos (Or.inl _) hu).comp continuous_ofReal.continuousAt
    rw [ofReal_re]; exact hx.1
  · refine' (continuousAt_cpow_const_of_re_pos (Or.inl _) hv).comp (continuous_const.sub continuous_ofReal).continuousAt
    rw [sub_re, one_re, ofReal_re, sub_nonneg]
    exact hx.2
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
⊢ ContinuousOn F (Icc 0 1)
[PROOFSTEP]
refine' (ContinuousAt.continuousOn fun x hx => _).mul (ContinuousAt.continuousOn fun x hx => _)
[GOAL]
case refine'_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ ContinuousAt (fun x => ↑x ^ u) x
[PROOFSTEP]
refine' (continuousAt_cpow_const_of_re_pos (Or.inl _) hu).comp continuous_ofReal.continuousAt
[GOAL]
case refine'_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 ≤ (↑x).re
[PROOFSTEP]
rw [ofReal_re]
[GOAL]
case refine'_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 ≤ x
[PROOFSTEP]
exact hx.1
[GOAL]
case refine'_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ ContinuousAt (fun x => (1 - ↑x) ^ v) x
[PROOFSTEP]
refine' (continuousAt_cpow_const_of_re_pos (Or.inl _) hv).comp (continuous_const.sub continuous_ofReal).continuousAt
[GOAL]
case refine'_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 ≤ (1 - ↑x).re
[PROOFSTEP]
rw [sub_re, one_re, ofReal_re, sub_nonneg]
[GOAL]
case refine'_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : x ∈ Icc 0 1
⊢ x ≤ 1
[PROOFSTEP]
exact hx.2
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have hder :
  ∀ x : ℝ,
    x ∈ Ioo (0 : ℝ) 1 →
      HasDerivAt F (u * ((x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ v) - v * ((x : ℂ) ^ u * (1 - (x : ℂ)) ^ (v - 1))) x :=
  by
  intro x hx
  have U : HasDerivAt (fun y : ℂ => y ^ u) (u * (x : ℂ) ^ (u - 1)) ↑x :=
    by
    have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
    simp only [id_eq, mul_one] at this
    · exact this
    · rw [id_eq, ofReal_re]; exact hx.1
  have V : HasDerivAt (fun y : ℂ => (1 - y) ^ v) (-v * (1 - (x : ℂ)) ^ (v - 1)) ↑x :=
    by
    have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
    swap; · rw [id.def, sub_re, one_re, ofReal_re, sub_pos]; exact hx.2
    simp_rw [id.def] at A
    have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by apply HasDerivAt.const_sub; apply hasDerivAt_id
    convert HasDerivAt.comp (↑x) A B using 1
    ring
  convert (U.mul V).comp_ofReal using 1
  ring
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
⊢ ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
[PROOFSTEP]
intro x hx
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
⊢ HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
[PROOFSTEP]
have U : HasDerivAt (fun y : ℂ => y ^ u) (u * (x : ℂ) ^ (u - 1)) ↑x :=
  by
  have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
  simp only [id_eq, mul_one] at this
  · exact this
  · rw [id_eq, ofReal_re]; exact hx.1
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
⊢ HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
[PROOFSTEP]
have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
[GOAL]
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
this : HasDerivAt (fun x => id x ^ u) (u * id ↑x ^ (u - 1) * 1) ↑x
⊢ HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < (id ↑x).re
[PROOFSTEP]
simp only [id_eq, mul_one] at this
[GOAL]
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
this : HasDerivAt (fun x => x ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
[PROOFSTEP]
exact this
[GOAL]
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < (id ↑x).re
[PROOFSTEP]
rw [id_eq, ofReal_re]
[GOAL]
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < x
[PROOFSTEP]
exact hx.1
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
[PROOFSTEP]
have V : HasDerivAt (fun y : ℂ => (1 - y) ^ v) (-v * (1 - (x : ℂ)) ^ (v - 1)) ↑x :=
  by
  have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
  swap; · rw [id.def, sub_re, one_re, ofReal_re, sub_pos]; exact hx.2
  simp_rw [id.def] at A
  have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by apply HasDerivAt.const_sub; apply hasDerivAt_id
  convert HasDerivAt.comp (↑x) A B using 1
  ring
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x
[PROOFSTEP]
have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
[GOAL]
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => id x ^ v) (v * id (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < (id (1 - ↑x)).re
[PROOFSTEP]
swap
[GOAL]
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < (id (1 - ↑x)).re
[PROOFSTEP]
rw [id.def, sub_re, one_re, ofReal_re, sub_pos]
[GOAL]
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ x < 1
[PROOFSTEP]
exact hx.2
[GOAL]
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => id x ^ v) (v * id (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x
[PROOFSTEP]
simp_rw [id.def] at A
[GOAL]
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x
[PROOFSTEP]
have B : HasDerivAt (fun y : ℂ => 1 - y) (-1) ↑x := by apply HasDerivAt.const_sub; apply hasDerivAt_id
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y => 1 - y) (-1) ↑x
[PROOFSTEP]
apply HasDerivAt.const_sub
[GOAL]
case hf
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun x => x) 1 ↑x
[PROOFSTEP]
apply hasDerivAt_id
[GOAL]
case refine_2
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
B : HasDerivAt (fun y => 1 - y) (-1) ↑x
⊢ HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x
[PROOFSTEP]
convert HasDerivAt.comp (↑x) A B using 1
[GOAL]
case h.e'_7
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
A : HasDerivAt (fun x => x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
B : HasDerivAt (fun y => 1 - y) (-1) ↑x
⊢ -v * (1 - ↑x) ^ (v - 1) = v * (1 - ↑x) ^ (v - 1) * 1 * -1
[PROOFSTEP]
ring
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
V : HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x
⊢ HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
[PROOFSTEP]
convert (U.mul V).comp_ofReal using 1
[GOAL]
case h.e'_7
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y => y ^ u) (u * ↑x ^ (u - 1)) ↑x
V : HasDerivAt (fun y => (1 - y) ^ v) (-v * (1 - ↑x) ^ (v - 1)) ↑x
⊢ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1)) =
    u * ↑x ^ (u - 1) * (1 - ↑x) ^ v + ↑x ^ u * (-v * (1 - ↑x) ^ (v - 1))
[PROOFSTEP]
ring
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have h_int := ((betaIntegral_convergent hu hv').const_mul u).sub ((betaIntegral_convergent hu' hv).const_mul v)
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int :
  IntervalIntegrable
    (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ (v + 1 - 1)) - v * (↑x ^ (u + 1 - 1) * (1 - ↑x) ^ (v - 1))) volume 0 1
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
rw [add_sub_cancel, add_sub_cancel] at h_int
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have int_ev := intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le zero_le_one hc hder h_int
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have hF0 : F 0 = 0 :=
  by
  simp only [mul_eq_zero, ofReal_zero, cpow_eq_zero_iff, eq_self_iff_true, Ne.def, true_and_iff, sub_zero, one_cpow,
    one_ne_zero, or_false_iff]
  contrapose! hu; rw [hu, zero_re]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
⊢ F 0 = 0
[PROOFSTEP]
simp only [mul_eq_zero, ofReal_zero, cpow_eq_zero_iff, eq_self_iff_true, Ne.def, true_and_iff, sub_zero, one_cpow,
  one_ne_zero, or_false_iff]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
⊢ ¬u = 0
[PROOFSTEP]
contrapose! hu
[GOAL]
u v : ℂ
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hu : u = 0
⊢ u.re ≤ 0
[PROOFSTEP]
rw [hu, zero_re]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hF0 : F 0 = 0
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
have hF1 : F 1 = 0 :=
  by
  simp only [mul_eq_zero, ofReal_one, one_cpow, one_ne_zero, sub_self, cpow_eq_zero_iff, eq_self_iff_true, Ne.def,
    true_and_iff, false_or_iff]
  contrapose! hv; rw [hv, zero_re]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hF0 : F 0 = 0
⊢ F 1 = 0
[PROOFSTEP]
simp only [mul_eq_zero, ofReal_one, one_cpow, one_ne_zero, sub_self, cpow_eq_zero_iff, eq_self_iff_true, Ne.def,
  true_and_iff, false_or_iff]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hF0 : F 0 = 0
⊢ ¬v = 0
[PROOFSTEP]
contrapose! hv
[GOAL]
u v : ℂ
hu : 0 < u.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hF0 : F 0 = 0
hv : v = 0
⊢ v.re ≤ 0
[PROOFSTEP]
rw [hv, zero_re]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
rw [hF0, hF1, sub_zero, intervalIntegral.integral_sub, intervalIntegral.integral_const_mul,
  intervalIntegral.integral_const_mul] at int_ev
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0 ..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v
[PROOFSTEP]
rw [betaIntegral, betaIntegral, ← sub_eq_zero]
[GOAL]
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0 ..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v + 1 - 1)) -
      v * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u + 1 - 1) * (1 - ↑x) ^ (v - 1) =
    0
[PROOFSTEP]
convert int_ev
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_4.h.h.e'_6.h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0 ..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
x✝ : ℝ
⊢ v + 1 - 1 = v
[PROOFSTEP]
ring
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_4.h.h.e'_5.h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0 ..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
x✝ : ℝ
⊢ u + 1 - 1 = u
[PROOFSTEP]
ring
[GOAL]
case hf
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ IntervalIntegrable (fun y => u * (↑y ^ (u - 1) * (1 - ↑y) ^ v)) volume 0 1
[PROOFSTEP]
apply IntervalIntegrable.const_mul
[GOAL]
case hf.hf
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ v) volume 0 1
[PROOFSTEP]
convert betaIntegral_convergent hu hv'
[GOAL]
case h.e'_3.h.h.e'_6.h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
x✝ : ℝ
⊢ v = v + 1 - 1
[PROOFSTEP]
ring
[GOAL]
case hg
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ IntervalIntegrable (fun y => v * (↑y ^ u * (1 - ↑y) ^ (v - 1))) volume 0 1
[PROOFSTEP]
apply IntervalIntegrable.const_mul
[GOAL]
case hg.hf
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ IntervalIntegrable (fun x => ↑x ^ u * (1 - ↑x) ^ (v - 1)) volume 0 1
[PROOFSTEP]
convert betaIntegral_convergent hu' hv
[GOAL]
case h.e'_3.h.h.e'_5.h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ (x : ℝ), x ∈ Ioo 0 1 → HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
x✝ : ℝ
⊢ u = u + 1 - 1
[PROOFSTEP]
ring
[GOAL]
u : ℂ
hu : 0 < u.re
n : ℕ
⊢ betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
[PROOFSTEP]
induction' n with n IH generalizing u
[GOAL]
case zero
u✝ : ℂ
hu✝ : 0 < u✝.re
u : ℂ
hu : 0 < u.re
⊢ betaIntegral u (↑Nat.zero + 1) = ↑Nat.zero ! / ∏ j in Finset.range (Nat.zero + 1), (u + ↑j)
[PROOFSTEP]
rw [Nat.cast_zero, zero_add, betaIntegral_eval_one_right hu, Nat.factorial_zero, Nat.cast_one]
[GOAL]
case zero
u✝ : ℂ
hu✝ : 0 < u✝.re
u : ℂ
hu : 0 < u.re
⊢ 1 / u = 1 / ∏ j in Finset.range (Nat.zero + 1), (u + ↑j)
[PROOFSTEP]
simp
[GOAL]
case succ
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n)! / ∏ j in Finset.range (Nat.succ n + 1), (u + ↑j)
[PROOFSTEP]
have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u * betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n)
⊢ betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n)! / ∏ j in Finset.range (Nat.succ n + 1), (u + ↑j)
case succ.refine_1
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < (↑(Nat.succ n)).re
[PROOFSTEP]
swap
[GOAL]
case succ.refine_1
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < (↑(Nat.succ n)).re
[PROOFSTEP]
rw [← ofReal_nat_cast, ofReal_re]
[GOAL]
case succ.refine_1
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < ↑(Nat.succ n)
[PROOFSTEP]
positivity
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u * betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n)
⊢ betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n)! / ∏ j in Finset.range (Nat.succ n + 1), (u + ↑j)
[PROOFSTEP]
rw [mul_comm u _, ← eq_div_iff] at this
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n)! / ∏ j in Finset.range (Nat.succ n + 1), (u + ↑j)
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) * u = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n)
⊢ u ≠ 0
[PROOFSTEP]
swap
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) * u = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n)
⊢ u ≠ 0
[PROOFSTEP]
contrapose! hu
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
this : betaIntegral u (↑(Nat.succ n) + 1) * u = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n)
hu : u = 0
⊢ u.re ≤ 0
[PROOFSTEP]
rw [hu, zero_re]
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n)! / ∏ j in Finset.range (Nat.succ n + 1), (u + ↑j)
[PROOFSTEP]
rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ (↑n + 1) * (↑n ! / ∏ j in Finset.range (n + 1), (u + 1 + ↑j)) / u =
    ↑(Nat.succ n)! / ((∏ k in Finset.range (n + 1), (u + ↑(k + 1))) * (u + ↑0))
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ 0 < (u + 1).re
[PROOFSTEP]
swap
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ 0 < (u + 1).re
[PROOFSTEP]
rw [add_re, one_re]
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ 0 < u.re + 1
[PROOFSTEP]
positivity
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ (↑n + 1) * (↑n ! / ∏ j in Finset.range (n + 1), (u + 1 + ↑j)) / u =
    ↑(Nat.succ n)! / ((∏ k in Finset.range (n + 1), (u + ↑(k + 1))) * (u + ↑0))
[PROOFSTEP]
rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_zero, add_zero, ← mul_div_assoc, ← div_div]
[GOAL]
case succ.refine_2
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
⊢ ((↑n + 1) * ↑n ! / ∏ j in Finset.range (n + 1), (u + 1 + ↑j)) / u =
    ((↑n + 1) * ↑n ! / ∏ k in Finset.range (n + 1), (u + ↑(k + 1))) / u
[PROOFSTEP]
congr 3 with j : 1
[GOAL]
case succ.refine_2.e_a.e_a.e_f.h
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
j : ℕ
⊢ u + 1 + ↑j = u + ↑(j + 1)
[PROOFSTEP]
push_cast
[GOAL]
case succ.refine_2.e_a.e_a.e_f.h
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
j : ℕ
⊢ u + 1 + ↑j = u + (↑j + 1)
[PROOFSTEP]
abel
[GOAL]
case succ.refine_2.e_a.e_a.e_f.h
u✝ : ℂ
hu✝ : 0 < u✝.re
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → betaIntegral u (↑n + 1) = ↑n ! / ∏ j in Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : betaIntegral u (↑(Nat.succ n) + 1) = ↑(Nat.succ n) * betaIntegral (u + 1) ↑(Nat.succ n) / u
j : ℕ
⊢ u + 1 + ↑j = u + (↑j + 1)
[PROOFSTEP]
abel
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
⊢ GammaSeq s n = ↑n ^ s * betaIntegral s (↑n + 1)
[PROOFSTEP]
rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ GammaSeq (s + 1) n / s = ↑n / (↑n + 1 + s) * GammaSeq s n
[PROOFSTEP]
conv_lhs => rw [GammaSeq, Finset.prod_range_succ, div_div]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
| GammaSeq (s + 1) n / s
[PROOFSTEP]
rw [GammaSeq, Finset.prod_range_succ, div_div]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
| GammaSeq (s + 1) n / s
[PROOFSTEP]
rw [GammaSeq, Finset.prod_range_succ, div_div]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
| GammaSeq (s + 1) n / s
[PROOFSTEP]
rw [GammaSeq, Finset.prod_range_succ, div_div]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) * ↑n ! / ((∏ x in Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) = ↑n / (↑n + 1 + s) * GammaSeq s n
[PROOFSTEP]
conv_rhs =>
  rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc, ← mul_assoc,
    mul_comm _ (Finset.prod _ _)]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n / (↑n + 1 + s) * GammaSeq s n
[PROOFSTEP]
rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc, ← mul_assoc,
    mul_comm _ (Finset.prod _ _)]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n / (↑n + 1 + s) * GammaSeq s n
[PROOFSTEP]
rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc, ← mul_assoc,
    mul_comm _ (Finset.prod _ _)]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n / (↑n + 1 + s) * GammaSeq s n
[PROOFSTEP]
rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc, ← mul_assoc,
  mul_comm _ (Finset.prod _ _)]
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) * ↑n ! / ((∏ x in Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) =
    ↑n * ↑n ^ s * ↑n ! / ((∏ k in Finset.range n, (s + ↑(k + 1))) * (↑n + 1 + s) * s)
[PROOFSTEP]
congr 3
[GOAL]
case e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) = ↑n * ↑n ^ s
[PROOFSTEP]
rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]
[GOAL]
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∏ x in Finset.range n, (s + 1 + ↑x) = ∏ k in Finset.range n, (s + ↑(k + 1))
[PROOFSTEP]
refine' Finset.prod_congr (by rfl) fun x _ => _
[GOAL]
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ Finset.range n = Finset.range n
[PROOFSTEP]
rfl
[GOAL]
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
x✝ : x ∈ Finset.range n
⊢ s + 1 + ↑x = s + ↑(x + 1)
[PROOFSTEP]
push_cast
[GOAL]
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
x✝ : x ∈ Finset.range n
⊢ s + 1 + ↑x = s + (↑x + 1)
[PROOFSTEP]
ring
[GOAL]
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s
[PROOFSTEP]
abel
[GOAL]
case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s
[PROOFSTEP]
abel
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ GammaSeq s n = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
[PROOFSTEP]
have : ∀ x : ℝ, x = x / n * n := by intro x; rw [div_mul_cancel]; exact Nat.cast_ne_zero.mpr hn
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ ∀ (x : ℝ), x = x / ↑n * ↑n
[PROOFSTEP]
intro x
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ x = x / ↑n * ↑n
[PROOFSTEP]
rw [div_mul_cancel]
[GOAL]
case h
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ ↑n ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.mpr hn
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
⊢ GammaSeq s n = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
[PROOFSTEP]
conv_rhs => enter [1, x, 2, 1]; rw [this x]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
| ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
[PROOFSTEP]
enter [1, x, 2, 1]; rw [this x]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
| ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
[PROOFSTEP]
enter [1, x, 2, 1]; rw [this x]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
| ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
[PROOFSTEP]
enter [1, x, 2, 1]
[GOAL]
case h
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
x : ℝ
| ↑x
[PROOFSTEP]
rw [this x]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
⊢ GammaSeq s n = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
[PROOFSTEP]
rw [GammaSeq_eq_betaIntegral_of_re_pos hs]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
⊢ ↑n ^ s * betaIntegral s (↑n + 1) = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
[PROOFSTEP]
have :=
  intervalIntegral.integral_comp_div (a := 0) (b := n) (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1) : ℝ → ℂ)
    (Nat.cast_ne_zero.mpr hn)
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)) (x / ↑n) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)) x
⊢ ↑n ^ s * betaIntegral s (↑n + 1) = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
[PROOFSTEP]
dsimp only at this
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ^ s * betaIntegral s (↑n + 1) = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
[PROOFSTEP]
rw [betaIntegral, this, real_smul, zero_div, div_self, add_sub_cancel, ← intervalIntegral.integral_const_mul, ←
  intervalIntegral.integral_const_mul]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) =
    ∫ (x : ℝ) in 0 ..1, ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1))
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ≠ 0
[PROOFSTEP]
swap
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.mpr hn
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ∫ (x : ℝ) in 0 ..1, ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) =
    ∫ (x : ℝ) in 0 ..1, ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1))
[PROOFSTEP]
simp_rw [intervalIntegral.integral_of_le zero_le_one]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioc 0 1, ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) =
    ∫ (x : ℝ) in Ioc 0 1, ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1))
[PROOFSTEP]
refine' set_integral_congr measurableSet_Ioc fun x hx => _
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
⊢ ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1))
[PROOFSTEP]
push_cast
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
⊢ ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
[PROOFSTEP]
have hn' : (n : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr hn
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
⊢ ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
[PROOFSTEP]
have A : (n : ℂ) ^ s = (n : ℂ) ^ (s - 1) * n :=
  by
  conv_lhs => rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
  simp
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
⊢ ↑n ^ s = ↑n ^ (s - 1) * ↑n
[PROOFSTEP]
conv_lhs => rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
| ↑n ^ s
[PROOFSTEP]
rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
| ↑n ^ s
[PROOFSTEP]
rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
| ↑n ^ s
[PROOFSTEP]
rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
⊢ s = s - 1 + 1
[PROOFSTEP]
ring
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
⊢ ↑n ^ (s - 1) * ↑n ^ 1 = ↑n ^ (s - 1) * ↑n
[PROOFSTEP]
simp
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
A : ↑n ^ s = ↑n ^ (s - 1) * ↑n
⊢ ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
[PROOFSTEP]
have B : ((x : ℂ) * ↑n) ^ (s - 1) = (x : ℂ) ^ (s - 1) * (n : ℂ) ^ (s - 1) := by
  rw [← ofReal_nat_cast, mul_cpow_ofReal_nonneg hx.1.le (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)).le]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
A : ↑n ^ s = ↑n ^ (s - 1) * ↑n
⊢ (↑x * ↑n) ^ (s - 1) = ↑x ^ (s - 1) * ↑n ^ (s - 1)
[PROOFSTEP]
rw [← ofReal_nat_cast, mul_cpow_ofReal_nonneg hx.1.le (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)).le]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
A : ↑n ^ s = ↑n ^ (s - 1) * ↑n
B : (↑x * ↑n) ^ (s - 1) = ↑x ^ (s - 1) * ↑n ^ (s - 1)
⊢ ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
[PROOFSTEP]
rw [A, B, cpow_nat_cast]
[GOAL]
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
A : ↑n ^ s = ↑n ^ (s - 1) * ↑n
B : (↑x * ↑n) ^ (s - 1) = ↑x ^ (s - 1) * ↑n ^ (s - 1)
⊢ ↑n ^ (s - 1) * ↑n * (↑x ^ (s - 1) * (1 - ↑x) ^ n) = ↑n * ((1 - ↑x) ^ n * (↑x ^ (s - 1) * ↑n ^ (s - 1)))
[PROOFSTEP]
ring
[GOAL]
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (Gamma s))
[PROOFSTEP]
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)`.
[GOAL]
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (GammaIntegral s))
[PROOFSTEP]
let f : ℕ → ℝ → ℂ := fun n =>
  indicator (Ioc 0 (n : ℝ)) fun x : ℝ =>
    ↑((1 - x / n) ^ n) *
      (x : ℂ) ^
        (s - 1)
          -- integrability of f
[GOAL]
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n => indicator (Ioc 0 ↑n) fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
⊢ Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (GammaIntegral s))
[PROOFSTEP]
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_integrable_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
    exact
      IsROrC.continuous_ofReal.comp
        ((continuous_const.sub (continuous_id'.div_const ↑n)).pow n)
          -- pointwise limit of f
[GOAL]
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n => indicator (Ioc 0 ↑n) fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
⊢ ∀ (n : ℕ), Integrable (f n)
[PROOFSTEP]
intro n
[GOAL]
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n => indicator (Ioc 0 ↑n) fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ Integrable (f n)
[PROOFSTEP]
rw [integrable_indicator_iff (measurableSet_Ioc : MeasurableSet (Ioc (_ : ℝ) _)), IntegrableOn,
  Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self, ← IntegrableOn, ←
  intervalIntegrable_iff_integrable_Ioc_of_le (by positivity : (0 : ℝ) ≤ n)]
[GOAL]
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n => indicator (Ioc 0 ↑n) fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ 0 ≤ ↑n
[PROOFSTEP]
positivity
[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 => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) volume 0 ↑n
[PROOFSTEP]
apply IntervalIntegrable.continuousOn_mul
[GOAL]
case hf
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
[PROOFSTEP]
refine' intervalIntegral.intervalIntegrable_cpow' _
[GOAL]
case hf
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n => indicator (Ioc 0 ↑n) fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ -1 < (s - 1).re
[PROOFSTEP]
rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
[GOAL]
case hg
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n => indicator (Ioc 0 ↑n) fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ ContinuousOn (fun x => ↑((1 - x / ↑n) ^ n)) (uIcc 0 ↑n)
[PROOFSTEP]
apply Continuous.continuousOn
[GOAL]
case hg.h
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n => indicator (Ioc 0 ↑n) fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ Continuous fun x => ↑((1 - x / ↑n) ^ n)
[PROOFSTEP]
exact
  IsROrC.continuous_ofReal.comp
    ((continuous_const.sub (continuous_id'.div_const ↑n)).pow n)
      -- pointwise limit of f
[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 (f n)
⊢ Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (GammaIntegral s))
[PROOFSTEP]
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'
  show ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x
  · refine' Eventually.mp (eventually_ge_atTop ⌈x⌉₊) (eventually_of_forall fun n hn => _)
    rw [Nat.ceil_le] at hn
    dsimp only
    rw [indicator_of_mem]
    exact ⟨hx, hn⟩
  · simp_rw [mul_comm]
    refine' (Tendsto.comp (continuous_ofReal.tendsto _) _).const_mul _
    convert tendsto_one_plus_div_pow_exp (-x) using 1
    ext1 n
    rw [neg_div, ← sub_eq_add_neg];
    norm_cast
      -- let `convert` identify the remaining goals
[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 (f n)
⊢ ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
[PROOFSTEP]
intro x hx
[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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
[PROOFSTEP]
apply Tendsto.congr'
[GOAL]
case hl
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ ?f₁ =ᶠ[atTop] fun n => f n x
case h
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto ?f₁ atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
case f₁
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ ℕ → ℂ
[PROOFSTEP]
show ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x
[GOAL]
case hl
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) = f n x
[PROOFSTEP]
refine' Eventually.mp (eventually_ge_atTop ⌈x⌉₊) (eventually_of_forall fun n hn => _)
[GOAL]
case hl
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
hn : ⌈x⌉₊ ≤ n
⊢ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) = f n x
[PROOFSTEP]
rw [Nat.ceil_le] at hn
[GOAL]
case hl
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
hn : x ≤ ↑n
⊢ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) = f n x
[PROOFSTEP]
dsimp only
[GOAL]
case hl
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
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
[PROOFSTEP]
rw [indicator_of_mem]
[GOAL]
case hl.h
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
hn : x ≤ ↑n
⊢ x ∈ Ioc 0 ↑n
[PROOFSTEP]
exact ⟨hx, hn⟩
[GOAL]
case h
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto (fun x_1 => ↑((1 - x / ↑x_1) ^ x_1) * ↑x ^ (s - 1)) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
case h
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto (fun x_1 => ↑x ^ (s - 1) * ↑((1 - x / ↑x_1) ^ x_1)) atTop (𝓝 (↑x ^ (s - 1) * ↑(rexp (-x))))
[PROOFSTEP]
refine' (Tendsto.comp (continuous_ofReal.tendsto _) _).const_mul _
[GOAL]
case h
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ Tendsto (fun x_1 => (1 - x / ↑x_1) ^ x_1) atTop (𝓝 (rexp (-x)))
[PROOFSTEP]
convert tendsto_one_plus_div_pow_exp (-x) using 1
[GOAL]
case h.e'_3
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x_1 => (1 - x / ↑x_1) ^ x_1) = fun x_1 => (1 + -x / ↑x_1) ^ ↑x_1
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_3.h
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
⊢ (1 - x / ↑n) ^ n = (1 + -x / ↑n) ^ ↑n
[PROOFSTEP]
rw [neg_div, ← sub_eq_add_neg]
[GOAL]
case h.e'_3.h
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 (f n)
x : ℝ
hx : x ∈ Ioi 0
n : ℕ
⊢ (1 - x / ↑n) ^ n = (1 - x / ↑n) ^ ↑n
[PROOFSTEP]
norm_cast
  -- let `convert` identify the remaining goals
[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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → 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 (𝓝 (GammaIntegral s))
[PROOFSTEP]
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
[GOAL]
case h.e'_3
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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) = fun n => ∫ (a : ℝ) in Ioi 0, f n a
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_3.h
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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) = ∫ (a : ℝ) in Ioi 0, f n a
[PROOFSTEP]
rw [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
[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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
⊢ 0 ≤ ↑n
[PROOFSTEP]
positivity
[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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → 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)
[PROOFSTEP]
intro n
[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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → 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)
[PROOFSTEP]
refine' (ae_restrict_iff' measurableSet_Ioi).mpr (ae_of_all _ fun x hx => _)
[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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖f n x‖ ≤ rexp (-x) * x ^ (s.re - 1)
[PROOFSTEP]
dsimp only
[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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖indicator (Ioc 0 ↑n) (fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)
[PROOFSTEP]
rcases lt_or_le (n : ℝ) x with (hxn | hxn)
[GOAL]
case inl
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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : x ∈ Ioi 0
hxn : ↑n < x
⊢ ‖indicator (Ioc 0 ↑n) (fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)
[PROOFSTEP]
rw [indicator_of_not_mem (not_mem_Ioc_of_gt hxn), norm_zero, mul_nonneg_iff_right_nonneg_of_pos (exp_pos _)]
[GOAL]
case inl
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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : x ∈ Ioi 0
hxn : ↑n < x
⊢ 0 ≤ x ^ (s.re - 1)
[PROOFSTEP]
exact rpow_nonneg_of_nonneg (le_of_lt hx) _
[GOAL]
case inr
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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : x ∈ Ioi 0
hxn : x ≤ ↑n
⊢ ‖indicator (Ioc 0 ↑n) (fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)
[PROOFSTEP]
rw [indicator_of_mem (mem_Ioc.mpr ⟨mem_Ioi.mp hx, hxn⟩), norm_mul, Complex.norm_eq_abs,
  Complex.abs_of_nonneg (pow_nonneg (sub_nonneg.mpr <| div_le_one_of_le hxn <| by positivity) _), Complex.norm_eq_abs,
  abs_cpow_eq_rpow_re_of_pos hx, sub_re, one_re, mul_le_mul_right (rpow_pos_of_pos hx _)]
[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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : x ∈ Ioi 0
hxn : x ≤ ↑n
⊢ 0 ≤ ↑n
[PROOFSTEP]
positivity
[GOAL]
case inr
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 (f n)
f_tends : ∀ (x : ℝ), x ∈ Ioi 0 → Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : x ∈ Ioi 0
hxn : x ≤ ↑n
⊢ (1 - x / ↑n) ^ n ≤ rexp (-x)
[PROOFSTEP]
exact one_sub_div_pow_le_exp_neg hxn
[GOAL]
s : ℂ
⊢ Tendsto (GammaSeq s) atTop (𝓝 (Gamma s))
[PROOFSTEP]
suffices ∀ m : ℕ, -↑m < re s → Tendsto (GammaSeq s) atTop (𝓝 <| GammaAux m s)
  by
  rw [Gamma]
  apply this
  rw [neg_lt]
  rcases lt_or_le 0 (re s) with (hs | hs)
  · exact (neg_neg_of_pos hs).trans_le (Nat.cast_nonneg _)
  · refine' (Nat.lt_floor_add_one _).trans_le _
    rw [sub_eq_neg_add, Nat.floor_add_one (neg_nonneg.mpr hs), Nat.cast_add_one]
[GOAL]
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
⊢ Tendsto (GammaSeq s) atTop (𝓝 (Gamma s))
[PROOFSTEP]
rw [Gamma]
[GOAL]
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
⊢ Tendsto (GammaSeq s) atTop (𝓝 (GammaAux ⌊1 - s.re⌋₊ s))
[PROOFSTEP]
apply this
[GOAL]
case a
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
⊢ -↑⌊1 - s.re⌋₊ < s.re
[PROOFSTEP]
rw [neg_lt]
[GOAL]
case a
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
⊢ -s.re < ↑⌊1 - s.re⌋₊
[PROOFSTEP]
rcases lt_or_le 0 (re s) with (hs | hs)
[GOAL]
case a.inl
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
hs : 0 < s.re
⊢ -s.re < ↑⌊1 - s.re⌋₊
[PROOFSTEP]
exact (neg_neg_of_pos hs).trans_le (Nat.cast_nonneg _)
[GOAL]
case a.inr
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
hs : s.re ≤ 0
⊢ -s.re < ↑⌊1 - s.re⌋₊
[PROOFSTEP]
refine' (Nat.lt_floor_add_one _).trans_le _
[GOAL]
case a.inr
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
hs : s.re ≤ 0
⊢ ↑⌊-s.re⌋₊ + 1 ≤ ↑⌊1 - s.re⌋₊
[PROOFSTEP]
rw [sub_eq_neg_add, Nat.floor_add_one (neg_nonneg.mpr hs), Nat.cast_add_one]
[GOAL]
s : ℂ
⊢ ∀ (m : ℕ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
[PROOFSTEP]
intro m
[GOAL]
s : ℂ
m : ℕ
⊢ -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
[PROOFSTEP]
induction' m with m IH generalizing s
[GOAL]
case zero
s✝ s : ℂ
⊢ -↑Nat.zero < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux Nat.zero s))
[PROOFSTEP]
intro hs
[GOAL]
case zero
s✝ s : ℂ
hs : -↑Nat.zero < s.re
⊢ Tendsto (GammaSeq s) atTop (𝓝 (GammaAux Nat.zero s))
[PROOFSTEP]
rw [Nat.cast_zero, neg_zero] at hs
[GOAL]
case zero
s✝ s : ℂ
hs : 0 < s.re
⊢ Tendsto (GammaSeq s) atTop (𝓝 (GammaAux Nat.zero s))
[PROOFSTEP]
rw [← Gamma_eq_GammaAux]
[GOAL]
case zero
s✝ s : ℂ
hs : 0 < s.re
⊢ Tendsto (GammaSeq s) atTop (𝓝 (Gamma s))
[PROOFSTEP]
refine' Tendsto.congr' _ (approx_Gamma_integral_tendsto_Gamma_integral hs)
[GOAL]
case zero
s✝ s : ℂ
hs : 0 < s.re
⊢ (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) =ᶠ[atTop] GammaSeq s
[PROOFSTEP]
refine' (eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => _)
[GOAL]
case zero
s✝ s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) n = GammaSeq s n
[PROOFSTEP]
exact (GammaSeq_eq_approx_Gamma_integral hs hn).symm
[GOAL]
case zero.h1
s✝ s : ℂ
hs : 0 < s.re
⊢ -s.re < ↑Nat.zero
[PROOFSTEP]
rwa [Nat.cast_zero, neg_lt_zero]
[GOAL]
case succ
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
⊢ -↑(Nat.succ m) < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux (Nat.succ m) s))
[PROOFSTEP]
intro hs
[GOAL]
case succ
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑(Nat.succ m) < s.re
⊢ Tendsto (GammaSeq s) atTop (𝓝 (GammaAux (Nat.succ m) s))
[PROOFSTEP]
rw [Nat.cast_succ, neg_add, ← sub_eq_add_neg, sub_lt_iff_lt_add, ← one_re, ← add_re] at hs
[GOAL]
case succ
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ Tendsto (GammaSeq s) atTop (𝓝 (GammaAux (Nat.succ m) s))
[PROOFSTEP]
rw [GammaAux]
[GOAL]
case succ
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ Tendsto (GammaSeq s) atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))
[PROOFSTEP]
have :=
  @Tendsto.congr' _ _ _ ?_ _ _ ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => ?_))
    ((IH _ hs).div_const s)
[GOAL]
case succ.refine_3
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto ?succ.refine_1 atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto (GammaSeq s) atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))
case succ.refine_1
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ ℕ → ℂ
case succ.refine_2
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
n : ℕ
hn : n ≠ 0
⊢ GammaSeq (s + 1) n / s = ?succ.refine_1 n
[PROOFSTEP]
pick_goal 3
[GOAL]
case succ.refine_2
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
n : ℕ
hn : n ≠ 0
⊢ GammaSeq (s + 1) n / s = ?succ.refine_1 n
[PROOFSTEP]
exact GammaSeq_add_one_left s hn
[GOAL]
case succ.refine_3
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto (GammaSeq s) atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))
[PROOFSTEP]
conv at this => arg 1; intro n; rw [mul_comm]
[GOAL]
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
| Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
[PROOFSTEP]
arg 1; intro n; rw [mul_comm]
[GOAL]
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
| Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
[PROOFSTEP]
arg 1; intro n; rw [mul_comm]
[GOAL]
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
| Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
[PROOFSTEP]
arg 1
[GOAL]
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
| fun n => ↑n / (↑n + 1 + s) * GammaSeq s n
[PROOFSTEP]
intro n
[GOAL]
case h
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => ↑n / (↑n + 1 + s) * GammaSeq s n) atTop (𝓝 (GammaAux m (s + 1) / s))
n : ℕ
| ↑n / (↑n + 1 + s) * GammaSeq s n
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case succ.refine_3
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => GammaSeq s n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto (GammaSeq s) atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))
[PROOFSTEP]
rwa [← mul_one (GammaAux m (s + 1) / s), tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
[GOAL]
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => GammaSeq s n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s * 1))
⊢ Tendsto (fun n => ↑n / (↑n + 1 + s)) atTop (𝓝 1)
[PROOFSTEP]
simp_rw [add_assoc]
[GOAL]
s✝ : ℂ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto (GammaSeq s) atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => GammaSeq s n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s * 1))
⊢ Tendsto (fun n => ↑n / (↑n + (1 + s))) atTop (𝓝 1)
[PROOFSTEP]
exact tendsto_coe_nat_div_add_atTop (1 + s)
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
⊢ GammaSeq z n * GammaSeq (1 - z) n = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
[PROOFSTEP]
have aux : ∀ a b c d : ℂ, a * b * (c * d) = a * c * (b * d) := by intros; ring
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
[PROOFSTEP]
intros
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
a✝ b✝ c✝ d✝ : ℂ
⊢ a✝ * b✝ * (c✝ * d✝) = a✝ * c✝ * (b✝ * d✝)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ GammaSeq z n * GammaSeq (1 - z) n = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
[PROOFSTEP]
rw [GammaSeq, GammaSeq, div_mul_div_comm, aux, ← pow_two]
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ ↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 /
      ((∏ j in Finset.range (n + 1), (z + ↑j)) * ∏ j in Finset.range (n + 1), (1 - z + ↑j)) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
[PROOFSTEP]
have : (n : ℂ) ^ z * (n : ℂ) ^ (1 - z) = n := by
  rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel'_right, cpow_one]
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ ↑n ^ z * ↑n ^ (1 - z) = ↑n
[PROOFSTEP]
rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel'_right, cpow_one]
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
⊢ ↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 /
      ((∏ j in Finset.range (n + 1), (z + ↑j)) * ∏ j in Finset.range (n + 1), (1 - z + ↑j)) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
[PROOFSTEP]
rw [this, Finset.prod_range_succ', Finset.prod_range_succ, aux, ← Finset.prod_mul_distrib, Nat.cast_zero, add_zero,
  add_comm (1 - z) n, ← add_sub_assoc]
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
⊢ ↑n * ↑n ! ^ 2 / ((∏ x in Finset.range n, (z + ↑(x + 1)) * (1 - z + ↑x)) * (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
[PROOFSTEP]
have : ∀ j : ℕ, (z + ↑(j + 1)) * (↑1 - z + ↑j) = ↑((j + 1) ^ 2) * (↑1 - z ^ 2 / ((j : ℂ) + 1) ^ 2) :=
  by
  intro j
  push_cast
  have : (j : ℂ) + 1 ≠ 0 := by rw [← Nat.cast_succ, Nat.cast_ne_zero]; exact Nat.succ_ne_zero j
  field_simp; ring
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
⊢ ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
[PROOFSTEP]
intro j
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
⊢ (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
[PROOFSTEP]
push_cast
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
⊢ (z + (↑j + 1)) * (1 - z + ↑j) = (↑j + 1) ^ 2 * (1 - z ^ 2 / (↑j + 1) ^ 2)
[PROOFSTEP]
have : (j : ℂ) + 1 ≠ 0 := by rw [← Nat.cast_succ, Nat.cast_ne_zero]; exact Nat.succ_ne_zero j
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
⊢ ↑j + 1 ≠ 0
[PROOFSTEP]
rw [← Nat.cast_succ, Nat.cast_ne_zero]
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
⊢ Nat.succ j ≠ 0
[PROOFSTEP]
exact Nat.succ_ne_zero j
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
this : ↑j + 1 ≠ 0
⊢ (z + (↑j + 1)) * (1 - z + ↑j) = (↑j + 1) ^ 2 * (1 - z ^ 2 / (↑j + 1) ^ 2)
[PROOFSTEP]
field_simp
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
j : ℕ
this : ↑j + 1 ≠ 0
⊢ (z + (↑j + 1)) * (1 - z + ↑j) * (↑j + 1) ^ 2 = (↑j + 1) ^ 2 * ((↑j + 1) ^ 2 - z ^ 2)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n * ↑n ! ^ 2 / ((∏ x in Finset.range n, (z + ↑(x + 1)) * (1 - z + ↑x)) * (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
[PROOFSTEP]
simp_rw [this]
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n * ↑n ! ^ 2 / ((∏ x in Finset.range n, ↑((x + 1) ^ 2) * (1 - z ^ 2 / (↑x + 1) ^ 2)) * (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
[PROOFSTEP]
rw [Finset.prod_mul_distrib, ← Nat.cast_prod, Finset.prod_pow, Finset.prod_range_add_one_eq_factorial, Nat.cast_pow,
  (by intros; ring : ∀ a b c d : ℂ, a * b * (c * d) = a * (d * (b * c))), ← div_div, mul_div_cancel, ← div_div,
  mul_comm z _, mul_one_div]
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ∀ (a b c d : ℂ), a * b * (c * d) = a * (d * (b * c))
[PROOFSTEP]
intros
[GOAL]
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
a✝ b✝ c✝ d✝ : ℂ
⊢ a✝ * b✝ * (c✝ * d✝) = a✝ * (d✝ * (b✝ * c✝))
[PROOFSTEP]
ring
[GOAL]
case h
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n ! ^ 2 ≠ 0
[PROOFSTEP]
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr <| Nat.factorial_ne_zero n)
[GOAL]
z : ℂ
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
[PROOFSTEP]
have pi_ne : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr pi_ne_zero
[GOAL]
z : ℂ
pi_ne : ↑π ≠ 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
[PROOFSTEP]
by_cases hs : sin (↑π * z) = 0
[GOAL]
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
[PROOFSTEP]
rw [hs, div_zero]
[GOAL]
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = 0
[PROOFSTEP]
rw [← neg_eq_zero, ← Complex.sin_neg, ← mul_neg, Complex.sin_eq_zero_iff, mul_comm] at hs
[GOAL]
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : ∃ k, -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0
[PROOFSTEP]
obtain ⟨k, hk⟩ := hs
[GOAL]
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0
[PROOFSTEP]
rw [mul_eq_mul_right_iff, eq_false (ofReal_ne_zero.mpr pi_pos.ne'), or_false_iff, neg_eq_iff_eq_neg] at hk
[GOAL]
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma z * Gamma (1 - z) = 0
[PROOFSTEP]
rw [hk]
[GOAL]
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma (-↑k) * Gamma (1 - -↑k) = 0
[PROOFSTEP]
cases k
[GOAL]
case pos.intro.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ Gamma (-↑(Int.ofNat a✝)) * Gamma (1 - -↑(Int.ofNat a✝)) = 0
[PROOFSTEP]
rw [Int.ofNat_eq_coe, Int.cast_ofNat, Complex.Gamma_neg_nat_eq_zero, zero_mul]
[GOAL]
case pos.intro.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ Gamma (-↑(Int.negSucc a✝)) * Gamma (1 - -↑(Int.negSucc a✝)) = 0
[PROOFSTEP]
rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel', Complex.Gamma_neg_nat_eq_zero,
  mul_zero]
[GOAL]
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
[PROOFSTEP]
refine' tendsto_nhds_unique ((GammaSeq_tendsto_Gamma z).mul (GammaSeq_tendsto_Gamma <| 1 - z)) _
[GOAL]
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Tendsto (fun x => GammaSeq z x * GammaSeq (1 - z) x) atTop (𝓝 (↑π / sin (↑π * z)))
[PROOFSTEP]
have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul]
[GOAL]
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
[PROOFSTEP]
rw [one_mul]
[GOAL]
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun x => GammaSeq z x * GammaSeq (1 - z) x) atTop (𝓝 (↑π / sin (↑π * z)))
[PROOFSTEP]
convert
  Tendsto.congr' ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => (GammaSeq_mul z hn).symm))
    (Tendsto.mul _ _)
[GOAL]
case neg.convert_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n => ↑n / (↑n + 1 - z)) atTop (𝓝 1)
[PROOFSTEP]
convert tendsto_coe_nat_div_add_atTop (1 - z) using 1
[GOAL]
case h.e'_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ (fun n => ↑n / (↑n + 1 - z)) = fun n => ↑n / (↑n + (1 - z))
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_3.h
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
n : ℕ
⊢ ↑n / (↑n + 1 - z) = ↑n / (↑n + (1 - z))
[PROOFSTEP]
rw [add_sub_assoc]
[GOAL]
case neg.convert_4
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n => 1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))
[PROOFSTEP]
have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by field_simp
[GOAL]
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
[PROOFSTEP]
field_simp
[GOAL]
case neg.convert_4
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n => 1 / (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))
[PROOFSTEP]
convert tendsto_const_nhds.div _ (div_ne_zero hs pi_ne)
[GOAL]
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun x => z * ∏ j in Finset.range x, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (sin (↑π * z) / ↑π))
[PROOFSTEP]
rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel _ pi_ne]
[GOAL]
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n => (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) atTop (𝓝 (sin (↑π * z)))
[PROOFSTEP]
convert tendsto_euler_sin_prod z using 1
[GOAL]
case h.e'_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ (fun n => (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) = fun n =>
    ↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_3.h
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
n : ℕ
⊢ (z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π =
    ↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
[PROOFSTEP]
rw [mul_comm, ← mul_assoc]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ Gamma s ≠ 0
[PROOFSTEP]
by_cases h_im : s.im = 0
[GOAL]
case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
⊢ Gamma s ≠ 0
[PROOFSTEP]
have : s = ↑s.re := by
  conv_lhs => rw [← Complex.re_add_im s]
  rw [h_im, ofReal_zero, zero_mul, add_zero]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
⊢ s = ↑s.re
[PROOFSTEP]
conv_lhs => rw [← Complex.re_add_im s]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
| s
[PROOFSTEP]
rw [← Complex.re_add_im s]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
| s
[PROOFSTEP]
rw [← Complex.re_add_im s]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
| s
[PROOFSTEP]
rw [← Complex.re_add_im s]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
⊢ ↑s.re + ↑s.im * I = ↑s.re
[PROOFSTEP]
rw [h_im, ofReal_zero, zero_mul, add_zero]
[GOAL]
case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
⊢ Gamma s ≠ 0
[PROOFSTEP]
rw [this, Gamma_ofReal, ofReal_ne_zero]
[GOAL]
case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
⊢ Real.Gamma s.re ≠ 0
[PROOFSTEP]
refine' Real.Gamma_ne_zero fun n => _
[GOAL]
case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
⊢ s.re ≠ -↑n
[PROOFSTEP]
specialize hs n
[GOAL]
case pos
s : ℂ
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
hs : s ≠ -↑n
⊢ s.re ≠ -↑n
[PROOFSTEP]
contrapose! hs
[GOAL]
case pos
s : ℂ
h_im : s.im = 0
this : s = ↑s.re
n : ℕ
hs : s.re = -↑n
⊢ s = -↑n
[PROOFSTEP]
rwa [this, ← ofReal_nat_cast, ← ofReal_neg, ofReal_inj]
[GOAL]
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
⊢ Gamma s ≠ 0
[PROOFSTEP]
have : sin (↑π * s) ≠ 0 := by
  rw [Complex.sin_ne_zero_iff]
  intro k
  apply_fun im
  rw [ofReal_mul_im, ← ofReal_int_cast, ← ofReal_mul, ofReal_im]
  exact mul_ne_zero Real.pi_pos.ne' h_im
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
⊢ sin (↑π * s) ≠ 0
[PROOFSTEP]
rw [Complex.sin_ne_zero_iff]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
⊢ ∀ (k : ℤ), ↑π * s ≠ ↑k * ↑π
[PROOFSTEP]
intro k
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ ↑π * s ≠ ↑k * ↑π
[PROOFSTEP]
apply_fun im
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ (↑π * s).im ≠ (↑k * ↑π).im
[PROOFSTEP]
rw [ofReal_mul_im, ← ofReal_int_cast, ← ofReal_mul, ofReal_im]
[GOAL]
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ 0
[PROOFSTEP]
exact mul_ne_zero Real.pi_pos.ne' h_im
[GOAL]
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
⊢ Gamma s ≠ 0
[PROOFSTEP]
have A := div_ne_zero (ofReal_ne_zero.mpr Real.pi_pos.ne') this
[GOAL]
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : ↑π / sin (↑π * s) ≠ 0
⊢ Gamma s ≠ 0
[PROOFSTEP]
rw [← Complex.Gamma_mul_Gamma_one_sub s, mul_ne_zero_iff] at A
[GOAL]
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0
[PROOFSTEP]
exact A.1
[GOAL]
s : ℂ
⊢ Gamma s = 0 ↔ ∃ m, s = -↑m
[PROOFSTEP]
constructor
[GOAL]
case mp
s : ℂ
⊢ Gamma s = 0 → ∃ m, s = -↑m
[PROOFSTEP]
contrapose!
[GOAL]
case mp
s : ℂ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0
[PROOFSTEP]
exact Gamma_ne_zero
[GOAL]
case mpr
s : ℂ
⊢ (∃ m, s = -↑m) → Gamma s = 0
[PROOFSTEP]
rintro ⟨m, rfl⟩
[GOAL]
case mpr.intro
m : ℕ
⊢ Gamma (-↑m) = 0
[PROOFSTEP]
exact Gamma_neg_nat_eq_zero m
[GOAL]
s : ℂ
hs : 0 < s.re
⊢ Gamma s ≠ 0
[PROOFSTEP]
refine' Gamma_ne_zero fun m => _
[GOAL]
s : ℂ
hs : 0 < s.re
m : ℕ
⊢ s ≠ -↑m
[PROOFSTEP]
contrapose! hs
[GOAL]
s : ℂ
m : ℕ
hs : s = -↑m
⊢ s.re ≤ 0
[PROOFSTEP]
simpa only [hs, neg_re, ← ofReal_nat_cast, ofReal_re, neg_nonpos] using Nat.cast_nonneg _
[GOAL]
s : ℝ
⊢ Tendsto (GammaSeq s) atTop (𝓝 (Gamma s))
[PROOFSTEP]
suffices : Tendsto ((↑) ∘ GammaSeq s : ℕ → ℂ) atTop (𝓝 <| Complex.Gamma s)
[GOAL]
s : ℝ
this : Tendsto (Complex.ofReal' ∘ GammaSeq s) atTop (𝓝 (Complex.Gamma ↑s))
⊢ Tendsto (GammaSeq s) atTop (𝓝 (Gamma s))
case this s : ℝ ⊢ Tendsto (Complex.ofReal' ∘ GammaSeq s) atTop (𝓝 (Complex.Gamma ↑s))
[PROOFSTEP]
exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this
[GOAL]
case this
s : ℝ
⊢ Tendsto (Complex.ofReal' ∘ GammaSeq s) atTop (𝓝 (Complex.Gamma ↑s))
[PROOFSTEP]
convert Complex.GammaSeq_tendsto_Gamma s
[GOAL]
case h.e'_3
s : ℝ
⊢ Complex.ofReal' ∘ GammaSeq s = Complex.GammaSeq ↑s
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_3.h
s : ℝ
n : ℕ
⊢ (Complex.ofReal' ∘ GammaSeq s) n = Complex.GammaSeq (↑s) n
[PROOFSTEP]
dsimp only [GammaSeq, Function.comp_apply, Complex.GammaSeq]
[GOAL]
case h.e'_3.h
s : ℝ
n : ℕ
⊢ ↑(↑n ^ s * ↑n ! / ∏ j in Finset.range (n + 1), (s + ↑j)) = ↑n ^ ↑s * ↑n ! / ∏ j in Finset.range (n + 1), (↑s + ↑j)
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.h
s : ℝ
n : ℕ
⊢ ↑(↑n ^ s) * ↑n ! / ∏ x in Finset.range (n + 1), (↑s + ↑x) = ↑n ^ ↑s * ↑n ! / ∏ x in Finset.range (n + 1), (↑s + ↑x)
[PROOFSTEP]
rw [Complex.ofReal_cpow n.cast_nonneg, Complex.ofReal_nat_cast]
[GOAL]
s : ℝ
⊢ Gamma s * Gamma (1 - s) = π / sin (π * s)
[PROOFSTEP]
simp_rw [← Complex.ofReal_inj, Complex.ofReal_div, Complex.ofReal_sin, Complex.ofReal_mul, ← Complex.Gamma_ofReal,
  Complex.ofReal_sub, Complex.ofReal_one]
[GOAL]
s : ℝ
⊢ Complex.Gamma ↑s * Complex.Gamma (1 - ↑s) = ↑π / Complex.sin (↑π * ↑s)
[PROOFSTEP]
exact Complex.Gamma_mul_Gamma_one_sub s
[GOAL]
s : ℂ
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
[PROOFSTEP]
rcases ne_or_eq s 0 with (h | rfl)
[GOAL]
case inl
s : ℂ
h : s ≠ 0
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
[PROOFSTEP]
rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]
[GOAL]
case inr
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹
[PROOFSTEP]
rw [zero_add, Gamma_zero, inv_zero, zero_mul]
[GOAL]
⊢ Differentiable ℂ fun s => (Gamma s)⁻¹
[PROOFSTEP]
suffices : ∀ n : ℕ, ∀ (s : ℂ) (_ : -s.re < n), DifferentiableAt ℂ (fun u : ℂ => (Gamma u)⁻¹) s
[GOAL]
this : ∀ (n : ℕ) (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
⊢ Differentiable ℂ fun s => (Gamma s)⁻¹
case this ⊢ ∀ (n : ℕ) (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
exact fun s =>
  let ⟨n, h⟩ := exists_nat_gt (-s.re)
  this n s h
[GOAL]
case this
⊢ ∀ (n : ℕ) (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
intro n
[GOAL]
case this
n : ℕ
⊢ ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
induction' n with m hm
[GOAL]
case this.zero
⊢ ∀ (s : ℂ), -s.re < ↑Nat.zero → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
intro s hs
[GOAL]
case this.zero
s : ℂ
hs : -s.re < ↑Nat.zero
⊢ DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
rw [Nat.cast_zero, neg_lt_zero] at hs
[GOAL]
case this.zero
s : ℂ
hs : 0 < s.re
⊢ DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
suffices : ∀ m : ℕ, s ≠ -↑m
[GOAL]
case this.zero
s : ℂ
hs : 0 < s.re
this : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
case this s : ℂ hs : 0 < s.re ⊢ ∀ (m : ℕ), s ≠ -↑m
[PROOFSTEP]
exact (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
[GOAL]
case this
s : ℂ
hs : 0 < s.re
⊢ ∀ (m : ℕ), s ≠ -↑m
[PROOFSTEP]
contrapose! hs
[GOAL]
case this
s : ℂ
hs : ∃ m, s = -↑m
⊢ s.re ≤ 0
[PROOFSTEP]
rcases hs with ⟨m, rfl⟩
[GOAL]
case this.intro
m : ℕ
⊢ (-↑m).re ≤ 0
[PROOFSTEP]
simpa only [neg_re, ← ofReal_nat_cast, ofReal_re, neg_nonpos] using Nat.cast_nonneg m
[GOAL]
case this.succ
m : ℕ
hm : ∀ (s : ℂ), -s.re < ↑m → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
⊢ ∀ (s : ℂ), -s.re < ↑(Nat.succ m) → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
intro s hs
[GOAL]
case this.succ
m : ℕ
hm : ∀ (s : ℂ), -s.re < ↑m → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
s : ℂ
hs : -s.re < ↑(Nat.succ m)
⊢ DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
[PROOFSTEP]
rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
[GOAL]
case this.succ
m : ℕ
hm : ∀ (s : ℂ), -s.re < ↑m → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
s : ℂ
hs : -s.re < ↑(Nat.succ m)
⊢ DifferentiableAt ℂ (fun x => x * (Gamma (x + 1))⁻¹) s
[PROOFSTEP]
specialize hm (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
[GOAL]
m : ℕ
hm : ∀ (s : ℂ), -s.re < ↑m → DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) s
s : ℂ
hs : -s.re < ↑(Nat.succ m)
⊢ -(s + 1).re < ↑m
[PROOFSTEP]
rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]
[GOAL]
case this.succ
m : ℕ
s : ℂ
hs : -s.re < ↑(Nat.succ m)
hm : DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) (s + 1)
⊢ DifferentiableAt ℂ (fun x => x * (Gamma (x + 1))⁻¹) s
[PROOFSTEP]
refine' differentiableAt_id.mul (hm.comp s _)
[GOAL]
case this.succ
m : ℕ
s : ℂ
hs : -s.re < ↑(Nat.succ m)
hm : DifferentiableAt ℂ (fun u => (Gamma u)⁻¹) (s + 1)
⊢ DifferentiableAt ℂ (fun x => x + 1) s
[PROOFSTEP]
exact differentiableAt_id.add (differentiableAt_const _)
[GOAL]
s : ℂ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑(sqrt π)
[PROOFSTEP]
suffices
  (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(Real.sqrt π)
  by
  convert congr_arg Inv.inv (congr_fun this s) using 1
  · rw [mul_inv, inv_inv, inv_inv]
  · rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
[GOAL]
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑(sqrt π)
[PROOFSTEP]
convert congr_arg Inv.inv (congr_fun this s) using 1
[GOAL]
case h.e'_2
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹
[PROOFSTEP]
rw [mul_inv, inv_inv, inv_inv]
[GOAL]
case h.e'_3
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑(sqrt π) = ((Gamma (2 * s))⁻¹ * 2 ^ (2 * s - 1) / ↑(sqrt π))⁻¹
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
[GOAL]
s : ℂ
⊢ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)
[PROOFSTEP]
have h1 : AnalyticOn ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ :=
  by
  refine' DifferentiableOn.analyticOn _ isOpen_univ
  refine' (differentiable_one_div_Gamma.mul _).differentiableOn
  exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))
[GOAL]
s : ℂ
⊢ AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
[PROOFSTEP]
refine' DifferentiableOn.analyticOn _ isOpen_univ
[GOAL]
s : ℂ
⊢ DifferentiableOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
[PROOFSTEP]
refine' (differentiable_one_div_Gamma.mul _).differentiableOn
[GOAL]
s : ℂ
⊢ Differentiable ℂ fun z => (Gamma (z + 1 / 2))⁻¹
[PROOFSTEP]
exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)
[PROOFSTEP]
have h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(Real.sqrt π)) univ :=
  by
  refine' DifferentiableOn.analyticOn _ isOpen_univ
  refine' (Differentiable.mul _ (differentiable_const _)).differentiableOn
  apply Differentiable.mul
  · exact differentiable_one_div_Gamma.comp (differentiable_id'.const_mul _)
  · refine' fun t => DifferentiableAt.const_cpow _ (Or.inl two_ne_zero)
    refine' DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
[PROOFSTEP]
refine' DifferentiableOn.analyticOn _ isOpen_univ
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ DifferentiableOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
[PROOFSTEP]
refine' (Differentiable.mul _ (differentiable_const _)).differentiableOn
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1)
[PROOFSTEP]
apply Differentiable.mul
[GOAL]
case ha
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun y => (Gamma (2 * y))⁻¹
[PROOFSTEP]
exact differentiable_one_div_Gamma.comp (differentiable_id'.const_mul _)
[GOAL]
case hb
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun y => 2 ^ (2 * y - 1)
[PROOFSTEP]
refine' fun t => DifferentiableAt.const_cpow _ (Or.inl two_ne_zero)
[GOAL]
case hb
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
t : ℂ
⊢ DifferentiableAt ℂ (fun y => 2 * y - 1) t
[PROOFSTEP]
refine' DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
⊢ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)
[PROOFSTEP]
have h3 : Tendsto ((↑) : ℝ → ℂ) (𝓝[≠] 1) (𝓝[≠] 1) :=
  by
  rw [tendsto_nhdsWithin_iff]; constructor
  · exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt
  · exact eventually_nhdsWithin_iff.mpr (eventually_of_forall fun t ht => ofReal_ne_one.mpr ht)
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
⊢ Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
[PROOFSTEP]
rw [tendsto_nhdsWithin_iff]
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
⊢ Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[{1}ᶜ] 1, ↑n ∈ {1}ᶜ
[PROOFSTEP]
constructor
[GOAL]
case left
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
⊢ Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝 1)
[PROOFSTEP]
exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt
[GOAL]
case right
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
⊢ ∀ᶠ (n : ℝ) in 𝓝[{1}ᶜ] 1, ↑n ∈ {1}ᶜ
[PROOFSTEP]
exact eventually_nhdsWithin_iff.mpr (eventually_of_forall fun t ht => ofReal_ne_one.mpr ht)
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
h3 : Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
⊢ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)
[PROOFSTEP]
refine' AnalyticOn.eq_of_frequently_eq h1 h2 (h3.frequently _)
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
h3 : Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
⊢ ∃ᶠ (x : ℝ) in 𝓝[{1}ᶜ] 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑(sqrt π)
[PROOFSTEP]
refine' ((Eventually.filter_mono nhdsWithin_le_nhds) _).frequently
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
h3 : Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
⊢ ∀ᶠ (x : ℝ) in 𝓝 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑(sqrt π)
[PROOFSTEP]
refine' (eventually_gt_nhds zero_lt_one).mp (eventually_of_forall fun t ht => _)
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
h3 : Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
t : ℝ
ht : 0 < t
⊢ (Gamma ↑t)⁻¹ * (Gamma (↑t + 1 / 2))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑(sqrt π)
[PROOFSTEP]
rw [← mul_inv, Gamma_ofReal, (by norm_num : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ← ofReal_mul,
  Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal, mul_inv, mul_inv,
  (by norm_num : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal, ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ←
  cpow_neg, ofReal_sub, ofReal_one, neg_sub, ← div_eq_mul_inv]
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
h3 : Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
t : ℝ
ht : 0 < t
⊢ ↑t + 1 / 2 = ↑(t + 1 / 2)
[PROOFSTEP]
norm_num
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
h3 : Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
t : ℝ
ht : 0 < t
⊢ 2 * ↑t = ↑(2 * t)
[PROOFSTEP]
norm_num
[GOAL]
s : ℂ
h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑(sqrt π)) univ
h3 : Tendsto ofReal' (𝓝[{1}ᶜ] 1) (𝓝[{1}ᶜ] 1)
t : ℝ
ht : 0 < t
⊢ ↑2 = 2
[PROOFSTEP]
norm_cast
[GOAL]
s : ℝ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * sqrt π
[PROOFSTEP]
rw [← ofReal_inj]
[GOAL]
s : ℝ
⊢ ↑(Gamma s * Gamma (s + 1 / 2)) = ↑(Gamma (2 * s) * 2 ^ (1 - 2 * s) * sqrt π)
[PROOFSTEP]
simpa only [← Gamma_ofReal, ofReal_cpow zero_le_two, ofReal_mul, ofReal_add, ofReal_div, ofReal_sub] using
  Complex.Gamma_mul_Gamma_add_half ↑s