awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
⊢ HasSum (fun (k : ℕ) ↦ f (k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))
have rw : HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
Tactic: rw [hasSum_nat_add_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
⊢ HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
have h : f = fun (i : ℕ) ↦
  ((↑(m + 1) : ℝ) + 1 / 2) *
    (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * i + 1))
Tactic: convert! (hasSum_log_one_add_inv m.cast_add_one_pos).mul_left ((↑(m + 1) : ℝ) + 1 / 2) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
h :
  f = fun (i : ℕ) ↦
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * i + 1))
⊢ HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
have h₁ : log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
  ((↑(m + 1) : ℝ) + 1 / 2) * log (1 + (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)⁻¹)
Tactic: convert! (hasSum_log_one_add_inv m.cast_add_one_pos).mul_left ((↑(m + 1) : ℝ) + 1 / 2) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
⊢ f = fun (i : ℕ) ↦
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * i + 1))
have h : ∀ (k : ℕ),
  f k =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k + 1))
Tactic: ext k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
k : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k + 1))
have h : 1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) ^ (2 * k) =
  ((↑(m + 1) : ℝ) + 1 / 2) *
    (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) *
      ((1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) *
        HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) 1))
Tactic: rw [← pow_mul, pow_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
k : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) ^ (2 * k) =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) *
        ((1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) *
          HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) 1))
have h : 1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) =
  (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1 / 2) *
    (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) *
      ((1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) *
        HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) 1))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
⊢ log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    ((↑(m + 1) : ℝ) + 1 / 2) * log (1 + (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)⁻¹)
have h : ∀ (x : ℝ) (hx : x ≠ 0), 1 + x⁻¹ = (x + 1) / x
Tactic: have h (x) (hx : x ≠ (0 : ℝ)) : 1 + x⁻¹ = (x + 1) / x := by field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
h : ∀ (x : ℝ) (hx : x ≠ 0), 1 + x⁻¹ = (x + 1) / x
⊢ log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    ((↑(m + 1) : ℝ) + 1 / 2) * log (1 + (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)⁻¹)
have h₁ : log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + log (↑m ! : ℝ) - 1 / 2 * (log 2 + log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)) -
        HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) - 1) -
      (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) + (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + log (↑m ! : ℝ)) -
          1 / 2 * (log 2 + log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) -
        (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) * (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) - 1)) +
    f 0 =
  (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1 / 2) *
    (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) - log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1))
Tactic: simp (disch := positivity) only [log_stirlingSeq_formula, log_div, log_mul, log_exp,
      factorial_succ, cast_mul, cast_succ, range_one, sum_singleton, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
    HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2)
have h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
Tactic: have h_nonneg : (0 : ℝ) ≤ ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 := sq_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
⊢ HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
have refine_2 : ∀
  (this :
    HasSum
      (fun (i : ℕ) ↦
        HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 *
          HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ i)
      (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 *
        (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2)⁻¹)),
  HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
Tactic: have := (hasSum_geometric_of_lt_one h_nonneg ?_).mul_left (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
refine_2 :
  ∀
    (this :
      HasSum
        (fun (i : ℕ) ↦
          HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 *
            HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ i)
        (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 *
          (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2)⁻¹)),
    HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
      (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
        (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
⊢ HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
have refine_1 : HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 < 1
Tactic: have := (hasSum_geometric_of_lt_one h_nonneg ?_).mul_left (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
this :
  HasSum
    (fun (i : ℕ) ↦
      HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 *
        HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ i)
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 *
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2)⁻¹)
⊢ HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
have this₁ : HasSum (fun (i : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (i + 1))
  (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 *
    (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2)⁻¹)
Tactic: simp_rw [← _root_.pow_succ'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
⊢ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 < 1
have refine_1 : (HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) 2)⁻¹ < 1
Tactic: rw [one_div, inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
    HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2)
have g : HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
  (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
    (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
Tactic: have g : HasSum (fun k : ℕ => (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1))
      (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)) := by
    have := (hasSum_geometric_of_lt_one h_nonneg ?_).mul_left (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)
    · simp_rw [← _root_.pow_succ'] at this
      exact this
    rw [one_div, inv_pow]
    exact inv_lt_one_of_one_lt₀ (one_lt_pow₀ (lt_add_of_pos_left _ <| by positivity) two_ne_zero)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
g :
  HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
k : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1) *
      HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1) ≤
    HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1)
have refine : 1 / (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1) ≤ 1
Tactic: refine mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
g :
  HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
k : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1) ≤ 1
have rw : (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1)⁻¹ ≤ 1
Tactic: rw [one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
g :
  HasSum (fun (k : ℕ) ↦ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2))
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
    HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 /
      (1 - HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2)
have hab : ∀ (k : ℕ),
  1 / (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1) *
      HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1) ≤
    HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (k + 1)
Tactic: have hab (k : ℕ) : (1 : ℝ) / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1) ≤
      (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1) := by
    refine mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_
    rw [one_div]
    exact inv_le_one_of_one_le₀ (le_add_of_nonneg_left <| by positivity)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
