awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≤ 1 - x
have linarith : 1 - x < 0 → x - 1 + (1 - x - 0) = 0
Tactic: linarith
-- 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)
⊢ 1 - x + x = 1
have linarith : 1 - x + x < 1 → 1 - x + x - 1 = 0
Tactic: linarith
-- 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)
linarith : 1 - x + x < 1 → 1 - x + x - 1 = 0
⊢ 1 - x + x = 1
have linarith₁ : 1 < 1 - x + x → 1 - (1 - x + x) = 0
Tactic: linarith
-- 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 : 2 ≤ n
hx : 0 < x
⊢ 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
have rw : 1 < n
Tactic: rw [← Nat.cast_one, sub_pos, Nat.cast_lt]
-- 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 : 2 ≤ n
hx : 0 < x
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
Tactic: have npos : 0 < (n : ℝ) - 1 := by rw [← Nat.cast_one, sub_pos, Nat.cast_lt]; lia
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ 0 < (↑n : ℝ) + x
have linarith : (↑n : ℝ) + x ≤ 0 → -1 + (0 - x) + (0 - HSub.hSub (α := ℝ) (↑n : ℝ) 1) + ((↑n : ℝ) + x - 0) = 0
Tactic: linarith
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 < (↑n : ℝ)
have linarith : (↑n : ℝ) ≤ HSub.hSub (α := ℝ) (↑n : ℝ) 1 → -1 + ((↑n : ℝ) - HSub.hSub (α := ℝ) (↑n : ℝ) 1) = 0
Tactic: linarith
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ (↑n : ℝ) < (↑n : ℝ) + x
have linarith : (↑n : ℝ) + x ≤ (↑n : ℝ) → 0 - x + ((↑n : ℝ) + x - (↑n : ℝ)) = 0
Tactic: linarith
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have c : (f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) / ((↑n : ℝ) - HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤
  (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / ((↑n : ℝ) + x - (↑n : ℝ))
Tactic: have c :=
    (convexOn_iff_slope_mono_adjacent.mp <| hf_conv).2 npos (by linarith : 0 < (n : ℝ) + x)
      (by linarith : (n : ℝ) - 1 < (n : ℝ)) (by linarith)
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c :
  (f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) / ((↑n : ℝ) - HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤
    (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / ((↑n : ℝ) + x - (↑n : ℝ))
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have c₁ : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
Tactic: rw [add_sub_cancel_left, sub_sub_cancel, div_one] at c
Cleared hypotheses: c
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
⊢ f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
have rw : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) + log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ)
Tactic: rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
rw : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) + log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ)
⊢ f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
have rw₁ : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1 + 1) = f (↑n : ℝ)
Tactic: rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
rw : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) + log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ)
rw₁ : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1 + 1) = f (↑n : ℝ)
⊢ f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
have rw₂ : f (↑n : ℝ) = f (↑n : ℝ)
Tactic: rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
Tactic: have : f (↑n - 1) = f n - log (↑n - 1) := by
    rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have rwa : ∀ (c : f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x)
  (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
  f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
Tactic: rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c
Cleared hypotheses: c, this
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
rwa :
  ∀ (c : f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x)
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have rwa₁ : ∀ (c : (f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1))) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
  (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
  f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
Tactic: rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c
Cleared hypotheses: c, this
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
rwa :
  ∀ (c : f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x)
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₁ :
  ∀ (c : (f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1))) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have rwa₂ : ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
  (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
  f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
Tactic: rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c
Cleared hypotheses: c, this
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
rwa :
  ∀ (c : f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x)
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₁ :
  ∀ (c : (f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1))) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₂ :
  ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have rwa₃ : ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x + f (↑n : ℝ) ≤ f ((↑n : ℝ) + x))
  (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
  f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
Tactic: rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c
Cleared hypotheses: c, this
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
rwa :
  ∀ (c : f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x)
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₁ :
  ∀ (c : (f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1))) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₂ :
  ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₃ :
  ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x + f (↑n : ℝ) ≤ f ((↑n : ℝ) + x))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have rwa₄ : ∀ (c : x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) + f (↑n : ℝ) ≤ f ((↑n : ℝ) + x))
  (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
  f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
Tactic: rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c
Cleared hypotheses: c, this
-- 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 : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
rwa :
  ∀ (c : f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x)
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₁ :
  ∀ (c : (f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1))) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₂ :
  ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₃ :
  ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x + f (↑n : ℝ) ≤ f ((↑n : ℝ) + x))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₄ :
  ∀ (c : x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) + f (↑n : ℝ) ≤ f ((↑n : ℝ) + x))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
have rwa₅ : ∀ (c : f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x))
  (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
  f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
Tactic: rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c
Cleared hypotheses: c, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
| x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) - ∑ m ∈ Finset.range (n + 1 + 1), log (x + (↑m : ℝ)) + log x -
    (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have rw : x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) - (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
    log x -
  (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: rw [Finset.sum_range_succ', Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) - ∑ m ∈ Finset.range (n + 1 + 1), log (x + (↑m : ℝ)) + log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have conv_rhs : (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
  x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) - (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
      log x -
    (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: conv_rhs => rw [Finset.sum_range_succ', Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have rw : (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
  x * log (↑(n + 1) : ℝ) + (log (↑(n + 1) : ℝ) + log (↑n ! : ℝ)) -
        (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
      log x -
    (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: rw [Nat.cast_mul, log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
rw :
  (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + (log (↑(n + 1) : ℝ) + log (↑n ! : ℝ)) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have hx : Ne (α := ℝ) (↑(n + 1) : ℝ) 0
Tactic: rw [Nat.cast_mul, log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
rw :
  (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + (log (↑(n + 1) : ℝ) + log (↑n ! : ℝ)) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
hx : Ne (α := ℝ) (↑(n + 1) : ℝ) 0
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have hy : Ne (α := ℝ) (↑n ! : ℝ) 0
Tactic: rw [Nat.cast_mul, log_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
⊢ Ne (α := ℝ) (↑(n + 1) : ℝ) 0
have hx : n + 1 ≠ 0
Tactic: rw [Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
⊢ Ne (α := ℝ) (↑n ! : ℝ) 0
have hy : n ! ≠ 0
Tactic: rw [Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
⊢ Eq (α := ℝ) (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)))
    (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)))
have a : ∀ m ∈ Finset.range (n + 1), x + 1 + (↑m : ℝ) = x + (↑(m + 1) : ℝ)
Tactic: congr! 2 with m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n m : ℕ
h : m ∈ Finset.range (n + 1)
⊢ x + 1 + (↑m : ℝ) = x + (↑(m + 1) : ℝ)
have a : x + 1 + (↑m : ℝ) = x + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
x : ℝ
n : ℕ
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + (log (↑(n + 1) : ℝ) + log (↑n ! : ℝ)) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have this : Eq (α := ℝ) (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ))) (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)))
Tactic: have :
    ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) =
      ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) := by
    congr! 2 with m
    push_cast
    abel
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
n : ℕ
this :
  Eq (α := ℝ) (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)))
    (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)))
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + (log (↑(n + 1) : ℝ) + log (↑n ! : ℝ)) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have rw : (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
  x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + log (↑n ! : ℝ)) -
        (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) + log x) +
      log x -
    (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: rw [← this, Nat.cast_add_one n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f x ≤ f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + logGammaSeq x n
have rw : f ((↑(n + 1) : ℝ) + x) ≤
  f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))
Tactic: rw [logGammaSeq, ← add_sub_assoc, le_sub_iff_add_le, ← f_add_nat_eq (@hf_feq) hx, add_comm x]