awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ((↑(n + 1) : ℝ) + x) ≤
    f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))
have refine : f (↑(n + 1) : ℝ) + x * log (↑(n + 1) : ℝ) =
  f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))
Tactic: refine (f_add_nat_le hf_conv (@hf_feq) (Nat.add_one_ne_zero n) hx hx').trans (le_of_eq ?_)
-- 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 (↑(n + 1) : ℝ) + x * log (↑(n + 1) : ℝ) =
    f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))
have rw : f 1 + log (↑n ! : ℝ) + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
  f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))
Tactic: rw [f_nat_eq @hf_feq (by lia : n + 1 ≠ 0), Nat.add_sub_cancel, Nat.cast_add_one]
-- 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
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))) ≤ f x
have rw : f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) ≤ f ((↑(n + 1) : ℝ) + x)
Tactic: rw [← add_sub_assoc, sub_le_iff_le_add, ← f_add_nat_eq (@hf_feq) hx, add_comm x _]
-- 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
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) ≤ f ((↑(n + 1) : ℝ) + x)
have refine_1 : f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) = f (↑(n + 1) : ℝ) + x * log (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1)
Tactic: refine le_trans (le_of_eq ?_) (f_add_nat_ge hf_conv @hf_feq ?_ hx)
-- 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
hx : 0 < x
hn : n ≠ 0
refine_1 : f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) = f (↑(n + 1) : ℝ) + x * log (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) ≤ f ((↑(n + 1) : ℝ) + x)
have refine_2 : 2 ≤ n + 1
Tactic: refine le_trans (le_of_eq ?_) (f_add_nat_ge hf_conv @hf_feq ?_ hx)
-- 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
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) = f (↑(n + 1) : ℝ) + x * log (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1)
have refine_1 : f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) = f 1 + log (↑n ! : ℝ) + x * log (↑n : ℝ)
Tactic: rw [f_nat_eq @hf_feq, Nat.add_sub_cancel, Nat.cast_add_one, add_sub_cancel_right]
-- 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
hx : 0 < x
hn : n ≠ 0
refine_1 : f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) = f 1 + log (↑n ! : ℝ) + x * log (↑n : ℝ)
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) = f (↑(n + 1) : ℝ) + x * log (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1)
have refine_1₁ : n + 1 ≠ 0
Tactic: rw [f_nat_eq @hf_feq, Nat.add_sub_cancel, Nat.cast_add_one, add_sub_cancel_right]
-- 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
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have refine_1 : Tendsto (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop (𝓝 (f x - f 1))
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le' (f := logGammaSeq x)
    (g := fun n ↦ f x - f 1 - x * (log (n + 1) - log n)) ?_ tendsto_const_nhds ?_ ?_
-- 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
refine_1 :
  Tendsto (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop (𝓝 (f x - f 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have refine_2 : ∀ᶠ (b : ℕ) in atTop,
  (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) b ≤ logGammaSeq x b
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le' (f := logGammaSeq x)
    (g := fun n ↦ f x - f 1 - x * (log (n + 1) - log n)) ?_ tendsto_const_nhds ?_ ?_
-- 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
refine_1 :
  Tendsto (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop (𝓝 (f x - f 1))
refine_2 :
  ∀ᶠ (b : ℕ) in atTop,
    (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) b ≤ logGammaSeq x b
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have refine_3 : ∀ᶠ (b : ℕ) in atTop, logGammaSeq x b ≤ f x - f 1
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le' (f := logGammaSeq x)
    (g := fun n ↦ f x - f 1 - x * (log (n + 1) - log n)) ?_ tendsto_const_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
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
⊢ Tendsto (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop (𝓝 (f x - f 1))
have this : f x - f 1 = f x - f 1 - x * 0
Tactic: have : f x - f 1 = f x - f 1 - x * 0 := by ring
-- 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
this : f x - f 1 = f x - f 1 - x * 0
⊢ Tendsto (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop (𝓝 (f x - f 1))
have refine_1 : Tendsto (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
  (𝓝 (f x - f 1 - x * 0))
Tactic: nth_rw 2 [this]
-- 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
⊢ ∀ᶠ (b : ℕ) in atTop,
    (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) b ≤ logGammaSeq x b
have refine_2 : ∀ (n : ℕ), f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) ≤ logGammaSeq x n
Tactic: filter_upwards with 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) - log (↑n : ℝ)) ≤ logGammaSeq x n
have refine_2 : f x ≤ f 1 + (x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) + logGammaSeq x n)
Tactic: rw [sub_le_iff_le_add', sub_le_iff_le_add']
-- 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) - log (↑n : ℝ)) + logGammaSeq x n)
have h : f 1 + (x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) + logGammaSeq x n) =
  f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + logGammaSeq x n
