internlm/Lean-Github huggingface dataset:
Theorem: taylor_mean_remainder_bound_central
Proof state before:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
rw [h, norm_div, norm_mul, Real.norm_coe_nat, Real.norm_eq_abs ((x - x₀) ^ _), ← abs_pow]
Proof state after:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| / ↑(n + 1)! ≤ C * |(x - x₀) ^ (n + 1)| / ↑(n + 1)!
Theorem: taylor_mean_remainder_bound_central
Proof state before:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| / ↑(n + 1)! ≤ C * |(x - x₀) ^ (n + 1)| / ↑(n + 1)!
Tactic:
refine' div_le_div_of_le (Nat.cast_nonneg _) _
Proof state after:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| ≤ C * |(x - x₀) ^ (n + 1)|
Theorem: taylor_mean_remainder_bound_central
Proof state before:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| ≤ C * |(x - x₀) ^ (n + 1)|
Tactic:
exact mul_le_mul_of_nonneg_right (hC _ hx') (abs_nonneg _)
Proof state after:
no goals
Theorem: taylor_mean_remainder_bound_central
Proof state before:
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ Icc a a
hx₀ : x₀ ∈ Icc a a
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
simp only [Icc_self, mem_singleton_iff] at hx hx₀
Proof state after:
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
hx : x = a
hx₀ : x₀ = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Theorem: taylor_mean_remainder_bound_central
Proof state before:
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
hx : x = a
hx₀ : x₀ = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
substs hx₀ hx
Proof state after:
case inl
f : ℝ → ℝ
C x : ℝ
n : ℕ
hab : x ≤ x
hf : ContDiffOn ℝ (↑n + 1) f (Icc x x)
hC : ∀ y ∈ Ioo x x, ‖iteratedDerivWithin (n + 1) f (Icc x x) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc x x) x x‖ ≤ C * |x - x| ^ (n + 1) / ↑(n + 1)!
Theorem: taylor_mean_remainder_bound_central
Proof state before:
case inl
f : ℝ → ℝ
C x : ℝ
n : ℕ
hab : x ≤ x
hf : ContDiffOn ℝ (↑n + 1) f (Icc x x)
hC : ∀ y ∈ Ioo x x, ‖iteratedDerivWithin (n + 1) f (Icc x x) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc x x) x x‖ ≤ C * |x - x| ^ (n + 1) / ↑(n + 1)!
Tactic:
rw [taylorWithinEval_self, sub_self, sub_self, abs_zero, zero_pow Nat.succ_pos',
  MulZeroClass.mul_zero, zero_div, norm_zero]
Proof state after:
no goals
Theorem: taylor_mean_remainder_bound_central
Proof state before:
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
⊢ DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
Tactic:
refine'
  (hf.differentiable_on_iterated_deriv_within _ (uniqueDiffOn_Icc hab)).mono Ioo_subset_Icc_self
Proof state after:
no goals
Theorem: exists_taylor_mean_remainder_bound_central
Proof state before:
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
rcases eq_or_lt_of_le hab with (rfl | h)
Proof state after:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
⊢ ∃ C, ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)

