awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
e_a : a * s + (1 - a) * t - 1 = a * (s - 1) + (1 - a) * (t - 1)
⊢ x ^ (a * s + (1 - a) * t - 1) = x ^ (a * (s - 1) + (1 - a) * (t - 1))

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
⊢ a * s + (1 - a) * t - 1 = a * (s - 1) + (1 - a) * (t - 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
⊢ x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1))

Tactic:
have B : x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1)) := by
      rw [← rpow_add hx, hab']; congr 1; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
B : x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1))
h : rexp (-a * x) * rexp (-b * x) * (x ^ (a * (s - 1)) * x ^ (b * (t - 1))) = f a s x * f b t x
⊢ rexp (-x) * x ^ (a * s + b * t - 1) = f a s x * f b t x

Tactic:
rw [A, B]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
B : x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1))
⊢ rexp (-a * x) * rexp (-b * x) * (x ^ (a * (s - 1)) * x ^ (b * (t - 1))) = f a s x * f b t x

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
h :
  HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (t - 1))
        b =
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
          f a s a_1 ^ (1 / a))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          f b t a ^ (1 / b))
        b
⊢ HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (t - 1))
        b =
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
          f a s a_1 ^ (1 / a))
        (1 / (1 / a)) *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          f b t a ^ (1 / b))
        (1 / (1 / b))

Tactic:
rw [one_div_one_div, one_div_one_div]

Premises used: one_div_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      f a s a_1 ^ (1 / a))
h₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (t - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f b t a ^ (1 / b))
⊢ HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (t - 1))
        b =
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
          f a s a_1 ^ (1 / a))
        a *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          f b t a ^ (1 / b))
        b

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < a

Tactic:
assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      f a s a_1 ^ (1 / a))

Tactic:
exact setIntegral_congr_fun measurableSet_Ioi fun x hx => fpow (by assumption) _ hx

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < b

Tactic:
assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp :
  ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
    MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (t - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ f b t a ^ (1 / b))

Tactic:
exact setIntegral_congr_fun measurableSet_Ioi fun x hx => fpow (by assumption) _ hx

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ ConvexOn ℝ (Ioi 0) (log ∘ Γ)

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

Premises used: Iff.mpr, convexOn_iff_forall_pos, And.intro, convex_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x) (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Ioi 0) y) (a b : ℝ)
    (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), (log ∘ Γ) (a • x + b • y) ≤ a • (log ∘ Γ) x + b • (log ∘ Γ) y
⊢ ConvexOn ℝ (Ioi 0) (log ∘ Γ)

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

Premises used: Iff.mpr, convexOn_iff_forall_pos, And.intro, convex_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioi 0) y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
linarith : b < 1 - a → -(a + b - 1) + (b - (1 - a)) = 0
linarith₁ : 1 - a < b → a + b - 1 + (1 - a - b) = 0
⊢ b = 1 - a

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioi 0) y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ b = 1 - a

Tactic:
have : b = 1 - a := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioi 0) y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this : b = 1 - a
subst :
  ∀ (hb : 0 < 1 - a) (hab : a + (1 - a) = 1), (log ∘ Γ) (a • x + (1 - a) • y) ≤ a • (log ∘ Γ) x + (1 - a) • (log ∘ Γ) y
⊢ (log ∘ Γ) (a • x + b • y) ≤ a • (log ∘ Γ) x + b • (log ∘ Γ) y

Tactic:
subst this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioi 0) y
a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
⊢ 0 < x

Tactic:
push _ ∈ _ at hx hy
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioi 0) y
a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx₁ : 0 < x
⊢ 0 < y

Tactic:
push _ ∈ _ at hx hy
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
rw : log (Γ (a * x + (1 - a) * y)) ≤ log (Γ x ^ a * Γ y ^ (1 - a))
hx₁ : Γ x ^ a ≠ 0
hy₁ : Γ y ^ (1 - a) ≠ 0
hx₂ : 0 < Γ y
hx₃ : 0 < Γ x
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)

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

