mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: 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 ∈ 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 * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

pp: 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 ∈ 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

pp: 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 ∈ 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

Tactic:
·

Goal state after:
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 ∈ 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 * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x ↦ Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ (fun n ↦ (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n)) =
    fun n ↦ (∫ (x : ℝ) in 0..π / 2, ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)) / ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n)

pp: case e'_5
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x ↦ Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * ↑0))

Tactic:
·

Goal state after:
case e'_3
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x ↦ Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ (fun n ↦ (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n)) =
    fun n ↦ (∫ (x : ℝ) in 0..π / 2, ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)) / ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))
⊢ (log ∘ f) x = (log ∘ Γ) x

pp: case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
⊢ ∀ {y : ℝ}, 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y

Tactic:
·

Goal state after:
case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))
⊢ (log ∘ f) x = (log ∘ Γ) x
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤
⊢ logDeriv (f * g) =ᶠ[codiscreteWithin U] logDeriv f + logDeriv g

Tactic:
filter_upwards [hf.analyticAt_mem_codiscreteWithin, hg.analyticAt_mem_codiscreteWithin,
    hf.eventually_codiscreteWithin_apply_ne_zero h'f,
    hg.eventually_codiscreteWithin_apply_ne_zero h'g]
    with y h₁y h₂y h₃y h₄y

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤
y : 𝕜
h₁y : AnalyticAt 𝕜 f y
h₂y : AnalyticAt 𝕜 g y
h₃y : f y ≠ 0
h₄y : g y ≠ 0
⊢ logDeriv (f * g) y = (logDeriv f + logDeriv g) y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
⊢ ∀ {y : ℝ}, 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y

Tactic:
·

Goal state after:
case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
⊢ ∀ {y : ℝ}, 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_5
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x ↦ Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * ↑0))

Tactic:
·

Goal state after:
case e'_5
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x ↦ Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * ↑0))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: 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 ∈ 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

pp: 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 ∈ 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

Tactic:
·

Goal state after:
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 ∈ 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
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y

pp: case refine_2
A : 0 < 3 / 2
this : (log ∘ Γ) (↑2 + 1 / 2) ≤ (log ∘ Γ) ↑2 + 1 / 2 * log ↑2
⊢ Γ (3 / 2) < 1

Tactic:
·

Goal state after:
case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: 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 ∈ 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

Tactic:
·

Goal state after:
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 ∈ 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
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
x : ℝ
⊢ (fun n ↦ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) =
    Complex.re ∘ fun n ↦ ↑π * ↑x * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)

pp: case e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re

Tactic:
·

Goal state after:
case e'_3
x : ℝ
⊢ (fun n ↦ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) =
    Complex.re ∘ fun n ↦ ↑π * ↑x * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re

Tactic:
·

Goal state after:
case e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_1
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < (↑n.succ).re

pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u * u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)

Tactic:
·

Goal state after:
case succ.refine_1
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < (↑n.succ).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case inl
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ioc 0 1
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}

pp: case inr.inl
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Icc 1 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}

pp: case inr.inr
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ici 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}

Tactic:
·

Goal state after:
case inl
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ioc 0 1
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case inr.inl
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Icc 1 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}

pp: case inr.inr
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ici 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}

Tactic:
·

Goal state after:
case inr.inl
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Icc 1 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u ≠ 0

pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)

Tactic:
·

Goal state after:
case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u ≠ 0
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ ⨆ p, atTop • 𝓝 v +ᵥ pure p ≤ atTop • 𝓝 v

pp: case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ atTop • 𝓝 v ≤ ⨆ p, atTop • 𝓝 v +ᵥ pure p

Tactic:
·

Goal state after:
case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ ⨆ p, atTop • 𝓝 v +ᵥ pure p ≤ atTop • 𝓝 v
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case inr.inr
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ici 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}

Tactic:
·

Goal state after:
case inr.inr
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Ici 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ 0 < (u + 1).re

pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ (↑n + 1) * (↑n ! / ∏ j ∈ Finset.range (n + 1), (u + 1 + ↑j)) / u =
    ↑(n + 1)! / ((∏ k ∈ Finset.range (n + 1), (u + ↑(k + 1))) * (u + ↑0))

Tactic:
·

Goal state after:
case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ 0 < (u + 1).re
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ atTop • 𝓝 v ≤ ⨆ p, atTop • 𝓝 v +ᵥ pure p

Tactic:
·

Goal state after:
case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ atTop • 𝓝 v ≤ ⨆ p, atTop • 𝓝 v +ᵥ pure p
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2))

pp: case refine_2
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2 + 1 / 2))

pp: case refine_3
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ s * log 2

Tactic:
·

Goal state after:
case refine_1
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_11
⊢ Ioi 0 = ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap ⁻¹' Ioi 0

pp: case e'_12
⊢ (fun s ↦ log (Γ (s / 2))) = (log ∘ Γ) ∘ ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap

Tactic:
·

Goal state after:
case e'_11
⊢ Ioi 0 = ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap ⁻¹' Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_12
⊢ (fun s ↦ log (Γ (s / 2))) = (log ∘ Γ) ∘ ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap

Tactic:
·

Goal state after:
case e'_12
⊢ (fun s ↦ log (Γ (s / 2))) = (log ∘ Γ) ∘ ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2 + 1 / 2))

pp: case refine_3
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ s * log 2

Tactic:
·

Goal state after:
case refine_2
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2 + 1 / 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_11
⊢ Ioi (-1) = ⇑((DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2)) ⁻¹' Ioi 0

pp: case e'_12
⊢ (fun s ↦ log (Γ (s / 2 + 1 / 2))) =
    (log ∘ Γ) ∘ ⇑((DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2))

Tactic:
·

Goal state after:
case e'_11
⊢ Ioi (-1) = ⇑((DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2)) ⁻¹' Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_12
⊢ (fun s ↦ log (Γ (s / 2 + 1 / 2))) =
    (log ∘ Γ) ∘ ⇑((DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2))

Tactic:
·

Goal state after:
case e'_12
⊢ (fun s ↦ log (Γ (s / 2 + 1 / 2))) =
    (log ∘ Γ) ∘ ⇑((DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap + AffineMap.const ℝ ℝ (1 / 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_3
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ s * log 2

Tactic:
·

Goal state after:
case refine_3
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ s * log 2
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v

pp: case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ asymptoticNhds k P v ≤ (𝓝 v).bind (asymptoticNhds k P)

Tactic:
·

Goal state after:
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) = ↑n * ↑n ^ s

pp: case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∏ x ∈ Finset.range n, (s + 1 + ↑x) = ∏ k ∈ Finset.range n, (s + ↑(k + 1))

pp: case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s

Tactic:
·

Goal state after:
case e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) = ↑n * ↑n ^ s
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ asymptoticNhds k P v ≤ (𝓝 v).bind (asymptoticNhds k P)

Tactic:
·

Goal state after:
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ asymptoticNhds k P v ≤ (𝓝 v).bind (asymptoticNhds k P)