awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
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 : Membership.mem (γ := Set ℝ) (Ioi 0) x
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x))
⊢ (log ∘ f) x = (log ∘ Γ) x

Tactic:
tendsto_nhds_unique e1 (BohrMollerup.tendsto_log_gamma hx)

Premises used: tendsto_nhds_unique, Real.BohrMollerup.tendsto_log_gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
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 : Membership.mem (γ := Set ℝ) (Ioi 0) x
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x))
⊢ (log ∘ f) x = (log ∘ Γ) x

Tactic:
exact tendsto_nhds_unique e1 (BohrMollerup.tendsto_log_gamma hx)

Premises used: tendsto_nhds_unique, Real.BohrMollerup.tendsto_log_gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
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 : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : 0 < y
refine_1 : log y + log (f y) = log (f y) + log y
⊢ (log ∘ f) (y + 1) = (log ∘ f) y + log y

Tactic:
rw [Function.comp_apply, Function.comp_apply, hf_feq hy, log_mul hy.ne' (hf_pos hy).ne']

Premises used: LT.lt.ne', Function.comp_apply, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
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 : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : 0 < y
⊢ log y + log (f y) = log (f y) + log y

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ Γ 2 = 1

Tactic:
simp [Nat.factorial_one]

Premises used: Nat.factorial_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ 0 < 3 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ 0 < 3 / 2

Tactic:
have A : (0 : ℝ) < 3 / 2 := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
⊢ 1 / 2 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
refine_2 : ∀ (this : (log ∘ Γ) ((↑2 : ℝ) + 1 / 2) ≤ (log ∘ Γ) (↑2 : ℝ) + 1 / 2 * log (↑2 : ℝ)), Γ (3 / 2) < 1
refine_1 : ∀ {y : ℝ} (hy : 0 < y), (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y
⊢ Γ (3 / 2) < 1

Tactic:
have :=
    BohrMollerup.f_add_nat_le convexOn_log_Gamma (fun {y} hy => ?_) two_ne_zero one_half_pos
      (by norm_num : 1 / 2 ≤ (1 : ℝ))
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
refine_1 : log (Γ (y + 1)) = (log ∘ Γ) y + log y
refine_1₁ : log (y * Γ y) = (log ∘ Γ) y + log y
refine_1₂ : log y + log (Γ y) = (log ∘ Γ) y + log y
refine_1₃ : log (Γ y) + log y = (log ∘ Γ) y + log y
refine_1₄ refine_1₅ : log (Γ y) + log y = log (Γ y) + log y
⊢ (log ∘ Γ) (y + 1) = (log ∘ Γ) y + log y

Tactic:
rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne',
      add_comm, Function.comp_apply]

Premises used: Real.Gamma_pos_of_pos, Real.Gamma_add_one, add_comm, LT.lt.ne', Function.comp_apply, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : log (Γ (2 + 1 / 2)) ≤ 1 / 2 * log 2
⊢ 2 + 1 / 2 = 3 / 2 + 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : (log ∘ Γ) ((↑2 : ℝ) + 1 / 2) ≤ (log ∘ Γ) (↑2 : ℝ) + 1 / 2 * log (↑2 : ℝ)
⊢ Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))

Tactic:
rw [Function.comp_apply, Function.comp_apply, Nat.cast_two, Gamma_two, log_one, zero_add,
    (by norm_num : (2 : ℝ) + 1 / 2 = 3 / 2 + 1), Gamma_add_one A.ne',
    log_mul A.ne' (Gamma_pos_of_pos A).ne', ← le_sub_iff_add_le',
    log_le_iff_le_exp (Gamma_pos_of_pos A)] at this

Premises used: Real.Gamma_pos_of_pos, Real.Gamma_two, le_sub_iff_add_le', Real.log_one, Real.log_le_iff_le_exp, Real.Gamma_add_one, zero_add, LT.lt.ne', Function.comp_apply, Real.log_mul, Nat.cast_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ Γ (3 / 2) < 1

Tactic:
this.trans_lt (exp_lt_one_iff.mpr ?_)

Premises used: Iff.mpr, Real.exp_lt_one_iff, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
refine_2 : 1 / 2 * log 2 - log (3 / 2) < 0
⊢ Γ (3 / 2) < 1

Tactic:
refine this.trans_lt (exp_lt_one_iff.mpr ?_)