case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Theorem: exists_taylor_mean_remainder_bound_central
Proof state before:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
let C := Sup ((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
Proof state after:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
C : Type := Sup ↑((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Theorem: exists_taylor_mean_remainder_bound_central
Proof state before:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
C : Type := Sup ↑((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
refine' ⟨C / (n + 1)!, fun x hx => _⟩
Proof state after:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
C : Type := Sup ↑((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ sorryAx ℝ true * |x - x₀| ^ (n + 1)
Theorem: exists_taylor_mean_remainder_bound_central
Proof state before:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
⊢ ∃ C, ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
refine' ⟨0, fun x hx => _⟩
Proof state after:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)
Theorem: exists_taylor_mean_remainder_bound_central
Proof state before:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)
Tactic:
rw [Icc_self, mem_singleton_iff] at hx hx₀
Proof state after:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ = a
x : ℝ
hx : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)
Theorem: exists_taylor_mean_remainder_bound_central
Proof state before:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ = a
x : ℝ
hx : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)
Tactic:
rw [hx₀, hx, taylorWithinEval_self, sub_self, MulZeroClass.zero_mul, norm_zero]
Proof state after:
no goals
Theorem: Fin.ne_zero_iff_eq_one
Proof state before:
⊢ ∀ {x : Fin 2}, x ≠ 0 ↔ x = 1
Tactic:
decide
Proof state after:
no goals
Theorem: Fin.eq_zero_iff_ne_one
Proof state before:
⊢ ∀ {x : Fin 2}, x = 0 ↔ x ≠ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Fin.fin_two_eq_zero_of_ne_one
Proof state before:
x : Fin 2
hx : x ≠ 1
⊢ x = 0
Tactic:
rwa [Fin.eq_zero_iff_ne_one]
Proof state after:
no goals
Theorem: iteratedFDerivWithin_nhds
Proof state before:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
u : Set E
x : E
f : E → F
n : ℕ
hu : u ∈ 𝓝 x
⊢ iteratedFDerivWithin 𝕜 n f u x = iteratedFDeriv 𝕜 n f x
Tactic:
rw [← iteratedFDerivWithin_univ, ← univ_inter u, iteratedFDerivWithin_inter hu]
Proof state after:
no goals
Theorem: iteratedDerivWithin_of_isOpen
Proof state before:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
f : 𝕜 → F
n : ℕ
hs : IsOpen s
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
Tactic:
rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_of_isOpen _ hs hx]
Proof state after:
no goals
Theorem: iteratedDerivWithin_nhds
Proof state before:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
u : Set 𝕜
x : 𝕜
f : 𝕜 → F
n : ℕ
hu : u ∈ 𝓝 x
⊢ iteratedDerivWithin n f u x = iteratedDeriv n f x
Tactic:
rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_nhds hu]
Proof state after:
no goals
Theorem: Nat.choose_add_le_pow_left
Proof state before:
s t : ℕ
⊢ choose (s + t) s ≤ (t + 1) ^ s
Tactic:
rw [add_comm, choose_eq_asc_factorial_div_factorial]
Proof state after:
s t : ℕ
⊢ ascFactorial t s / s ! ≤ (t + 1) ^ s
Theorem: Nat.choose_add_le_pow_left
Proof state before:
s t : ℕ
⊢ ascFactorial t s / s ! ≤ (t + 1) ^ s
Tactic:
exact Nat.div_le_of_le_mul asc_le_pow_mul_factorial
Proof state after:
no goals
Theorem: Nat.choose_le_pow_left
Proof state before:
s t : ℕ
⊢ choose s t ≤ (s + 1 - t) ^ t
Tactic:
cases' le_or_lt t s with h h
Proof state after:
case inl
s t : ℕ
h : t ≤ s
⊢ choose s t ≤ (s + 1 - t) ^ t

case inr
s t : ℕ
h : s < t
⊢ choose s t ≤ (s + 1 - t) ^ t
Theorem: Nat.choose_le_pow_left
Proof state before:
case inr
s t : ℕ
h : s < t
⊢ choose s t ≤ (s + 1 - t) ^ t
Tactic:
rw [choose_eq_zero_of_lt h]
Proof state after:
case inr
s t : ℕ
h : s < t
⊢ 0 ≤ (s + 1 - t) ^ t
Theorem: Nat.choose_le_pow_left
Proof state before:
case inr
s t : ℕ
h : s < t
⊢ 0 ≤ (s + 1 - t) ^ t
Tactic:
exact zero_le'
Proof state after:
no goals
Theorem: Nat.choose_le_pow_left
Proof state before:
case inl
s t : ℕ
h : t ≤ s
⊢ choose s t ≤ (s + 1 - t) ^ t
Tactic:
obtain ⟨s, rfl⟩ := exists_add_of_le h
Proof state after:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ choose (t + s) t ≤ (t + s + 1 - t) ^ t
Theorem: Nat.choose_le_pow_left
Proof state before:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ choose (t + s) t ≤ (t + s + 1 - t) ^ t
Tactic:
refine (choose_add_le_pow_left t s).trans ?_
Proof state after:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ (s + 1) ^ t ≤ (t + s + 1 - t) ^ t
Theorem: Nat.choose_le_pow_left
Proof state before:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ (s + 1) ^ t ≤ (t + s + 1 - t) ^ t
Tactic:
rw [add_assoc, Nat.add_sub_cancel_left]
Proof state after:
no goals
Theorem: sum_tsub
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : ExistsAddOfLE β
inst✝³ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub β
inst✝ : OrderedSub β
s : Finset α
f g : α → β
hfg : ∀ x ∈ s, g x ≤ f x
⊢ ∑ x in s, (f x - g x) + ∑ x in s, g x = ∑ x in s, f x
Tactic:
rw [← Finset.sum_add_distrib]
Proof state after:
α : Type u_1
β : Type u_2
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : ExistsAddOfLE β
inst✝³ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub β
inst✝ : OrderedSub β
s : Finset α
f g : α → β
hfg : ∀ x ∈ s, g x ≤ f x
⊢ ∑ x in s, (f x - g x + g x) = ∑ x in s, f x
Theorem: sum_tsub
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : ExistsAddOfLE β
inst✝³ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub β
inst✝ : OrderedSub β
s : Finset α
f g : α → β
hfg : ∀ x ∈ s, g x ≤ f x
⊢ ∑ x in s, (f x - g x + g x) = ∑ x in s, f x
Tactic:
exact Finset.sum_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx
Proof state after:
no goals
Theorem: Nat.asc_le_pow_mul_factorial
Proof state before:
s t : ℕ
⊢ ascFactorial t s ≤ s ! * (t + 1) ^ s
Tactic:
induction' s with s ih
Proof state after:
case zero
t : ℕ
⊢ ascFactorial t zero ≤ zero ! * (t + 1) ^ zero

case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ ascFactorial t (succ s) ≤ (succ s)! * (t + 1) ^ succ s
Theorem: Nat.asc_le_pow_mul_factorial
Proof state before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ ascFactorial t (succ s) ≤ (succ s)! * (t + 1) ^ succ s
Tactic:
rw [ascFactorial_succ, factorial_succ, pow_succ', mul_mul_mul_comm]
Proof state after:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ (t + s + 1) * ascFactorial t s ≤ (s + 1) * (t + 1) * (s ! * (t + 1) ^ s)
Theorem: Nat.asc_le_pow_mul_factorial
Proof state before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ (t + s + 1) * ascFactorial t s ≤ (s + 1) * (t + 1) * (s ! * (t + 1) ^ s)
Tactic:
refine' Nat.mul_le_mul _ ih
Proof state after:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ t + s + 1 ≤ (s + 1) * (t + 1)
Theorem: Nat.asc_le_pow_mul_factorial
Proof state before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ t + s + 1 ≤ (s + 1) * (t + 1)
Tactic:
rw [add_comm t, add_one_mul s, mul_add_one s, add_assoc]
Proof state after:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ s + (t + 1) ≤ s * t + s + (t + 1)
Theorem: Nat.asc_le_pow_mul_factorial
Proof state before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ s + (t + 1) ≤ s * t + s + (t + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.asc_le_pow_mul_factorial
Proof state before:
case zero
t : ℕ
⊢ ascFactorial t zero ≤ zero ! * (t + 1) ^ zero
Tactic:
simp
Proof state after:
no goals
Theorem: centralBinom_ratio
Proof state before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom (n + 1)) / ↑(centralBinom n) = 4 * ((↑n + 1 / 2) / (↑n + 1))
Tactic:
rw [mul_div_assoc', mul_add, eq_div_iff, ← cast_add_one, div_mul_eq_mul_div, mul_comm, ← cast_mul,
  succ_mul_centralBinom_succ, cast_mul, mul_div_cancel]
Proof state after:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * (2 * n + 1)) = 4 * ↑n + 4 * (1 / 2)

case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom n) ≠ 0

α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑n + 1 ≠ 0
Theorem: centralBinom_ratio
Proof state before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑n + 1 ≠ 0
Tactic:
exact Nat.cast_add_one_ne_zero _
Proof state after:
no goals
Theorem: centralBinom_ratio
Proof state before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * (2 * n + 1)) = 4 * ↑n + 4 * (1 / 2)
Tactic:
rw [mul_add_one, ← mul_assoc, cast_add, cast_mul]
Proof state after:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * 2) * ↑n + ↑2 = 4 * ↑n + 4 * (1 / 2)
Theorem: centralBinom_ratio
Proof state before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * 2) * ↑n + ↑2 = 4 * ↑n + 4 * (1 / 2)
Tactic:
norm_num1
Proof state after:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ 4 * ↑n + 2 = 4 * ↑n + 2
Theorem: centralBinom_ratio
Proof state before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ 4 * ↑n + 2 = 4 * ↑n + 2
Tactic:
rfl
Proof state after:
no goals
Theorem: centralBinom_ratio
Proof state before:
case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom n) ≠ 0
Tactic:
rw [Nat.cast_ne_zero]
Proof state after:
case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ centralBinom n ≠ 0
Theorem: centralBinom_ratio
Proof state before:
case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ centralBinom n ≠ 0
Tactic:
exact centralBinom_ne_zero _
Proof state after:
no goals
Theorem: upper_monotone_aux
Proof state before:
n : ℕ
⊢ (↑n + 1 / 2) / (↑n + 1) ≤ Real.sqrt (↑n + 1 / 3) / Real.sqrt (↑n + 1 + 1 / 3)
Tactic:
rw [← Real.sqrt_div]
Proof state after:
n : ℕ
⊢ (↑n + 1 / 2) / (↑n + 1) ≤ Real.sqrt ((↑n + 1 / 3) / (↑n + 1 + 1 / 3))

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Theorem: upper_monotone_aux
Proof state before:
n : ℕ
⊢ (↑n + 1 / 2) / (↑n + 1) ≤ Real.sqrt ((↑n + 1 / 3) / (↑n + 1 + 1 / 3))

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Tactic:
refine' Real.le_sqrt_of_sq_le _
Proof state after:
n : ℕ
⊢ ((↑n + 1 / 2) / (↑n + 1)) ^ 2 ≤ (↑n + 1 / 3) / (↑n + 1 + 1 / 3)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Theorem: upper_monotone_aux
Proof state before:
n : ℕ
⊢ ((↑n + 1 / 2) / (↑n + 1)) ^ 2 ≤ (↑n + 1 / 3) / (↑n + 1 + 1 / 3)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Tactic:
rw [div_pow, div_le_div_iff]
Proof state after:
n : ℕ
⊢ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 3) ≤ (↑n + 1 / 3) * (↑n + 1) ^ 2

