Zulip Chat Archive
Stream: Is there code for X?
Topic: Upper and Lower Bounds of Cosine
Yongxi Lin (Aaron) (Oct 21 2025 at 06:17):
I want to prove in lean that for 0 ≤ x ≤ 1, 1-x^2/2+x^4/4-x^6/6 ≤ cos x ≤ 1-x^2/2+x^4/4 (and more generally we want more terms in this inequality). More specifically I just want this inequality for x=1.
This kind of inequality is mentioned in this post #Is there code for X? > 0.54 < Real.cos 1 ∧ Real.cos 1 < 0.55 made roughly two years ago, I wonder whether we have a result in Mathlib now that can help me to prove them.
Yury G. Kudryashov (Oct 21 2025 at 17:04):
You can use this. Could you please open a Mathlib PR with this lemma + individual bounds as corollaries + non-strict inequality versions + versions for negative x?
theorem Real.sin_cos_bound_of_pos (x : ℝ) (hx : 0 < x) (n : ℕ) :
(∑ i ∈ .range (2 * n + 2), (-1) ^ i * x ^ (2 * i + 1) / (2 * i + 1)! < x.sin) ∧
(x.sin < ∑ i ∈ .range (2 * n + 1), (-1) ^ i * x ^ (2 * i + 1) / (2 * i + 1)!) ∧
(∑ i ∈ .range (2 * n + 2), (-1) ^ i * x ^ (2 * i) / (2 * i)! < x.cos) ∧
(x.cos < ∑ i ∈ .range (2 * n + 3), (-1) ^ i * x ^ (2 * i) / (2 * i)!) := by
have H₀ (x : ℝ) (n : ℕ) (k : ℕ → ℕ) :
HasDerivAt (fun x : ℝ ↦ ∑ i ∈ .range n, (-1) ^ i * x ^ (k i) / (k i)!)
(∑ i ∈ .range n, (-1) ^ i * k i * x ^ (k i - 1) / (k i)!) x := by
refine HasDerivAt.fun_sum fun i hi ↦ ?_
simpa only [mul_assoc] using ((hasDerivAt_pow (k i) x).const_mul _).div_const _
set cosSeries := fun (n : ℕ) (x : ℝ) ↦ ∑ i ∈ .range n, (-1) ^ i * x ^ (2 * i) / (2 * i)!
set sinSeries := fun (n : ℕ) (x : ℝ) ↦ ∑ i ∈ .range n, (-1) ^ i * x ^ (2 * i + 1) / (2 * i + 1)!
have Hcos₀ (n) : cosSeries (n + 1) 0 = 1 := by simp [cosSeries, Finset.sum_range_succ']
have Hsin₀ (n) : sinSeries n 0 = 0 := by simp [sinSeries]
have HsinDeriv (x : ℝ) (n : ℕ) : HasDerivAt (sin - sinSeries n) (cos x - cosSeries n x) x := by
convert (hasDerivAt_sin x).sub (H₀ _ _ _) using 1
simp (disch := positivity) [Nat.factorial_succ, field, mul_assoc,
mul_left_comm _ (2 * _ + 1 : ℝ), mul_div_mul_left]
have HcosDeriv (x : ℝ) (n : ℕ) :
HasDerivAt (cos - cosSeries (n + 1)) (-sin x + sinSeries n x) x := by
rw [← sub_neg_eq_add (-sin x)]
convert (hasDerivAt_cos x).sub (H₀ _ _ _) using 2
rw [Finset.sum_range_succ', ← Finset.sum_neg_distrib, eq_comm]
convert add_zero _ using 2
· simp
· simp [field, Nat.factorial_succ, mul_add_one]
ring
have Hstep_sin_cos (n : ℕ) (ih : ∀ x > 0, sin x < sinSeries n x) (x : ℝ) (hx : 0 < x) :
cosSeries (n + 1) x < cos x := by
suffices StrictMonoOn (cos - cosSeries (n + 1)) (.Ici 0) by
simpa [Hcos₀] using this Set.left_mem_Ici hx.le hx
apply strictMonoOn_of_deriv_pos
· apply convex_Ici
· simp only [cosSeries, Pi.sub_def]
fun_prop
· simpa [(HcosDeriv _ _).deriv] using ih
have Hstep_sin_cos' (n : ℕ) (ih : ∀ x > 0, sinSeries n x < sin x) (x : ℝ) (hx : 0 < x) :
cos x < cosSeries (n + 1) x := by
suffices StrictAntiOn (cos - cosSeries (n + 1)) (.Ici 0) by
simpa [Hcos₀] using this Set.left_mem_Ici hx.le hx
apply strictAntiOn_of_deriv_neg
· apply convex_Ici
· simp only [cosSeries, Pi.sub_def]
fun_prop
· simpa [(HcosDeriv _ _).deriv] using ih
have Hstep_cos_sin (n : ℕ) (ih : ∀ x > 0, cos x < cosSeries n x) (x : ℝ) (hx : 0 < x) :
sin x < sinSeries n x := by
suffices StrictAntiOn (sin - sinSeries n) (Set.Ici 0) by
simpa [Hsin₀] using this Set.left_mem_Ici hx.le hx
apply strictAntiOn_of_deriv_neg
· apply convex_Ici
· simp only [sinSeries, Pi.sub_def]
exact continuousOn_sin.sub <| continuousOn_finset_sum _ fun _ _ ↦ by fun_prop
· simpa [(HsinDeriv _ _).deriv] using ih
have Hstep_cos_sin' (n : ℕ) (ih : ∀ x > 0, cosSeries n x < cos x) (x : ℝ) (hx : 0 < x) :
sinSeries n x < sin x := by
suffices StrictMonoOn (sin - sinSeries n) (Set.Ici 0) by
simpa [Hsin₀] using this Set.left_mem_Ici hx.le hx
apply strictMonoOn_of_deriv_pos
· apply convex_Ici
· simp only [sinSeries, Pi.sub_def]
exact continuousOn_sin.sub <| continuousOn_finset_sum _ fun _ _ ↦ by fun_prop
· simpa [(HsinDeriv _ _).deriv] using ih
induction n generalizing x with
| zero =>
have Hsin_lt : ∀ x > 0, sin x < sinSeries 1 x := by
intro x hx
simpa [sinSeries] using sin_lt hx
have Hlt_cos : ∀ x > 0, cosSeries 2 x < cos x := Hstep_sin_cos 1 Hsin_lt
have Hlt_sin : ∀ x > 0, sinSeries 2 x < sin x := Hstep_cos_sin' 2 Hlt_cos
have Hcos_lt : ∀ x > 0, cos x < cosSeries 3 x := Hstep_sin_cos' 2 Hlt_sin
exact ⟨Hlt_sin _ hx, Hsin_lt _ hx, Hlt_cos _ hx, Hcos_lt _ hx⟩
| succ n ihn =>
have Hsin_lt : ∀ x > 0, sin x < sinSeries (2 * n + 3) x := Hstep_cos_sin _ fun x hx ↦
(ihn x hx).2.2.2
have Hlt_cos : ∀ x > 0, cosSeries (2 * n + 4) x < cos x := Hstep_sin_cos _ Hsin_lt
have Hlt_sin : ∀ x > 0, sinSeries (2 * n + 4) x < sin x := Hstep_cos_sin' _ Hlt_cos
have Hcos_lt : ∀ x > 0, cos x < cosSeries (2 * n + 5) x := Hstep_sin_cos' _ Hlt_sin
simp only [mul_add_one, add_assoc]
exact ⟨Hlt_sin _ hx, Hsin_lt _ hx, Hlt_cos _ hx, Hcos_lt _ hx⟩
Aaron Liu (Oct 21 2025 at 17:06):
Didn't I open a thread about this
Aaron Liu (Oct 21 2025 at 17:06):
Yury G. Kudryashov (Oct 21 2025 at 17:12):
I think that we should have both versions.
Yury G. Kudryashov (Oct 21 2025 at 17:14):
I left a comment on #29355
Yongxi Lin (Aaron) (Oct 21 2025 at 18:29):
Yury G. Kudryashov said:
You can use this. Could you please open a Mathlib PR with this lemma + individual bounds as corollaries + non-strict inequality versions + versions for negative
x?theorem Real.sin_cos_bound_of_pos (x : ℝ) (hx : 0 < x) (n : ℕ) : (∑ i ∈ .range (2 * n + 2), (-1) ^ i * x ^ (2 * i + 1) / (2 * i + 1)! < x.sin) ∧ (x.sin < ∑ i ∈ .range (2 * n + 1), (-1) ^ i * x ^ (2 * i + 1) / (2 * i + 1)!) ∧ (∑ i ∈ .range (2 * n + 2), (-1) ^ i * x ^ (2 * i) / (2 * i)! < x.cos) ∧ (x.cos < ∑ i ∈ .range (2 * n + 3), (-1) ^ i * x ^ (2 * i) / (2 * i)!) := by have H₀ (x : ℝ) (n : ℕ) (k : ℕ → ℕ) : HasDerivAt (fun x : ℝ ↦ ∑ i ∈ .range n, (-1) ^ i * x ^ (k i) / (k i)!) (∑ i ∈ .range n, (-1) ^ i * k i * x ^ (k i - 1) / (k i)!) x := by refine HasDerivAt.fun_sum fun i hi ↦ ?_ simpa only [mul_assoc] using ((hasDerivAt_pow (k i) x).const_mul _).div_const _ set cosSeries := fun (n : ℕ) (x : ℝ) ↦ ∑ i ∈ .range n, (-1) ^ i * x ^ (2 * i) / (2 * i)! set sinSeries := fun (n : ℕ) (x : ℝ) ↦ ∑ i ∈ .range n, (-1) ^ i * x ^ (2 * i + 1) / (2 * i + 1)! have Hcos₀ (n) : cosSeries (n + 1) 0 = 1 := by simp [cosSeries, Finset.sum_range_succ'] have Hsin₀ (n) : sinSeries n 0 = 0 := by simp [sinSeries] have HsinDeriv (x : ℝ) (n : ℕ) : HasDerivAt (sin - sinSeries n) (cos x - cosSeries n x) x := by convert (hasDerivAt_sin x).sub (H₀ _ _ _) using 1 simp (disch := positivity) [Nat.factorial_succ, field, mul_assoc, mul_left_comm _ (2 * _ + 1 : ℝ), mul_div_mul_left] have HcosDeriv (x : ℝ) (n : ℕ) : HasDerivAt (cos - cosSeries (n + 1)) (-sin x + sinSeries n x) x := by rw [← sub_neg_eq_add (-sin x)] convert (hasDerivAt_cos x).sub (H₀ _ _ _) using 2 rw [Finset.sum_range_succ', ← Finset.sum_neg_distrib, eq_comm] convert add_zero _ using 2 · simp · simp [field, Nat.factorial_succ, mul_add_one] ring have Hstep_sin_cos (n : ℕ) (ih : ∀ x > 0, sin x < sinSeries n x) (x : ℝ) (hx : 0 < x) : cosSeries (n + 1) x < cos x := by suffices StrictMonoOn (cos - cosSeries (n + 1)) (.Ici 0) by simpa [Hcos₀] using this Set.left_mem_Ici hx.le hx apply strictMonoOn_of_deriv_pos · apply convex_Ici · simp only [cosSeries, Pi.sub_def] fun_prop · simpa [(HcosDeriv _ _).deriv] using ih have Hstep_sin_cos' (n : ℕ) (ih : ∀ x > 0, sinSeries n x < sin x) (x : ℝ) (hx : 0 < x) : cos x < cosSeries (n + 1) x := by suffices StrictAntiOn (cos - cosSeries (n + 1)) (.Ici 0) by simpa [Hcos₀] using this Set.left_mem_Ici hx.le hx apply strictAntiOn_of_deriv_neg · apply convex_Ici · simp only [cosSeries, Pi.sub_def] fun_prop · simpa [(HcosDeriv _ _).deriv] using ih have Hstep_cos_sin (n : ℕ) (ih : ∀ x > 0, cos x < cosSeries n x) (x : ℝ) (hx : 0 < x) : sin x < sinSeries n x := by suffices StrictAntiOn (sin - sinSeries n) (Set.Ici 0) by simpa [Hsin₀] using this Set.left_mem_Ici hx.le hx apply strictAntiOn_of_deriv_neg · apply convex_Ici · simp only [sinSeries, Pi.sub_def] exact continuousOn_sin.sub <| continuousOn_finset_sum _ fun _ _ ↦ by fun_prop · simpa [(HsinDeriv _ _).deriv] using ih have Hstep_cos_sin' (n : ℕ) (ih : ∀ x > 0, cosSeries n x < cos x) (x : ℝ) (hx : 0 < x) : sinSeries n x < sin x := by suffices StrictMonoOn (sin - sinSeries n) (Set.Ici 0) by simpa [Hsin₀] using this Set.left_mem_Ici hx.le hx apply strictMonoOn_of_deriv_pos · apply convex_Ici · simp only [sinSeries, Pi.sub_def] exact continuousOn_sin.sub <| continuousOn_finset_sum _ fun _ _ ↦ by fun_prop · simpa [(HsinDeriv _ _).deriv] using ih induction n generalizing x with | zero => have Hsin_lt : ∀ x > 0, sin x < sinSeries 1 x := by intro x hx simpa [sinSeries] using sin_lt hx have Hlt_cos : ∀ x > 0, cosSeries 2 x < cos x := Hstep_sin_cos 1 Hsin_lt have Hlt_sin : ∀ x > 0, sinSeries 2 x < sin x := Hstep_cos_sin' 2 Hlt_cos have Hcos_lt : ∀ x > 0, cos x < cosSeries 3 x := Hstep_sin_cos' 2 Hlt_sin exact ⟨Hlt_sin _ hx, Hsin_lt _ hx, Hlt_cos _ hx, Hcos_lt _ hx⟩ | succ n ihn => have Hsin_lt : ∀ x > 0, sin x < sinSeries (2 * n + 3) x := Hstep_cos_sin _ fun x hx ↦ (ihn x hx).2.2.2 have Hlt_cos : ∀ x > 0, cosSeries (2 * n + 4) x < cos x := Hstep_sin_cos _ Hsin_lt have Hlt_sin : ∀ x > 0, sinSeries (2 * n + 4) x < sin x := Hstep_cos_sin' _ Hlt_cos have Hcos_lt : ∀ x > 0, cos x < cosSeries (2 * n + 5) x := Hstep_sin_cos' _ Hlt_sin simp only [mul_add_one, add_assoc] exact ⟨Hlt_sin _ hx, Hsin_lt _ hx, Hlt_cos _ hx, Hcos_lt _ hx⟩
Thank you very much, and this is indeed very helpful. Should I make a new PR or not?
Yury G. Kudryashov (Oct 21 2025 at 19:41):
Please follow the discussion in #29355
Last updated: Dec 20 2025 at 21:32 UTC