Premises used: Iff.mpr, Real.exp_lt_one_iff, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
refine_2 : (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0
⊢ 1 / 2 * log 2 - log (3 / 2) < 0

Tactic:
rw [mul_comm, ← mul_div_assoc, div_sub' two_ne_zero]

Premises used: mul_div_assoc, two_ne_zero, mul_comm, div_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0

Tactic:
div_neg_of_neg_of_pos ?_ two_pos

Premises used: two_pos, div_neg_of_neg_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
refine_2 : log 2 * 1 - 2 * log (3 / 2) < 0
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0

Tactic:
refine div_neg_of_neg_of_pos ?_ two_pos

Premises used: div_neg_of_neg_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
refine_2 : 2 < HPow.hPow (β := ℕ) (3 / 2) 2
refine_2₁ : 0 < HPow.hPow (β := ℕ) (3 / 2) 2
⊢ log 2 * 1 - 2 * log (3 / 2) < 0

Tactic:
rw [sub_neg, mul_one, ← Nat.cast_two, ← log_pow, ← exp_lt_exp, Nat.cast_two, exp_log two_pos,
      exp_log]

Premises used: sub_neg, two_pos, Real.exp_log, Real.exp_lt_exp, Real.log_pow, mul_one, Nat.cast_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 2 < HPow.hPow (β := ℕ) (3 / 2) 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 0 < HPow.hPow (β := ℕ) (3 / 2) 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (3 / 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ 1 < 3 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ 3 / 2 < 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h : Eq (α := Set ℝ) (Ici 2) (Ioi 0 ∩ Ici 2)
⊢ StrictMonoOn Γ (Ici 2)

Tactic:
convert!
    convexOn_Gamma.strictMonoOn (by simp : (0 : ℝ) < 3 / 2) (by norm_num : (3 / 2 : ℝ) < 2)
      (Gamma_two.symm ▸ Gamma_three_div_two_lt_one)

Premises used: Real.Gamma_two, Eq.rec, Real.convexOn_Gamma, ConvexOn.strictMonoOn, Eq.symm, Real.Gamma_three_div_two_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h : Eq (α := Set ℝ) (Ioi 0 ∩ Ici 2) (Ici 2)
⊢ Eq (α := Set ℝ) (Ici 2) (Ioi 0 ∩ Ici 2)

Tactic:
symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h : Subset (α := Set ℝ) (Ici 2) (Ioi 0)
⊢ Eq (α := Set ℝ) (Ioi 0 ∩ Ici 2) (Ici 2)

Tactic:
rw [inter_eq_right]

Premises used: Set.inter_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ Subset (α := Set ℝ) (Ici 2) (Ioi 0)

Tactic:
fun x hx => two_pos.trans_le <| mem_Ici.mp hx

Premises used: Set.Ioi, Set.Mem, setOf, two_pos, Set.Subset, LT.lt.trans_le, Set.mem_Ici, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ Subset (α := Set ℝ) (Ici 2) (Ioi 0)

Tactic:
exact fun x hx => two_pos.trans_le <| mem_Ici.mp hx

Premises used: two_pos, LT.lt.trans_le, Set.mem_Ici, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ Subset (α := Set ℝ) (Icc 1 2) (Ioi 0)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
have :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x) (hmin : IsMinOn Γ (Icc 1 2) x),
    ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x

Tactic:
have ⟨x, hx, hmin⟩ := isCompact_Icc.exists_isMinOn (nonempty_Icc.mpr one_le_two) <|
    differentiableOn_Gamma_Ioi.continuousOn.mono <| by grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
⊢ Membership.mem (γ := Set ℝ) (Icc 1 2) (3 / 2)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
⊢ Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2)

Tactic:
simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num

Premises used: Real.Gamma_three_div_two_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
⊢ Γ (3 / 2) < Γ 1

Tactic:
have ⟨h1, h2, h3half⟩ : Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2) := by
    simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
⊢ Γ (3 / 2) < Γ 2

Tactic:
have ⟨h1, h2, h3half⟩ : Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2) := by
    simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
⊢ Γ x ≤ Γ (3 / 2)

Tactic:
have ⟨h1, h2, h3half⟩ : Γ (3 / 2) < Γ 1 ∧ Γ (3 / 2) < Γ 2 ∧ Γ x ≤ Γ (3 / 2) := by
    simpa [Gamma_three_div_two_lt_one] using hmin <| by norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
⊢ Membership.mem (γ := Set ℝ) (Ioo 1 2) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
refine :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) y → Membership.mem (γ := Set ℝ) {x_2 : ℝ | (fun (x_3 : ℝ) ↦ Γ x ≤ Γ x_3) x_2} y
⊢ ∃ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo 1 2) x ∧ IsMinOn Γ (Ioi 0) x

Tactic:
refine ⟨x, by grind, fun y _ ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
⊢ Membership.mem (γ := Set ℝ) (Ioc 0 1) y ∨
    Membership.mem (γ := Set ℝ) (Icc 1 2) y ∨ Membership.mem (γ := Set ℝ) (Ici 2) y

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
inl :
  ∀ (hy : Membership.mem (γ := Set ℝ) (Ioc 0 1) y),
    Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
inr :
  ∀ (hy : Membership.mem (γ := Set ℝ) (Icc 1 2) y),
    Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