Premises used: Real.log_rpow, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
hxy : Γ (a * x + (1 - a) * y) ≤ Γ x ^ a * Γ y ^ (1 - a)
⊢ log (Γ (a * x + (1 - a) * y)) ≤ log (Γ x ^ a * Γ y ^ (1 - a))

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ (a * x + (1 - a) * y) ≤ Γ x ^ a * Γ y ^ (1 - a)

Tactic:
Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma hx hy ha hb hab

Premises used: Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ (a * x + (1 - a) * y) ≤ Γ x ^ a * Γ y ^ (1 - a)

Tactic:
exact Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma hx hy ha hb hab

Premises used: Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ x ^ a ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ y ^ (1 - a) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ y

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ ConvexOn ℝ (Ioi 0) Γ

Tactic:
((convexOn_exp.subset (subset_univ _) ?_).comp convexOn_log_Gamma
          (exp_monotone.monotoneOn _)).congr
      fun x hx => exp_log (Gamma_pos_of_pos hx)

Premises used: Real.Gamma_pos_of_pos, Set.subset_univ, Real.exp_monotone, Real.convexOn_log_Gamma, Real.exp_log, convexOn_exp, ConvexOn.congr, Monotone.monotoneOn, ConvexOn.comp, ConvexOn.subset
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
fun : Convex ℝ (log ∘ Γ '' Ioi 0)
⊢ ConvexOn ℝ (Ioi 0) Γ

Tactic:
refine
    ((convexOn_exp.subset (subset_univ _) ?_).comp convexOn_log_Gamma
          (exp_monotone.monotoneOn _)).congr
      fun x hx => exp_log (Gamma_pos_of_pos hx)

Premises used: Real.Gamma_pos_of_pos, Set.subset_univ, Real.exp_monotone, Real.convexOn_log_Gamma, Real.exp_log, convexOn_exp, ConvexOn.congr, Monotone.monotoneOn, ConvexOn.comp, ConvexOn.subset
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
rw : IsPreconnected (log ∘ Γ '' Ioi 0)
⊢ Convex ℝ (log ∘ Γ '' Ioi 0)

Tactic:
rw [convex_iff_isPreconnected]

Premises used: Real.convex_iff_isPreconnected
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ IsPreconnected (log ∘ Γ '' Ioi 0)

Tactic:
isPreconnected_Ioi.image _ fun x hx => ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousAt.continuousWithinAt, IsPreconnected.image, isPreconnected_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), ContinuousAt (log ∘ Γ) x
⊢ IsPreconnected (log ∘ Γ '' Ioi 0)

Tactic:
refine isPreconnected_Ioi.image _ fun x hx => ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousAt.continuousWithinAt, IsPreconnected.image, isPreconnected_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (log ∘ Γ) x

Tactic:
(differentiableAt_Gamma fun m => ?_).continuousAt.log (Gamma_pos_of_pos hx).ne'

Premises used: Real.Gamma_pos_of_pos, ContinuousAt.log, DifferentiableAt.continuousAt, Real.differentiableAt_Gamma, Real.log, dite, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
refine : ∀ (m : ℕ), x ≠ -(↑m : ℝ)
⊢ ContinuousAt (log ∘ Γ) x

Tactic:
refine (differentiableAt_Gamma fun m => ?_).continuousAt.log (Gamma_pos_of_pos hx).ne'

Premises used: Real.Gamma_pos_of_pos, ContinuousAt.log, DifferentiableAt.continuousAt, Real.differentiableAt_Gamma, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
m : ℕ
⊢ x ≠ -(↑m : ℝ)

Tactic:
(neg_lt_iff_pos_add.mpr (add_pos_of_pos_of_nonneg (mem_Ioi.mp hx) (Nat.cast_nonneg m))).ne'