⊢ log (stirlingSeq n) - log (stirlingSeq (n + 1)) ≤ 1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have zero : log (stirlingSeq 0) - log (stirlingSeq (HAdd.hAdd (α := ℕ) 0 1)) ≤
  1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)
Tactic: rcases n with (_ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
zero :
  log (stirlingSeq 0) - log (stirlingSeq (HAdd.hAdd (α := ℕ) 0 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)
⊢ log (stirlingSeq n) - log (stirlingSeq (n + 1)) ≤ 1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have succ : ∀ (n : ℕ),
  log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
Tactic: rcases n with (_ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ log (stirlingSeq 0) - log (stirlingSeq (HAdd.hAdd (α := ℕ) 0 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)
have zero : 0 ≤ log (rexp 1 / √2)
Tactic: suffices 0 ≤ Real.log (Real.exp 1 / Real.sqrt 2) by simpa
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ 0 ≤ log (rexp 1 / √2)
have zero : 1 ≤ rexp 1 / √2
Tactic: apply Real.log_nonneg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ 1 ≤ rexp 1 / √2
have zero : 2 ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) 1 1) 2
Tactic: grw [one_le_div (by positivity), Real.sqrt_le_left (by positivity), ← Real.add_one_le_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
have hr : let r := HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2;
r = HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
Tactic: set r := ((1 : ℝ) / (2 * (n + 1) + 1)) ^ 2 with hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
r : ℝ := HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr : r = HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
⊢ r < 1
have grw : HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1)) 2 < 1
Tactic: grw [hr, ← n.zero_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
r : ℝ := HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr : r = HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
have hr1 : r < 1
Tactic: have hr1 : r < 1 := by grw [hr, ← n.zero_le]; norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
r : ℝ := HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr : r = HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr1 : r < 1
this :
  HasSum (fun (j : ℕ) ↦ r ^ (j + 1) / 3)
    (1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
have refine : ∀ (j : ℕ),
  1 / (HMul.hMul (α := ℝ) 2 (↑(j + 1) : ℝ) + 1) *
      HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (j + 1) ≤
    r ^ (j + 1) / 3
Tactic: refine hasSum_le (fun j ↦ ?_) (log_stirlingSeq_diff_hasSum n) this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
r : ℝ := HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr : r = HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr1 : r < 1
this :
  HasSum (fun (j : ℕ) ↦ r ^ (j + 1) / 3)
    (1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))
j : ℕ
⊢ 3 ≤ 2 * HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 + 1
have norm_cast : 3 ≤ 2 * (j + 1) + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
r : ℝ := HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr : r = HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) 2
hr1 : r < 1
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
have succ : HasSum (fun (j : ℕ) ↦ r ^ (j + 1) / 3)
  (1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))
Tactic: suffices HasSum (fun j ↦ r ^ (j + 1) / 3) ((1 : ℝ) / (12 * (n + 1 : ℕ) * ((n + 1 : ℕ) + 1))) by
    refine hasSum_le (fun j ↦ ?_) (log_stirlingSeq_diff_hasSum n) this
    simpa [hr, field] using show (3 : ℝ) ≤ 2 * (j + 1) + 1 by norm_cast; grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
⊢ log (stirlingSeq n) - log (stirlingSeq (n + 1)) ≤ 1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
have grw : 1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ 1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
Tactic: grw [log_stirlingSeq_diff_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
have zero : 1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) ≤ 1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
zero :
  1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2)
⊢ 1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
have succ : ∀ (n : ℕ),
  1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2)
have succ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * 4 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * 12
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
k : ℕ
hk : k ∈ range n
⊢ f k - f (k + 1) ≤ g k - g (k + 1)
have grw : 1 / (HMul.hMul (α := ℝ) 12 (↑(k + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(k + 1) : ℝ) 1) ≤ g k - g (k + 1)
Tactic: grw [log_stirlingSeq_diff_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
have hf : ∀ (k : ℕ) (hk : k ∈ range n), f k - f (k + 1) ≤ g k - g (k + 1)
Tactic: have hf k (hk : k ∈ range n) : f k - (f (k + 1)) ≤ g k - g (k + 1) := by
    grw [log_stirlingSeq_diff_le]
    simp [field]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hf : ∀ (k : ℕ) (hk : k ∈ range n), f k - f (k + 1) ≤ g k - g (k + 1)
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
have hf₁ : LE.le (α := ℝ) (∑ i ∈ range n, (f i - f (i + 1))) (∑ i ∈ range n, (g i - g (i + 1)))
Tactic: replace hf := Finset.sum_le_sum hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hf : LE.le (α := ℝ) (∑ i ∈ range n, (f i - f (i + 1))) (∑ i ∈ range n, (g i - g (i + 1)))
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
have hf₁ : f 0 - f n ≤ g 0 - g n
Tactic: rw [Finset.sum_range_sub', Finset.sum_range_sub'] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hf :
  log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤
    1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
have grw : 1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ 12⁻¹
Tactic: grw [hf]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hf :
  log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤
    1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ 12⁻¹
have simp : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
⊢ HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
have this : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
Tactic: have := log_stirlingSeq_bounded_aux n