inr₁ :
  ∀ (hy : Membership.mem (γ := Set ℝ) (Ici 2) y),
    Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y

Tactic:
obtain hy | hy | hy : y ∈ Ioc 0 1 ∨ y ∈ Icc 1 2 ∨ y ∈ Ici 2 := by grind

Premises used: Set.Ioc, Set.Ici, Set.Icc, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
hy : Membership.mem (γ := Set ℝ) (Ioc 0 1) y
⊢ Membership.mem (γ := Set ℝ) (Ioc 0 1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
hy : Membership.mem (γ := Set ℝ) (Ioc 0 1) y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y

Tactic:
exact h3half.trans h1.le |>.trans <| Gamma_strictAntiOn_Ioc.antitoneOn hy (by simp) hy.right

Premises used: Real.Gamma_strictAntiOn_Ioc, LT.lt.le, And.right, StrictAntiOn.antitoneOn, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
hy : Membership.mem (γ := Set ℝ) (Icc 1 2) y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y

Tactic:
hmin hy

Premises used: Set.Mem, setOf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
hy : Membership.mem (γ := Set ℝ) (Icc 1 2) y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y

Tactic:
exact hmin hy
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
hy : Membership.mem (γ := Set ℝ) (Ici 2) y
⊢ Membership.mem (γ := Set ℝ) (Ici 2) 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 1 2) x
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) y
hy : Membership.mem (γ := Set ℝ) (Ici 2) y
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (x_2 : ℝ) ↦ Γ x ≤ Γ x_2) x_1} y

Tactic:
exact h3half.trans h2.le |>.trans <| Gamma_strictMonoOn_Ici.monotoneOn (by simp) hy hy

Premises used: Real.Gamma_strictMonoOn_Ici, LT.lt.le, StrictMonoOn.monotoneOn, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : s ≠ 0
⊢ s + 1 - 1 = s - 1 + 1

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : s ≠ 0
rw :
  Γ (s / 2 + 1 / 2) * (s / 2 * Γ (s / 2)) * (HPow.hPow (α := ℝ) 2 (s - 1) * 2) / √π =
    s * (Γ (s / 2) * Γ (s / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (s - 1) / √π)
⊢ (s + 1).doublingGamma = s * s.doublingGamma

Tactic:
rw [doublingGamma, doublingGamma, (by abel : s + 1 - 1 = s - 1 + 1), add_div, add_assoc,
    add_halves (1 : ℝ), Gamma_add_one (div_ne_zero hs two_ne_zero), rpow_add two_pos, rpow_one]

Premises used: add_halves, add_assoc, two_pos, Real.Gamma_add_one, Real.rpow_one, div_ne_zero, two_ne_zero, Real.rpow_add, OfNat.ofNat, add_div, Real.doublingGamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : s ≠ 0
⊢ Γ (s / 2 + 1 / 2) * (s / 2 * Γ (s / 2)) * (HPow.hPow (α := ℝ) 2 (s - 1) * 2) / √π =
    s * (Γ (s / 2) * Γ (s / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (s - 1) / √π)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
simp_rw : Γ (1 / 2) * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₁ : √π * Γ (1 / 2 + 1 / 2) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₂ : √π * Γ 1 * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℝ) 1 1) / √π = 1
simp_rw₃ : √π * Γ 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₄ : √π * 1 * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₅ : √π * HPow.hPow (α := ℝ) (β := ℝ) 2 0 / √π = 1
simp_rw₆ : √π * 1 / √π = 1
simp_rw₇ : √π / √π = 1
⊢ doublingGamma 1 = 1

Tactic:
simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]

Premises used: Iff.mpr, add_halves, sub_self, Real.Gamma_one, Real.Gamma_one_half_eq, Real.rpow_zero, Real.pi_pos, mul_one, OfNat.ofNat, div_self, Real.sqrt_ne_zero', Real.doublingGamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
⊢ √π ≠ 0

Tactic:
have h1 : √π ≠ 0 := sqrt_ne_zero'.mpr pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
⊢ Γ (s / 2) ≠ 0

Tactic:
have h2 : Gamma (s / 2) ≠ 0 := (Gamma_pos_of_pos <| div_pos hs two_pos).ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
⊢ Γ (s / 2 + 1 / 2) ≠ 0

Tactic:
have h3 : Gamma (s / 2 + 1 / 2) ≠ 0 :=
    (Gamma_pos_of_pos <| add_pos (div_pos hs two_pos) one_half_pos).ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
⊢ HPow.hPow (α := ℝ) 2 (s - 1) ≠ 0

Tactic:
have h4 : (2 : ℝ) ^ (s - 1) ≠ 0 := (rpow_pos_of_pos two_pos _).ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : HPow.hPow (α := ℝ) 2 (s - 1) ≠ 0
rw :
  log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + (s - 1) * log 2 - log √π =
    (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - (log 2 + log √π)) s