Tactic: convert! le_logGammaSeq hf_conv (@hf_feq) hx hx' n using 1
-- 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 : ℕ) in atTop, logGammaSeq x n ≤ f x - f 1
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x_1 : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x_1 →
        Membership.mem (γ := Set ℕ) {x_2 : ℕ | (fun (n : ℕ) ↦ logGammaSeq x n ≤ f x - f 1) x_2} x_1}
    a
Tactic: filter_upwards [eventually_ne_atTop 0] with n hn using
      le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv hf_feq hx hn)
-- 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
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x_1 : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x_1 →
          Membership.mem (γ := Set ℕ) {x_2 : ℕ | (fun (n : ℕ) ↦ logGammaSeq x n ≤ f x - f 1) x_2} x_1}
      a
⊢ ∀ᶠ (n : ℕ) in atTop, logGammaSeq x n ≤ f x - f 1
have h₁ : ∀ (a : ℕ), a ≠ 0 → logGammaSeq x a ≤ f x - f 1
Tactic: filter_upwards [eventually_ne_atTop 0] with n hn using
      le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv hf_feq hx hn)
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have refine_1 : (↑⌈x - 1⌉₊ : ℝ) < x
Tactic: refine this ⌈x - 1⌉₊ ?_ ?_
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
refine_1 : (↑⌈x - 1⌉₊ : ℝ) < x
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have refine_2 : x ≤ HAdd.hAdd (α := ℝ) (↑⌈x - 1⌉₊ : ℝ) 1
Tactic: refine this ⌈x - 1⌉₊ ?_ ?_
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ (↑⌈x - 1⌉₊ : ℝ) < x
have refine_1 : x < 1 → (↑⌈x - 1⌉₊ : ℝ) < x
Tactic: rcases lt_or_ge x 1 with ⟨⟩
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
refine_1 : x < 1 → (↑⌈x - 1⌉₊ : ℝ) < x
⊢ (↑⌈x - 1⌉₊ : ℝ) < x
have refine_1₁ : 1 ≤ x → (↑⌈x - 1⌉₊ : ℝ) < x
Tactic: rcases lt_or_ge x 1 with ⟨⟩
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
h : x < 1
⊢ x - 1 ≤ 0
have linarith : 0 < x - 1 → x - 1 + (0 - (x - 1)) = 0
Tactic: linarith
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
h : x < 1
⊢ (↑⌈x - 1⌉₊ : ℝ) < x
have refine_1 : (↑0 : ℝ) < x
Tactic: rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
h : 1 ≤ x
⊢ 0 ≤ x - 1
have linarith : x - 1 < 0 → 1 - x + (x - 1 - 0) = 0
Tactic: linarith
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
h : 1 ≤ x
⊢ (↑⌈x - 1⌉₊ : ℝ) < x
have h : x = x - 1 + 1
Tactic: convert! Nat.ceil_lt_add_one (by linarith : 0 ≤ x - 1)
-- 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
this : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ x ≤ HAdd.hAdd (α := ℝ) (↑⌈x - 1⌉₊ : ℝ) 1
have refine_2 : x - 1 ≤ (↑⌈x - 1⌉₊ : ℝ)
Tactic: rw [← sub_le_iff_le_add]
-- 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
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have suffices : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
Tactic: suffices ∀ m : ℕ, ↑m < x → x ≤ m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1) by
    refine this ⌈x - 1⌉₊ ?_ ?_
    · rcases lt_or_ge x 1 with ⟨⟩
      · rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]
      · convert! Nat.ceil_lt_add_one (by linarith : 0 ≤ x - 1)
        abel
    · rw [← sub_le_iff_le_add]; exact Nat.le_ceil _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
