awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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))
refine_1 : HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 < 1
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 (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

Premises used: pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 ^ (i + 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))

Tactic:
this

Premises used: DivInvMonoid.div'
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 ^ (i + 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))

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
refine_1 : (HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) 2)⁻¹ < 1
⊢ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 < 1

Tactic:
rw [one_div, inv_pow]

Premises used: inv_pow, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
h_nonneg : 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2
⊢ (HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) 2)⁻¹ < 1

Tactic:
exact inv_lt_one_of_one_lt₀ (one_lt_pow₀ (lt_add_of_pos_left _ <| by positivity) two_ne_zero)

Premises used: inv_lt_one_of_one_lt₀, two_ne_zero, lt_add_of_pos_left, one_lt_pow₀
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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))

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)
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)

Tactic:
mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_

Premises used: pow_nonneg, mul_le_of_le_one_left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 : ℕ
refine : 1 / (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1) ≤ 1
⊢ 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:
refine mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_

Premises used: pow_nonneg, mul_le_of_le_one_left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 : ℕ
rw : (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1)⁻¹ ≤ 1
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1) ≤ 1

Tactic:
rw [one_div]

Premises used: one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 : ℕ
⊢ 0 ≤ HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1)⁻¹ ≤ 1

Tactic:
exact inv_le_one_of_one_le₀ (le_add_of_nonneg_left <| by positivity)

Premises used: inv_le_one_of_one_le₀, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)

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)
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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))
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)
⊢ 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)

Tactic:
hasSum_le hab (log_stirlingSeq_diff_hasSum n) g

Premises used: Stirling.log_stirlingSeq_diff_hasSum, hasSum_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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))
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)
⊢ 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)

Tactic:
exact hasSum_le hab (log_stirlingSeq_diff_hasSum n) g

Premises used: Stirling.log_stirlingSeq_diff_hasSum, hasSum_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
zero :
  log (stirlingSeq 0) - log (stirlingSeq (HAdd.hAdd (α := ℕ) 0 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)
succ :
  ∀ (n : ℕ),
    log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤
      1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ log (stirlingSeq n) - log (stirlingSeq (n + 1)) ≤ 1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
rcases n with (_ | n)
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
this : 0 ≤ log (rexp 1 / √2)
⊢ log (stirlingSeq 0) - log (stirlingSeq (HAdd.hAdd (α := ℕ) 0 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
zero : 0 ≤ log (rexp 1 / √2)
⊢ log (stirlingSeq 0) - log (stirlingSeq (HAdd.hAdd (α := ℕ) 0 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)

Tactic:
suffices 0 ≤ Real.log (Real.exp 1 / Real.sqrt 2) by simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
zero : 1 ≤ rexp 1 / √2
⊢ 0 ≤ log (rexp 1 / √2)

Tactic:
apply Real.log_nonneg

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ 0 < √2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ 0 ≤ rexp 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
zero : 2 ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) 1 1) 2
⊢ 1 ≤ rexp 1 / √2

Tactic:
grw [one_le_div (by positivity), Real.sqrt_le_left (by positivity), ← Real.add_one_le_exp]

Premises used: Real.sqrt_le_left, one_le_div, Real.add_one_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ 2 ≤ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) 1 1) 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ 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

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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
grw : HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1)) 2 < 1
⊢ r < 1

Tactic:
grw [hr, ← n.zero_le]

Premises used: Nat.zero_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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
⊢ HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1)) 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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

Tactic:
have hr1 : r < 1 := by grw [hr, ← n.zero_le]; norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)

Tactic:
hasSum_le (fun j ↦ ?_) (log_stirlingSeq_diff_hasSum n) this

Premises used: Stirling.log_stirlingSeq_diff_hasSum, hasSum_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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))
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
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤
    1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)

Tactic:
refine hasSum_le (fun j ↦ ?_) (log_stirlingSeq_diff_hasSum n) this

Premises used: Stirling.log_stirlingSeq_diff_hasSum, hasSum_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 : ℕ
norm_cast : 3 ≤ 2 * (j + 1) + 1
⊢ 3 ≤ 2 * HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 + 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 * (j + 1) + 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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 : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑(j + 1) : ℝ) + 1) *
      HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (j + 1) ≤
    r ^ (j + 1) / 3

Tactic:
simpa [hr, field] using show (3 : ℝ) ≤ 2 * (j + 1) + 1 by norm_cast; grind
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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
succ :
  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)

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
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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
⊢ 0 ≤ r

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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
⊢ HasSum (fun (j : ℕ) ↦ r ^ (j + 1) / 3)
    (1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))

Tactic:
grind [((hasSum_geometric_of_lt_one (by positivity) hr1).mul_right r).div_const 3]

Premises used: HasSum.div_const, HasSum.mul_right, OfNat.ofNat, hasSum_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
grw :
  1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)
⊢ log (stirlingSeq n) - log (stirlingSeq (n + 1)) ≤ 1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)

Tactic:
grw [log_stirlingSeq_diff_le]

Premises used: Stirling.log_stirlingSeq_diff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
zero :
  1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2)
succ :
  ∀ (n : ℕ),
    1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) ≤
      1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2)
⊢ 1 / (HMul.hMul (α := ℝ) 12 (↑n : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2)

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ 1 / (HMul.hMul (α := ℝ) 12 (↑0 : ℝ) * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
succ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * 4 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * 12
⊢ 1 / (HMul.hMul (α := ℝ) 12 (↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) ≤
    1 / (4 * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * 4 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * 12

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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
grw : 1 / (HMul.hMul (α := ℝ) 12 (↑(k + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(k + 1) : ℝ) 1) ≤ g k - g (k + 1)
⊢ f k - f (k + 1) ≤ g k - g (k + 1)

Tactic:
grw [log_stirlingSeq_diff_le]

Premises used: Stirling.log_stirlingSeq_diff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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
⊢ 1 / (HMul.hMul (α := ℝ) 12 (↑(k + 1) : ℝ) * HAdd.hAdd (α := ℝ) (↑(k + 1) : ℝ) 1) ≤ g k - g (k + 1)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)))
⊢ f 0 - f n ≤ g 0 - g n

Tactic:
rw [Finset.sum_range_sub', Finset.sum_range_sub'] at hf

Premises used: Finset.sum_range_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hf : f 0 - f n ≤ g 0 - g n
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤
    1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
simp only [f, g, zero_add] at hf

Premises used: zero_add
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)
grw : 1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ 12⁻¹
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹

Tactic:
grw [hf]
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
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)
simp : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ 1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ 12⁻¹

Tactic:
simp