case b0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

case d0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 3

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Theorem: upper_monotone_aux
Proof state before:
case b0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

case d0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 3

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Tactic:
all_goals positivity
Proof state after:
no goals
Theorem: upper_monotone_aux
Proof state before:
n : ℕ
⊢ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 3) ≤ (↑n + 1 / 3) * (↑n + 1) ^ 2
Tactic:
ring_nf
Proof state after:
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑3 + ↑n * (↑(Int.ofNat 19) / ↑12) + ↑n ^ 2 * (↑(Int.ofNat 7) / ↑3) + ↑n ^ 3 ≤
    ↑(Int.ofNat 1) / ↑3 + ↑n * (↑(Int.ofNat 5) / ↑3) + ↑n ^ 2 * (↑(Int.ofNat 7) / ↑3) + ↑n ^ 3
Theorem: upper_monotone_aux
Proof state before:
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑3 + ↑n * (↑(Int.ofNat 19) / ↑12) + ↑n ^ 2 * (↑(Int.ofNat 7) / ↑3) + ↑n ^ 3 ≤
    ↑(Int.ofNat 1) / ↑3 + ↑n * (↑(Int.ofNat 5) / ↑3) + ↑n ^ 2 * (↑(Int.ofNat 7) / ↑3) + ↑n ^ 3
