awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
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)
⊢ rexp (-x) * x ^ (a * s + b * t - 1) = f a s x * f b t x
have B : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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 (-x) * x ^ (a * s + b * t - 1) = f a s x * f b t x
have h : rexp (-a * x) * rexp (-b * x) * (x ^ (a * (s - 1)) * x ^ (b * (t - 1))) = f a s x * f b t x
Tactic: rw [A, B]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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))
⊢ 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))
have 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
Tactic: rw [one_div_one_div, one_div_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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))
⊢ 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
have 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))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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))
⊢ 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
have 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))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ ConvexOn ℝ (Ioi 0) (log ∘ Γ)
have 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
Tactic: refine convexOn_iff_forall_pos.mpr ⟨convex_Ioi _, fun x hx y hy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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
have linarith : b < 1 - a → -(a + b - 1) + (b - (1 - a)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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
⊢ b = 1 - a
have linarith₁ : 1 - a < b → a + b - 1 + (1 - a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
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
⊢ (log ∘ Γ) (a • x + b • y) ≤ a • (log ∘ Γ) x + b • (log ∘ Γ) y
have this : b = 1 - a
Tactic: have : b = 1 - a := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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
⊢ (log ∘ Γ) (a • x + b • y) ≤ a • (log ∘ Γ) x + b • (log ∘ Γ) y
have subst : ∀ (hb : 0 < 1 - a) (hab : a + (1 - a) = 1), (log ∘ Γ) (a • x + (1 - a) • y) ≤ a • (log ∘ Γ) x + (1 - a) • (log ∘ Γ) y
Tactic: subst this
Cleared hypotheses: b, hb, hab, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
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
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)
have hx₁ : 0 < x
Tactic: push _ ∈ _ at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
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
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)
have hy₁ : 0 < y
Tactic: push _ ∈ _ at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)
have rw : log (Γ (a * x + (1 - a) * y)) ≤ log (Γ x ^ a * Γ y ^ (1 - a))
Tactic: rw [← log_rpow, ← log_rpow, ← log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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))
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)
have hx₁ : Γ x ^ a ≠ 0
Tactic: rw [← log_rpow, ← log_rpow, ← log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)
have hy₁ : Γ y ^ (1 - a) ≠ 0
Tactic: rw [← log_rpow, ← log_rpow, ← log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)
have hx₂ : 0 < Γ y
Tactic: rw [← log_rpow, ← log_rpow, ← log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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
⊢ log (Γ (a * x + (1 - a) * y)) ≤ a * log (Γ x) + (1 - a) * log (Γ y)
have hx₃ : 0 < Γ x
Tactic: rw [← log_rpow, ← log_rpow, ← log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ log (Γ (a * x + (1 - a) * y)) ≤ log (Γ x ^ a * Γ y ^ (1 - a))
have hxy : Γ (a * x + (1 - a) * y) ≤ Γ x ^ a * Γ y ^ (1 - a)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ ConvexOn ℝ (Ioi 0) Γ
have fun : Convex ℝ (log ∘ Γ '' 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ Convex ℝ (log ∘ Γ '' Ioi 0)
have rw : IsPreconnected (log ∘ Γ '' Ioi 0)
Tactic: rw [convex_iff_isPreconnected]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ IsPreconnected (log ∘ Γ '' Ioi 0)
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), ContinuousAt (log ∘ Γ) x
Tactic: refine isPreconnected_Ioi.image _ fun x hx => ContinuousAt.continuousWithinAt ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (log ∘ Γ) x
have refine : ∀ (m : ℕ), x ≠ -(↑m : ℝ)
Tactic: refine (differentiableAt_Gamma fun m => ?_).continuousAt.log (Gamma_pos_of_pos hx).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
⊢ f (↑n : ℝ) = f 1 + log (↑(n - 1)! : ℝ)
have refine : ∀ (m : ℕ) (hm : 1 ≤ m) (IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)), f (↑(m + 1) : ℝ) = f 1 + log (↑(m + 1 - 1)! : ℝ)
Tactic: refine Nat.le_induction (by simp) (fun m hm IH => ?_) n (Nat.one_le_iff_ne_zero.2 hn)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
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)! : ℝ)
⊢ f (↑(m + 1) : ℝ) = f 1 + log (↑(m + 1 - 1)! : ℝ)
have A : LT.lt (α := ℝ) 0 (↑m : ℝ)
Tactic: have A : 0 < (m : ℝ) := Nat.cast_pos.2 hm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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 : ℝ)
⊢ f (↑(m + 1) : ℝ) = f 1 + log (↑(m + 1 - 1)! : ℝ)
have simp : f (↑m : ℝ) + log (↑m : ℝ) = f 1 + log (↑m ! : ℝ)
Tactic: simp only [hf_feq A, Nat.cast_add, Nat.cast_one, Nat.add_succ_sub_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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 : ℝ)
⊢ f (↑m : ℝ) + log (↑m : ℝ) = f 1 + log (↑m ! : ℝ)
have rw : f 1 + log (↑((m - 1)! * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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 : ℝ)
| f 1 + log (↑m ! : ℝ)
have rw : f 1 + log (↑(m.pred ! * (m.pred + 1)) : ℝ)
Tactic: rw [← Nat.succ_pred_eq_of_pos hm, Nat.factorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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 : ℝ)
⊢ f 1 + log (↑((m - 1)! * m) : ℝ) = f 1 + log (↑m ! : ℝ)
have conv_rhs : f 1 + log (↑((m - 1)! * m) : ℝ) = f 1 + log (↑(m.pred ! * (m.pred + 1)) : ℝ)
Tactic: conv_rhs => rw [← Nat.succ_pred_eq_of_pos hm, Nat.factorial_succ, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
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 : ℝ)
⊢ f 1 + log (↑((m - 1)! * m) : ℝ) = f 1 + log (↑(m.pred ! * (m.pred + 1)) : ℝ)
have e_a : m = m.pred + 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
⊢ x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
have push_cast : x + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = x + (↑n : ℝ) + 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
⊢ f (x + (↑(n + 1) : ℝ)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
have this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
Tactic: have : x + n.succ = x + n + 1 := by push_cast; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
⊢ f (x + (↑(n + 1) : ℝ)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
have succ : f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
  f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
Tactic: rw [this, hf_feq, hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
succ :
  f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
    f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
⊢ f (x + (↑(n + 1) : ℝ)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
have succ₁ : 0 < x + (↑n : ℝ)
Tactic: rw [this, hf_feq, hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
⊢ f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
    f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
have succ : f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
  f x + (log (x + (↑n : ℝ)) + ∑ x_1 ∈ Finset.range n, log (x + (↑x_1 : ℝ)))
Tactic: rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
⊢ 0 < x + (↑n : ℝ)
have linarith : x + (↑n : ℝ) ≤ 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (0 - x) + (x + (↑n : ℝ) - 0) = 0
Tactic: linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
⊢ f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
have zero : f (x + (↑0 : ℝ)) = f x + ∑ m ∈ Finset.range 0, log (x + (↑m : ℝ))
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : x + n.succ = x + n + 1 := by push_cast; ring
    rw [this, hf_feq, hn]
    · rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]
      abel
    · linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
zero : f (x + (↑0 : ℝ)) = f x + ∑ m ∈ Finset.range 0, log (x + (↑m : ℝ))
⊢ f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
have succ : ∀ (n : ℕ) (hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))),
  f (x + (↑(n + 1) : ℝ)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : x + n.succ = x + n + 1 := by push_cast; ring
    rw [this, hf_feq, hn]
    · rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]
      abel
    · linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
⊢ f ((↑n : ℝ) + x) ≤ f (↑n : ℝ) + x * log (↑n : ℝ)
have hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have hn' : 0 < (n : ℝ) := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * (f (↑n : ℝ) + log (↑n : ℝ))
Tactic: rw [hf_feq hn']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ f ((↑n : ℝ) + x) ≤ f (↑n : ℝ) + x * log (↑n : ℝ)
have this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: have : f n + x * log n = (1 - x) * f n + x * f (n + 1) := by rw [hf_feq hn']; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ f ((↑n : ℝ) + x) ≤ f (↑n : ℝ) + x * log (↑n : ℝ)
have rw : f ((1 - x) * (↑n : ℝ) + x * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤
  (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [this, (by ring : (n : ℝ) + x = (1 - x) * n + x * (n + 1))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 0 → -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 0) = 0
Tactic: linarith