-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem convexOn_log_Gamma : ConvexOn ℝ (Ioi 0) (log ∘ Gamma)

Proof state:
case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Gamma x ^ a ≠ 0

case hy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Gamma y ^ (1 - a) ≠ 0

case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Gamma y

case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Gamma x

Tactic:
all_goals positivity

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
⊢ (log ∘ Gamma) (a • x + (1 - a) • y) ≤ a • (log ∘ Gamma) x + (1 - a) • (log ∘ Gamma) y

Tactic:
simp_rw [Function.comp_apply, smul_eq_mul]

Result:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
⊢ log (Gamma (a * x + (1 - a) * y)) ≤ a * log (Gamma x) + (1 - a) * log (Gamma y)

Proof state:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (log ∘ Gamma) (a • x + b • y) ≤ a • (log ∘ Gamma) x + b • (log ∘ Gamma) y

Tactic:
have : b = 1 - a := by linarith

Result:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this : b = 1 - a
⊢ (log ∘ Gamma) (a • x + b • y) ≤ a • (log ∘ Gamma) x + b • (log ∘ Gamma) y

Proof state:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ b = 1 - a

Tactic:
linarith

Result:
no goals

Proof state:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Gamma (a * x + (1 - a) * y)) ≤ log (Gamma x ^ a * Gamma y ^ (1 - a))

Tactic:
gcongr

Result:
case hxy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Gamma (a * x + (1 - a) * y) ≤ Gamma x ^ a * Gamma y ^ (1 - a)

Proof state:
⊢ ConvexOn ℝ (Ioi 0) (log ∘ Gamma)

Tactic:
refine convexOn_iff_forall_pos.mpr ⟨convex_Ioi _, fun x hx y hy a b ha hb hab => ?_⟩

Result:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (log ∘ Gamma) (a • x + b • y) ≤ a • (log ∘ Gamma) x + b • (log ∘ Gamma) y

Proof state:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
⊢ log (Gamma (a * x + (1 - a) * y)) ≤ a * log (Gamma x) + (1 - a) * log (Gamma y)

Tactic:
simp only [mem_Ioi] at hx hy

Result:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Gamma (a * x + (1 - a) * y)) ≤ a * log (Gamma x) + (1 - a) * log (Gamma y)

Proof state:
case hxy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Gamma (a * x + (1 - a) * y) ≤ Gamma x ^ a * Gamma y ^ (1 - a)

Tactic:
exact Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma hx hy ha hb hab

Result:
no goals

Proof state:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Gamma (a * x + (1 - a) * y)) ≤ a * log (Gamma x) + (1 - a) * log (Gamma y)

Tactic:
rw [← log_rpow, ← log_rpow, ← log_mul]

Result:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Gamma (a * x + (1 - a) * y)) ≤ log (Gamma x ^ a * Gamma y ^ (1 - a))

case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Gamma x ^ a ≠ 0

case hy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Gamma y ^ (1 - a) ≠ 0

case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Gamma y

case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Gamma x

Proof state:
case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Gamma x

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this : b = 1 - a
⊢ (log ∘ Gamma) (a • x + b • y) ≤ a • (log ∘ Gamma) x + b • (log ∘ Gamma) y

Tactic:
subst this

Result:
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : y ∈ Ioi 0
a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
⊢ (log ∘ Gamma) (a • x + (1 - a) • y) ≤ a • (log ∘ Gamma) x + (1 - a) • (log ∘ Gamma) y