Tactic:
gcongr _ + _ * ?_ + _ + _
Proof state after:
case bc.bc.bc.h
n : ℕ
⊢ ↑(Int.ofNat 19) / ↑12 ≤ ↑(Int.ofNat 5) / ↑3
Theorem: upper_monotone_aux
Proof state before:
case bc.bc.bc.h
n : ℕ
⊢ ↑(Int.ofNat 19) / ↑12 ≤ ↑(Int.ofNat 5) / ↑3
Tactic:
norm_num1
Proof state after:
no goals
Theorem: upper_monotone_aux
Proof state before:
case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Tactic:
positivity
Proof state after:
no goals
Theorem: lower_monotone_aux
Proof state before:
n : ℕ
⊢ Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4) ≤ (↑n + 1 / 2) / (↑n + 1)
Tactic:
rw [← Real.sqrt_div, sqrt_le_left, div_pow, div_le_div_iff]
Proof state after:
n : ℕ
⊢ (↑n + 1 / 4) * (↑n + 1) ^ 2 ≤ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 4)

case b0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 4

case d0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

n : ℕ
⊢ 0 ≤ (↑n + 1 / 2) / (↑n + 1)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 4
Theorem: lower_monotone_aux
Proof state before:
case b0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 4

case d0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

n : ℕ
⊢ 0 ≤ (↑n + 1 / 2) / (↑n + 1)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 4
Tactic:
all_goals positivity
Proof state after:
no goals
Theorem: lower_monotone_aux
Proof state before:
n : ℕ
⊢ (↑n + 1 / 4) * (↑n + 1) ^ 2 ≤ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 4)
Tactic:
ring_nf
Proof state after:
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3 ≤
    ↑(Int.ofNat 5) / ↑16 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3
