n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
n : ℕ
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
have h₁ : ↑0 < ↑4 * ((n:ℝ) + 1) ^ 2 := by positivity
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
have h₃ : ↑0 < (2 * ((n:ℝ) + 1) + 1) ^ 2 := by positivity
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
have h₂ : ↑0 < ↑1 - (1 / (2 * ((n:ℝ) + 1) + 1)) ^ 2 := by
  rw [← mul_lt_mul_right h₃]
  have H : ↑0 < (2 * ((n:ℝ) + 1) + 1) ^ 2 - 1 := by nlinarith [@cast_nonneg ℝ _ n]
  convert H using 1 <;> field_simp [h₃.ne']
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2) ≤ 1 / (4 * ↑(succ n) ^ 2)
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
refine' (log_stirlingSeq_diff_le_geo_sum n).trans _
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 / (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) ≤ 1 / (4 * (↑n + 1) ^ 2)
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2) ≤ 1 / (4 * ↑(succ n) ^ 2)
push_cast
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 * (4 * (↑n + 1) ^ 2) ≤ 1 * (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2)
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 / (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) ≤ 1 / (4 * (↑n + 1) ^ 2)
rw [div_le_div_iff h₂ h₁]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 / (2 * (↑n + 1) + 1) ^ 2 ≤ ((2 * (↑n + 1) + 1) ^ 2 - 1) / (2 * (↑n + 1) + 1) ^ 2
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 * (4 * (↑n + 1) ^ 2) ≤ 1 * (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2)
field_simp [h₃.ne']
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 ≤ (2 * (↑n + 1) + 1) ^ 2 - 1
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 / (2 * (↑n + 1) + 1) ^ 2 ≤ ((2 * (↑n + 1) + 1) ^ 2 - 1) / (2 * (↑n + 1) + 1) ^ 2
rw [div_le_div_right h₃]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + ↑n * 8 + ↑n ^ 2 * 4 ≤ 8 + ↑n * 12 + ↑n ^ 2 * 4
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 ≤ (2 * (↑n + 1) + 1) ^ 2 - 1
ring_nf
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + n * 8 + n ^ 2 * 4 ≤ 8 + n * 12 + n ^ 2 * 4
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + ↑n * 8 + ↑n ^ 2 * 4 ≤ 8 + ↑n * 12 + ↑n ^ 2 * 4
norm_cast
no goals
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + n * 8 + n ^ 2 * 4 ≤ 8 + n * 12 + n ^ 2 * 4
linarith
no goals
n : ℕ
⊢ 0 < 4 * (↑n + 1) ^ 2
positivity
no goals
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ 0 < (2 * (↑n + 1) + 1) ^ 2
positivity
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
rw [← mul_lt_mul_right h₃]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
H : 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2
have H : ↑0 < (2 * ((n:ℝ) + 1) + 1) ^ 2 - 1 := by nlinarith [@cast_nonneg ℝ _ n]
no goals
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
H : 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2
convert H using 1 <;> field_simp [h₃.ne']
no goals
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
nlinarith [@cast_nonneg ℝ _ n]