Premises used: Iff.mpr, Nat.cast_nonneg, Set.mem_Ioi, LT.lt.ne', neg_lt_iff_pos_add, Iff.mp, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
m : ℕ
⊢ x ≠ -(↑m : ℝ)

Tactic:
exact (neg_lt_iff_pos_add.mpr (add_pos_of_pos_of_nonneg (mem_Ioi.mp hx) (Nat.cast_nonneg m))).ne'

Premises used: Iff.mpr, Nat.cast_nonneg, Set.mem_Ioi, LT.lt.ne', neg_lt_iff_pos_add, Iff.mp, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
⊢ f (↑1 : ℝ) = f 1 + log (↑(HSub.hSub (α := ℕ) 1 1)! : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
refine :
  ∀ (m : ℕ) (hm : 1 ≤ m) (IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)), f (↑(m + 1) : ℝ) = f 1 + log (↑(m + 1 - 1)! : ℝ)
⊢ f (↑n : ℝ) = f 1 + log (↑(n - 1)! : ℝ)

Tactic:
refine Nat.le_induction (by simp) (fun m hm IH => ?_) n (Nat.one_le_iff_ne_zero.2 hn)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑m : ℝ)

Tactic:
have A : 0 < (m : ℝ) := Nat.cast_pos.2 hm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
A : LT.lt (α := ℝ) 0 (↑m : ℝ)
simp : f (↑m : ℝ) + log (↑m : ℝ) = f 1 + log (↑m ! : ℝ)
⊢ f (↑(m + 1) : ℝ) = f 1 + log (↑(m + 1 - 1)! : ℝ)

Tactic:
simp only [hf_feq A, Nat.cast_add, Nat.cast_one, Nat.add_succ_sub_one, add_zero]

Premises used: Nat.cast_add, Nat.add_succ_sub_one, add_zero, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
A : LT.lt (α := ℝ) 0 (↑m : ℝ)
rw : f 1 + log (↑((m - 1)! * m) : ℝ) = f 1 + log (↑m ! : ℝ)
⊢ f (↑m : ℝ) + log (↑m : ℝ) = f 1 + log (↑m ! : ℝ)

Tactic:
rw [IH, add_assoc, ← log_mul (Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)) A.ne', ←
    Nat.cast_mul]

Premises used: Iff.mpr, add_assoc, LT.lt.ne', Nat.factorial_ne_zero, Nat.cast_mul, Real.log_mul, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
A : LT.lt (α := ℝ) 0 (↑m : ℝ)
rw : f 1 + log (↑(m.pred ! * (m.pred + 1)) : ℝ)
| f 1 + log (↑m ! : ℝ)

Tactic:
rw [← Nat.succ_pred_eq_of_pos hm, Nat.factorial_succ, mul_comm]

Premises used: Nat.succ_pred_eq_of_pos, Nat.factorial_succ, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
A : LT.lt (α := ℝ) 0 (↑m : ℝ)
conv_rhs : f 1 + log (↑((m - 1)! * m) : ℝ) = f 1 + log (↑(m.pred ! * (m.pred + 1)) : ℝ)
⊢ f 1 + log (↑((m - 1)! * m) : ℝ) = f 1 + log (↑m ! : ℝ)

Tactic:
conv_rhs => rw [← Nat.succ_pred_eq_of_pos hm, Nat.factorial_succ, mul_comm]

Premises used: Nat.succ_pred_eq_of_pos, Nat.factorial_succ, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
A : LT.lt (α := ℝ) 0 (↑m : ℝ)
e_a : m = m.pred + 1
⊢ f 1 + log (↑((m - 1)! * m) : ℝ) = f 1 + log (↑(m.pred ! * (m.pred + 1)) : ℝ)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
A : LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ m = m.pred + 1

Tactic:
(Nat.succ_pred_eq_of_pos hm).symm

Premises used: Nat.succ_pred_eq_of_pos, Eq.symm