Theorem: lower_monotone_aux
Proof state before:
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3 ≤
    ↑(Int.ofNat 5) / ↑16 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3
Tactic:
gcongr ?_ + _ + _ + _
Proof state after:
case bc.bc.bc
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 ≤ ↑(Int.ofNat 5) / ↑16
Theorem: lower_monotone_aux
Proof state before:
case bc.bc.bc
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 ≤ ↑(Int.ofNat 5) / ↑16
Tactic:
norm_num1
Proof state after:
no goals
Theorem: lower_monotone_aux
Proof state before:
case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 4
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialLower_monotone
Proof state before:
⊢ Monotone centralBinomialLower
Tactic:
refine' monotone_nat_of_le_succ _
Proof state after:
⊢ ∀ (n : ℕ), centralBinomialLower n ≤ centralBinomialLower (n + 1)
Theorem: centralBinomialLower_monotone
Proof state before:
⊢ ∀ (n : ℕ), centralBinomialLower n ≤ centralBinomialLower (n + 1)
Tactic:
intro n
Proof state after:
n : ℕ
⊢ centralBinomialLower n ≤ centralBinomialLower (n + 1)
Theorem: centralBinomialLower_monotone
Proof state before:
n : ℕ
⊢ centralBinomialLower n ≤ centralBinomialLower (n + 1)
Tactic:
rw [centralBinomialLower, centralBinomialLower, _root_.pow_succ, ←div_div]
Proof state after:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) / 4 ^ n ≤
    ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4 / 4 ^ n
Theorem: centralBinomialLower_monotone
Proof state before:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) / 4 ^ n ≤
    ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4 / 4 ^ n
Tactic:
refine' div_le_div_of_le (by positivity) _
Proof state after:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) ≤ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4
Theorem: centralBinomialLower_monotone
Proof state before:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) ≤ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4
Tactic:
rw [le_div_iff, mul_assoc, mul_comm, ← div_le_div_iff, centralBinom_ratio, mul_comm,
  mul_div_assoc, Nat.cast_add_one]
Proof state after:
n : ℕ
⊢ 4 * (Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4)) ≤ 4 * ((↑n + 1 / 2) / (↑n + 1))

case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)

case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)

n : ℕ
⊢ 0 < 4
Theorem: centralBinomialLower_monotone
Proof state before:
n : ℕ
⊢ 4 * (Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4)) ≤ 4 * ((↑n + 1 / 2) / (↑n + 1))

case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)

case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)

n : ℕ
⊢ 0 < 4
Tactic:
refine' mul_le_mul_of_nonneg_left (lower_monotone_aux n) (by positivity)
Proof state after:
case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)

case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)

n : ℕ
⊢ 0 < 4
Theorem: centralBinomialLower_monotone
Proof state before:
n : ℕ
⊢ 0 ≤ 4 ^ n
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialLower_monotone
Proof state before:
n : ℕ
⊢ 0 ≤ 4
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialLower_monotone
Proof state before:
case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialLower_monotone
Proof state before:
case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)
Tactic:
rw [Nat.cast_pos]
Proof state after:
case d0
n : ℕ
⊢ 0 < centralBinom n