x : ℝ
hx : 0 < x
⊢ (↑0 : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have zero : 0 < x → x ≤ 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
Tactic: rw [Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm :
  ∀ {x : ℝ} (hx : 0 < x),
    (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
hy : (↑(m + 1) : ℝ) < x
hy' : x ≤ HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have hy'₁ : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: rw [Nat.cast_succ, ← sub_le_iff_le_add] at hy'
Cleared hypotheses: hy'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm :
  ∀ {x : ℝ} (hx : 0 < x),
    (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
hy : (↑(m + 1) : ℝ) < x
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have hy₁ : (↑m : ℝ) < x - 1
Tactic: rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy
Cleared hypotheses: hy, hy'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm :
  ∀ {x : ℝ} (hx : 0 < x),
    (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have hm₁ : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
Tactic: specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
⊢ ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
have refine : ∀ (n : ℕ) (hn : 1 ≤ n),
  logGammaSeq (x - 1) n =
    logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
Tactic: refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
n : ℕ
hn : 1 ≤ n
⊢ logGammaSeq (x - 1) n =
    logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
have this : logGammaSeq (x - 1 + 1) (n - 1) =
  logGammaSeq (x - 1) (n - 1 + 1) + log (x - 1) -
    (x - 1 + 1) * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ))
Tactic: have := logGammaSeq_add_one (x - 1) (n - 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
n : ℕ
hn : 1 ≤ n
this :
  logGammaSeq (x - 1 + 1) (n - 1) =
    logGammaSeq (x - 1) (n - 1 + 1) + log (x - 1) -
      (x - 1 + 1) * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ))
⊢ logGammaSeq (x - 1) n =
    logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
have this₁ : logGammaSeq x (n - 1) =
  logGammaSeq (x - 1) n + log (x - 1) - x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ))
Tactic: rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
n : ℕ
hn : 1 ≤ n
this :
  logGammaSeq x (n - 1) =
    logGammaSeq (x - 1) n + log (x - 1) - x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ))
⊢ logGammaSeq (x - 1) n =
    logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
have rw : logGammaSeq (x - 1) n =
  logGammaSeq (x - 1) n + log (x - 1) - x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) +
      x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
    log (x - 1)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have this : ∀ᶠ (n : ℕ) in atTop,
  logGammaSeq (x - 1) n =
    logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
Tactic: have :
      ∀ᶠ n : ℕ in atTop,
        logGammaSeq (x - 1) n =
          logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1) := by
      refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)
      have := logGammaSeq_add_one (x - 1) (n - 1)
      rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
      rw [this]
      ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
have hm₁ : Tendsto (α := ℕ)
  ((fun (x_1 : ℕ) ↦
      logGammaSeq x (x_1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(x_1 - 1) : ℝ) 1) - log (↑(x_1 - 1) : ℝ)) - log (x - 1) +
        log (x - 1)) ∘
    fun (a : ℕ) ↦ a + 1)
  atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
Tactic: replace hm :=
      ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
        (tendsto_add_atTop_nat 1)
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : (↑m : ℝ) < x - 1
hy' : x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n =
      logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)
hm :
  Tendsto (α := ℕ)
    ((fun (x_1 : ℕ) ↦
        logGammaSeq x (x_1 - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(x_1 - 1) : ℝ) 1) - log (↑(x_1 - 1) : ℝ)) -
            log (x - 1) +
          log (x - 1)) ∘
      fun (a : ℕ) ↦ a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
⊢ Eq (α := ℕ → ℝ)
    ((fun (x_1 : ℕ) ↦
        HAdd.hAdd (α := ℝ)
          ((fun (n : ℕ) ↦
              logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                log (x - 1))
            x_1)
          ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
      fun (a : ℕ) ↦ a + 1)
    fun (n : ℕ) ↦ logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
have h : ∀ (n : ℕ),
  ((fun (x_1 : ℕ) ↦
          HAdd.hAdd (α := ℝ)
            ((fun (n : ℕ) ↦
                logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) -
                  log (x - 1))
              x_1)
            ((fun (b : ℕ) ↦ log (x - 1)) x_1)) ∘
        fun (a : ℕ) ↦ a + 1)
      n =
    logGammaSeq x n + x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
Tactic: ext1 n