⊢ (log ∘ doublingGamma) s = (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s

Tactic:
rw [Function.comp_apply, doublingGamma, log_div (mul_ne_zero (mul_ne_zero h2 h3) h4) h1,
    log_mul (mul_ne_zero h2 h3) h4, log_mul h2 h3, log_rpow two_pos, log_mul two_ne_zero h1]

Premises used: Real.log_rpow, two_pos, Real.log_div, two_ne_zero, Function.comp_apply, mul_ne_zero, Real.log_mul, Real.doublingGamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Ioi 0) s
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : HPow.hPow (α := ℝ) 2 (s - 1) ≠ 0
⊢ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + (s - 1) * log 2 - log √π =
    (fun (s : ℝ) ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - (log 2 + log √π)) s

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)

Tactic:
(((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm

Premises used: Set.EqOn.symm, ConvexOn.congr, ConvexOn.add, ConvexOn.add_const, Real.log_doublingGamma_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
refine_1 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2))
refine_2 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
refine_3 : ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ s * log 2
⊢ ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)

Tactic:
refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm

Premises used: Set.EqOn.symm, ConvexOn.congr, ConvexOn.add, ConvexOn.add_const, Real.log_doublingGamma_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ ConvexOn ℝ (E := ℝ)
    (preimage (β := ℝ) (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ) (Ioi 0))
    ((log ∘ Γ) ∘ (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ))

Tactic:
convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap

Premises used: Real, DistribSMul.toLinearMap, HDiv.hDiv, LinearMap.toAffineMap, Real.convexOn_log_Gamma, ConvexOn.comp_affineMap, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h :
  Eq (α := Set ℝ) (Ioi 0)
    (preimage (β := ℝ) (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ) (Ioi 0))
h₁ :
  Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2)))
    ((log ∘ Γ) ∘ (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ))
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2))

Tactic:
convert!
    convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap using 1

Premises used: Real, DistribSMul.toLinearMap, HDiv.hDiv, LinearMap.toAffineMap, Real.convexOn_log_Gamma, ConvexOn.comp_affineMap, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ Eq (α := Set ℝ) (Ioi 0)
    (preimage (β := ℝ) (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ) (Ioi 0))

Tactic:
simpa only [zero_div] using (preimage_const_mul_Ioi₀ (0 : ℝ) one_half_pos).symm

Premises used: Set.preimage_const_mul_Ioi₀, zero_div, one_half_pos, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h :
  ∀ (x : ℝ),
    log (Γ (x / 2)) = ((log ∘ Γ) ∘ (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ)) x
⊢ Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2)))
    ((log ∘ Γ) ∘ (⇑(LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2))) : (a : ℝ) → ℝ))

Tactic:
ext1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
h : log (Γ (x / 2)) = log (Γ (1 / 2 * x))
h₁ : log (Γ (x / 2)) = log (Γ (x * (1 / 2)))
h₂ h₃ : log (Γ (x / 2)) = log (Γ (x / 2))
⊢ log (Γ (x / 2)) = log (Γ ((1 / 2) • x))

Tactic:
rw [smul_eq_mul, mul_comm, mul_one_div]

Premises used: mul_one_div, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))

Tactic:
ConvexOn.subset ?_ (Ioi_subset_Ioi <| neg_one_lt_zero.le) (convex_Ioi _)

Premises used: LT.lt.le, Set.Ioi_subset_Ioi, neg_one_lt_zero, convex_Ioi, ConvexOn.subset
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
refine_2 : ConvexOn ℝ (β := ℝ) (Ioi (-1)) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))

Tactic:
refine ConvexOn.subset ?_ (Ioi_subset_Ioi <| neg_one_lt_zero.le) (convex_Ioi _)

Premises used: LT.lt.le, Set.Ioi_subset_Ioi, neg_one_lt_zero, convex_Ioi, ConvexOn.subset
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ ConvexOn ℝ (E := ℝ)
    (preimage (β := ℝ)
      (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
            (AffineMap.const ℝ ℝ (1 / 2))) :
        (a : ℝ) → ℝ)
      (Ioi 0))
    ((log ∘ Γ) ∘
      (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
            (AffineMap.const ℝ ℝ (1 / 2))) :
        (a : ℝ) → ℝ))

Tactic:
convexOn_log_Gamma.comp_affineMap
        ((DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap +
          AffineMap.const ℝ ℝ (1 / 2 : ℝ))

Premises used: Real, DistribSMul.toLinearMap, HDiv.hDiv, LinearMap.toAffineMap, Real.convexOn_log_Gamma, HAdd.hAdd, AffineMap.const, ConvexOn.comp_affineMap, OfNat.ofNat