-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem tendsto_logGammaSeq_of_le_one (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)

Proof state:
case h.e'_4
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 (↑n + 1) - log ↑n) + logGammaSeq x n) = f 1 + x * log (↑n + 1) - x * log ↑n + logGammaSeq x n

Tactic:
ring

Result:
no goals

Proof state:
case refine_2
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 (↑n + 1) - log ↑n)) b ≤ logGammaSeq x b

Tactic:
filter_upwards with n

Result:
case refine_2.h
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 (↑n + 1) - log ↑n) ≤ logGammaSeq x n

Proof state:
case refine_1
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 (↑n + 1) - log ↑n)) atTop (𝓝 (f x - f 1))

Tactic:
nth_rw 2 [this]

Result:
case refine_1
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 (↑n + 1) - log ↑n)) atTop (𝓝 (f x - f 1 - x * 0))

Proof state:
case refine_2.h
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 (↑n + 1) - log ↑n) + logGammaSeq x n)

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

Result:
case h.e'_4
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 (↑n + 1) - log ↑n) + logGammaSeq x n) = f 1 + x * log (↑n + 1) - x * log ↑n + logGammaSeq x n

Proof state:
case refine_1
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 (↑n + 1) - log ↑n)) atTop (𝓝 (f x - f 1))

Tactic:
have : f x - f 1 = f x - f 1 - x * 0 := by ring

Result:
case refine_1
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 (↑n + 1) - log ↑n)) atTop (𝓝 (f x - f 1))

Proof state:
case refine_2.h
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 (↑n + 1) - log ↑n) ≤ logGammaSeq x n

Tactic:
rw [sub_le_iff_le_add', sub_le_iff_le_add']

Result:
case refine_2.h
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 (↑n + 1) - log ↑n) + logGammaSeq x n)

Proof state:
case refine_1
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 (↑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 _)

Result:
no goals

Proof state:
case refine_3
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

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)

Result:
no goals

Proof state:
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

Result:
no goals

Proof state:
case refine_3
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, logGammaSeq x b ≤ f x - f 1

Tactic:
show ∀ᶠ n : ℕ in atTop, logGammaSeq x n ≤ f x - f 1

Result:
case refine_3
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

Proof state:
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:
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 ?_ ?_

Result:
case refine_1
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 (↑n + 1) - log ↑n)) atTop (𝓝 (f x - f 1))

case refine_2
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 (↑n + 1) - log ↑n)) b ≤ logGammaSeq x b

case refine_3
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, logGammaSeq x b ≤ f x - f 1