awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℕ
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 ! : ℝ))
⊢ f (↑(n + 1) : ℝ) + x * log (↑(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]

Premises used: Real.BohrMollerup.f_nat_eq, Nat.add_sub_cancel, Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
rw : f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) ≤ f ((↑(n + 1) : ℝ) + x)
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))) ≤ f x

Tactic:
rw [← add_sub_assoc, sub_le_iff_le_add, ← f_add_nat_eq (@hf_feq) hx, add_comm x _]

Premises used: add_sub_assoc, sub_le_iff_le_add, add_comm, Real.BohrMollerup.f_add_nat_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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)

Tactic:
le_trans (le_of_eq ?_) (f_add_nat_ge hf_conv @hf_feq ?_ hx)

Premises used: Real.BohrMollerup.f_add_nat_ge, le_of_eq, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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)
refine_2 : 2 ≤ n + 1
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) ≤ f ((↑(n + 1) : ℝ) + x)

Tactic:
refine le_trans (le_of_eq ?_) (f_add_nat_ge hf_conv @hf_feq ?_ hx)

Premises used: Real.BohrMollerup.f_add_nat_ge, le_of_eq, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℝ)
refine_1₁ : n + 1 ≠ 0
⊢ f 1 + (x * log (↑n : ℝ) + log (↑n ! : ℝ)) = f (↑(n + 1) : ℝ) + x * log (HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1)

Tactic:
rw [f_nat_eq @hf_feq, Nat.add_sub_cancel, Nat.cast_add_one, add_sub_cancel_right]

Premises used: Real.BohrMollerup.f_nat_eq, Nat.add_sub_cancel, add_sub_cancel_right, Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 1 + log (↑n ! : ℝ) + x * log (↑n : ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
⊢ n + 1 ≠ 0

Tactic:
Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
⊢ n + 1 ≠ 0

Tactic:
exact Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
⊢ 2 ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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))

Tactic:
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 ?_ ?_

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
refine_3 : ∀ᶠ (b : ℕ) in atTop, logGammaSeq x b ≤ f x - f 1
⊢ Tendsto (logGammaSeq x) 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 ?_ ?_

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
⊢ f x - f 1 = f x - f 1 - x * 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
⊢ f x - f 1 = f x - f 1 - x * 0

Tactic:
have : f x - f 1 = f x - f 1 - x * 0 := by ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
refine_1 :
  Tendsto (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) atTop
    (𝓝 (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))

Tactic:
nth_rw 2 [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - x * 0))

Tactic:
Tendsto.sub tendsto_const_nhds (tendsto_log_nat_add_one_sub_log.const_mul _)

Premises used: tendsto_const_nhds, Filter.Tendsto.const_mul, Real.tendsto_log_nat_add_one_sub_log, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - x * 0))

Tactic:
exact Tendsto.sub tendsto_const_nhds (tendsto_log_nat_add_one_sub_log.const_mul _)

Premises used: tendsto_const_nhds, Filter.Tendsto.const_mul, Real.tendsto_log_nat_add_one_sub_log, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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_2 : ∀ (n : ℕ), f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) ≤ logGammaSeq x n
⊢ ∀ᶠ (b : ℕ) in atTop,
    (fun (n : ℕ) ↦ f x - f 1 - x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))) b ≤ logGammaSeq x b

Tactic:
filter_upwards with n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℕ
refine_2 : f x ≤ f 1 + (x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) + logGammaSeq x n)
⊢ 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']

Premises used: sub_le_iff_le_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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

Tactic:
le_logGammaSeq hf_conv (@hf_feq) hx hx' n

Premises used: Real.BohrMollerup.le_logGammaSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℕ
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
⊢ f x ≤ f 1 + (x * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)) + logGammaSeq x n)

Tactic:
convert! le_logGammaSeq hf_conv (@hf_feq) hx hx' n using 1

Premises used: Real.BohrMollerup.le_logGammaSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : ℕ
hn : n ≠ 0
⊢ logGammaSeq x n ≤ f x - f 1

Tactic:
le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv hf_feq hx hn)

Premises used: Iff.mpr, le_sub_iff_add_le', Real.BohrMollerup.ge_logGammaSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
h₁ h₂ : ∀ (n : ℕ) (hn : n ≠ 0), logGammaSeq x n ≤ f x - f 1
⊢ ∀ᶠ (n : ℕ) in atTop, logGammaSeq x n ≤ 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)

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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))

Tactic:
this ⌈x - 1⌉₊ ?_ ?_

Premises used: HSub.hSub, Nat.ceil, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
refine_2 : x ≤ HAdd.hAdd (α := ℝ) (↑⌈x - 1⌉₊ : ℝ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
refine this ⌈x - 1⌉₊ ?_ ?_

Premises used: HSub.hSub, Nat.ceil, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
refine_1₁ : 1 ≤ x → (↑⌈x - 1⌉₊ : ℝ) < x
⊢ (↑⌈x - 1⌉₊ : ℝ) < x

Tactic:
rcases lt_or_ge x 1 with ⟨⟩

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
linarith : 0 < x - 1 → x - 1 + (0 - (x - 1)) = 0
⊢ x - 1 ≤ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
refine_1 : (↑0 : ℝ) < x
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : 0 < x
⊢ (↑⌈x - 1⌉₊ : ℝ) < x

Tactic:
rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]

Premises used: Iff.mpr, Nat.ceil_eq_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
linarith : x - 1 < 0 → 1 - x + (x - 1 - 0) = 0
⊢ 0 ≤ x - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 : 1 ≤ x
h : x = x - 1 + 1
⊢ (↑⌈x - 1⌉₊ : ℝ) < x

Tactic:
convert! Nat.ceil_lt_add_one (by linarith : 0 ≤ x - 1)

Premises used: Nat.ceil_lt_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 = x - 1 + 1

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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_2 : x - 1 ≤ (↑⌈x - 1⌉₊ : ℝ)
⊢ x ≤ HAdd.hAdd (α := ℝ) (↑⌈x - 1⌉₊ : ℝ) 1

Tactic:
rw [← sub_le_iff_le_add]

Premises used: sub_le_iff_le_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - 1⌉₊ : ℝ)

Tactic:
Nat.le_ceil _

Premises used: Nat.le_ceil
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - 1⌉₊ : ℝ)

Tactic:
exact Nat.le_ceil _

Premises used: Nat.le_ceil
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
suffices : ∀ (m : ℕ), (↑m : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 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 _
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
x : ℝ
hx : 0 < x
zero : 0 < x → x ≤ 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ (↑0 : ℝ) < x → x ≤ HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
rw [Nat.cast_zero, zero_add]

Premises used: zero_add, Nat.cast_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 ≤ 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
fun _ hx' => tendsto_logGammaSeq_of_le_one hf_conv (@hf_feq) hx hx'

Premises used: Real.BohrMollerup.tendsto_logGammaSeq_of_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 ≤ 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
exact fun _ hx' => tendsto_logGammaSeq_of_le_one hf_conv (@hf_feq) hx hx'

Premises used: Real.BohrMollerup.tendsto_logGammaSeq_of_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
⊢ x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
rw [Nat.cast_succ, ← sub_le_iff_le_add] at hy'

Premises used: Nat.cast_succ, sub_le_iff_le_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
⊢ (↑m : ℝ) < x - 1

Tactic:
rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy

Premises used: Nat.cast_succ, lt_sub_iff_add_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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
hy₁ : (↑m : ℝ) < x - 1
⊢ x - 1 ≤ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy

Premises used: Nat.cast_succ, lt_sub_iff_add_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - 1)) atTop (𝓝 (f (x - 1) - f 1))

Tactic:
specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'

Premises used: Nat.cast_nonneg, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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)

Tactic:
Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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))
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)
⊢ ∀ᶠ (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:
refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 + 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 (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

Premises used: Nat.sub_add_cancel, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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) : ℝ))
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)
⊢ logGammaSeq (x - 1) n =
    logGammaSeq x (n - 1) + x * (log (HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) - log (↑(n - 1) : ℝ)) - log (x - 1)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
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 - 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:
ring