Proving sin parabola inequalities

sin_parabola_inequalities.lean

/-
This file was generated by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid: 9e58125b-45de-4dcb-aa58-ff8cd2349248
-/

/-
I have proven the two inequalities relating the sine function and parabolas on the interval [0, π/2].

The first inequality, `parabola_le_sin_lower`, states that `(1 / π) * x * (π - x) ≤ sin x` for `x ∈ [0, π/2]`. This was proven using the Taylor series lower bound `sin x ≥ x - x^3/6`.

The second inequality, `sin_le_parabola_left`, states that `sin x ≤ (4 / π^2) * x * (π - x)` for `x ∈ [0, π/2]`. This required a more involved analysis of the difference function `f(x) = (4 / π^2) * x * (π - x) - sin x`. I showed that `f(x) ≥ 0` by analyzing its first and second derivatives, establishing that `f` increases then decreases, with `f(0) = f(π/2) = 0`.
-/

import Mathlib

set_option linter.mathlibStandardSet false

open scoped BigOperators
open scoped Real
open scoped Nat
open scoped Classical
open scoped Pointwise

set_option maxHeartbeats 0
set_option maxRecDepth 4000
set_option synthInstance.maxHeartbeats 20000
set_option synthInstance.maxSize 128

set_option relaxedAutoImplicit false
set_option autoImplicit false

noncomputable section

/-
For x in [0, pi/2], the parabola x(pi-x)/pi is less than or equal to sin(x).
-/
theorem parabola_le_sin_lower (x : ℝ) (hx : x ∈ Set.Icc 0 Real.pi) (h2 : x ≤ Real.pi / 2) :
  (1 / Real.pi) * x * (Real.pi - x) ≤ Real.sin x := by
    -- Since $x \leq \frac{\pi}{2}$, we have $\sin x \geq x - \frac{x^3}{6}$.
    have h_sin_bound : Real.sin x ≥ x - x^3 / 6 := by
      -- We'll use the fact that $Real.sin x \geq x - \frac{x^3}{6}$ for $x \in [0, \frac{\pi}{2}]$. This follows from the Taylor series expansion of $\sin x$.
      have h_sin_bound : ∀ x ∈ Set.Icc 0 (Real.pi / 2), Real.sin x ≥ x - x^3 / 6 := by
        -- Let's choose any $x$ in the interval $[0, \frac{\pi}{2}]$ and derive the inequality.
        intro x hx
        have h_sin_deriv : ∀ t ∈ Set.Icc 0 x, Real.cos t ≥ 1 - t^2 / 2 := by
          exact?;
        -- Integrate both sides of $\cos t \geq 1 - t^2 / 2$ from $0$ to $x$.
        have h_integral : ∫ t in (0 : ℝ)..x, Real.cos t ≥ ∫ t in (0 : ℝ)..x, (1 - t^2 / 2) := by
          refine' intervalIntegral.integral_mono_on _ _ _ _ <;> aesop;
        norm_num at *; linarith;
      exact h_sin_bound x ⟨ hx.1, h2 ⟩;
    -- We'll use the fact that $\pi \approx 3.14$ to simplify the inequality.
    have h_pi_approx : Real.pi < 3.15 := by
      exact?;
    norm_num at *; nlinarith [ Real.pi_gt_three, mul_le_mul_of_nonneg_left h2 hx.1, pow_nonneg hx.1 2, pow_nonneg hx.1 3, mul_inv_cancel₀ Real.pi_ne_zero ] ;

/-
The second derivative of the difference function is -8/pi^2 + sin(x).
-/
def parabola_sin_diff (x : ℝ) : ℝ := (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x

lemma parabola_sin_diff_deriv_deriv (x : ℝ) :
  deriv (deriv parabola_sin_diff) x = -(8 / Real.pi ^ 2) + Real.sin x := by
    unfold parabola_sin_diff;
    unfold deriv;
    norm_num [ Real.differentiableAt_sin, sub_mul, mul_assoc, mul_comm, mul_left_comm, fderiv_deriv ] ; ring

/-
The second derivative of the difference function is strictly increasing on [0, pi/2].
-/
lemma parabola_sin_diff_deriv_deriv_mono :
  StrictMonoOn (deriv (deriv parabola_sin_diff)) (Set.Icc 0 (Real.pi / 2)) := by
    -- Since the second derivative of f(x) is -8/π² + sin(x), and sin(x) is strictly increasing on [0, π/2], the second derivative must also be strictly increasing on this interval.
    have h_sin_inc : StrictMonoOn Real.sin (Set.Icc 0 (Real.pi / 2)) := by
      exact Real.strictMonoOn_sin.mono ( Set.Icc_subset_Icc_left ( by linarith [ Real.pi_pos ] ) );
    have h_deriv2 : ∀ x, deriv (deriv parabola_sin_diff) x = -8 / Real.pi ^ 2 + Real.sin x := by
      apply_rules [ parabola_sin_diff_deriv_deriv ];
      unfold parabola_sin_diff; norm_num [ Real.differentiableAt_sin, mul_comm ] ; ext; ring;
      unfold deriv ; norm_num [ fderiv_deriv, Real.differentiableAt_sin, mul_assoc, mul_comm ] ; ring;
    exact fun x hx y hy hxy => by simpa only [ h_deriv2 ] using add_lt_add_left ( h_sin_inc hx hy hxy ) _;

/-
The second derivative of the difference function at 0 is negative.
-/
lemma parabola_sin_diff_deriv_deriv_zero_lt_zero : deriv (deriv parabola_sin_diff) 0 < 0 := by
  rw [ show deriv parabola_sin_diff = fun x => deriv ( fun x => ( 4 : ℝ ) / Real.pi ^ 2 * x * ( Real.pi - x ) - Real.sin x ) x from funext fun x => rfl ] ; norm_num [ Real.differentiableAt_sin, Real.differentiableAt_cos, mul_assoc, mul_comm, mul_left_comm, sub_mul ] ; ring_nf;
  positivity

/-
The second derivative of the difference function at pi/2 is positive.
-/
lemma parabola_sin_diff_deriv_deriv_pi_div_two_gt_zero : deriv (deriv parabola_sin_diff) (Real.pi / 2) > 0 := by
  -- By definition of $parabola_sin_diff$, we know that its second derivative is $-(8 / Real.pi ^ 2) + Real.sin x$.
  simp [parabola_sin_diff_deriv_deriv];
  rw [ div_lt_iff₀ ] <;> nlinarith [ Real.pi_gt_three ]

/-
The first derivative of the difference function at 0 is positive.
-/
lemma parabola_sin_diff_deriv_zero_gt_zero : deriv parabola_sin_diff 0 > 0 := by
  unfold parabola_sin_diff;
  norm_num [ sub_mul, mul_assoc, mul_comm, mul_left_comm, Real.differentiableAt_sin, Real.pi_ne_zero ];
  rw [ mul_div, lt_div_iff₀ ] <;> nlinarith [ Real.pi_gt_three, show Real.pi < 4 by pi_upper_bound [ ] ]

/-
The first derivative of the difference function at pi/2 is 0.
-/
lemma parabola_sin_diff_deriv_pi_div_two_eq_zero : deriv parabola_sin_diff (Real.pi / 2) = 0 := by
  rw [ show parabola_sin_diff = fun x => ( 4 / Real.pi ^ 2 ) * x * ( Real.pi - x ) - Real.sin x from funext fun x => rfl ] ; norm_num [ Real.differentiableAt_sin, Real.differentiableAt_cos, mul_assoc, mul_comm, mul_left_comm, Real.pi_ne_zero, sub_mul ];
  ring

/-
There is a unique point c in (0, pi/2) where the second derivative is zero.
-/
lemma exists_unique_parabola_sin_diff_deriv_deriv_eq_zero :
  ∃! c, c ∈ Set.Ioo 0 (Real.pi / 2) ∧ deriv (deriv parabola_sin_diff) c = 0 := by
    -- By the properties of the intermediate value theorem and the strict monotonicity of the second derivative, there must be a unique $c$ in $(0, \frac{\pi}{2})$ such that $deriv (deriv parabola_sin_diff) c = 0$.
    obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo 0 (Real.pi / 2), deriv (deriv parabola_sin_diff) c = 0 := by
      -- By the Intermediate Value Theorem, since the second derivative is continuous and changes sign between 0 and π/2, there exists a c in (0, π/2) where the second derivative is zero.
      have h_ivt : ContinuousOn (deriv (deriv parabola_sin_diff)) (Set.Icc 0 (Real.pi / 2)) := by
        exact Continuous.continuousOn ( by rw [ show deriv ( deriv parabola_sin_diff ) = _ from by funext x; exact parabola_sin_diff_deriv_deriv x ] ; continuity );
      apply_rules [ intermediate_value_Ioo ];
      · positivity;
      · exact ⟨ by exact? , by exact? ⟩;
    exact ⟨ c, hc, fun x hx => StrictMonoOn.injOn ( show StrictMonoOn ( deriv ( deriv parabola_sin_diff ) ) ( Set.Icc 0 ( Real.pi / 2 ) ) from by simpa only [ Set.Ioo_subset_Icc_self ] using parabola_sin_diff_deriv_deriv_mono ) ⟨ hx.1.1.le, hx.1.2.le ⟩ ⟨ hc.1.1.le, hc.1.2.le ⟩ <| by aesop ⟩

/-
c is the unique point in (0, pi/2) where the second derivative is zero.
-/
noncomputable def parabola_sin_diff_c : ℝ := Classical.choose exists_unique_parabola_sin_diff_deriv_deriv_eq_zero

lemma parabola_sin_diff_c_spec :
  parabola_sin_diff_c ∈ Set.Ioo 0 (Real.pi / 2) ∧ deriv (deriv parabola_sin_diff) parabola_sin_diff_c = 0 := by
    exact Classical.choose_spec exists_unique_parabola_sin_diff_deriv_deriv_eq_zero |>.1

/-
The second derivative is negative before c.
-/
lemma parabola_sin_diff_deriv_deriv_neg_of_lt_c (x : ℝ) (hx : x ∈ Set.Ico 0 parabola_sin_diff_c) :
  deriv (deriv parabola_sin_diff) x < 0 := by
    have := Classical.choose_spec ( exists_unique_parabola_sin_diff_deriv_deriv_eq_zero ) |>.1;
    have h_deriv_neg : StrictMonoOn (deriv (deriv parabola_sin_diff)) (Set.Icc 0 (Real.pi / 2)) := by
      exact?;
    have := h_deriv_neg ( show x ∈ Set.Icc 0 ( Real.pi / 2 ) from ⟨ hx.1, hx.2.le.trans this.1.2.le ⟩ ) ( show Classical.choose exists_unique_parabola_sin_diff_deriv_deriv_eq_zero ∈ Set.Icc 0 ( Real.pi / 2 ) from ⟨ this.1.1.le, this.1.2.le ⟩ ) hx.2; aesop;

/-
The second derivative is positive after c.
-/
lemma parabola_sin_diff_deriv_deriv_pos_of_gt_c (x : ℝ) (hx : x ∈ Set.Ioc parabola_sin_diff_c (Real.pi / 2)) :
  deriv (deriv parabola_sin_diff) x > 0 := by
    have := exists_unique_parabola_sin_diff_deriv_deriv_eq_zero.choose_spec.2;
    contrapose! this;
    -- Since $x \in (c, \pi/2]$ and the second derivative is strictly increasing, we have $deriv (deriv parabola_sin_diff) x > deriv (deriv parabola_sin_diff) c$.
    have h_inc : deriv (deriv parabola_sin_diff) x > deriv (deriv parabola_sin_diff) parabola_sin_diff_c := by
      have h_inc : StrictMonoOn (deriv (deriv parabola_sin_diff)) (Set.Icc 0 (Real.pi / 2)) := by
        exact?;
      exact h_inc ⟨ by linarith [ hx.1, parabola_sin_diff_c_spec.1.1 ], by linarith [ hx.2, parabola_sin_diff_c_spec.1.2 ] ⟩ ⟨ by linarith [ hx.1, parabola_sin_diff_c_spec.1.1 ], by linarith [ hx.2, parabola_sin_diff_c_spec.1.2 ] ⟩ hx.1;
    exact False.elim <| h_inc.not_le <| by linarith [ show deriv ( deriv parabola_sin_diff ) parabola_sin_diff_c = 0 from Classical.choose_spec exists_unique_parabola_sin_diff_deriv_deriv_eq_zero |>.1.2 ] ;

/-
The first derivative is non-positive on [c, pi/2].
-/
lemma parabola_sin_diff_deriv_neg_of_ge_c (x : ℝ) (hx : x ∈ Set.Icc parabola_sin_diff_c (Real.pi / 2)) :
  deriv parabola_sin_diff x ≤ 0 := by
    -- Since the first derivative is strictly decreasing on [c, pi/2], and it is positive at x, it must be positive at all points in [x, pi/2].
    have h_deriv_pos : ∀ y ∈ Set.Icc x (Real.pi / 2), deriv parabola_sin_diff y ≥ deriv parabola_sin_diff x := by
      intros y hy
      have h_deriv_pos : ∀ z ∈ Set.Icc x y, deriv (deriv parabola_sin_diff) z ≥ 0 := by
        intros z hz
        have h_deriv_pos : z ≥ parabola_sin_diff_c := by
          linarith [ hx.1, hz.1 ];
        exact le_of_not_gt fun h => by linarith [ parabola_sin_diff_deriv_deriv_pos_of_gt_c z ⟨ h_deriv_pos.lt_of_ne <| by rintro rfl; linarith [ parabola_sin_diff_c_spec.2 ], by linarith [ Real.pi_pos, hy.2, hz.2 ] ⟩ ] ;
      by_cases hxy : x < y;
      · have := exists_deriv_eq_slope ( deriv parabola_sin_diff ) hxy;
        -- Apply the Mean Value Theorem to the interval [x, y].
        obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo x y, deriv (deriv parabola_sin_diff) c = (deriv parabola_sin_diff y - deriv parabola_sin_diff x) / (y - x) := by
          apply this;
          · exact Continuous.continuousOn ( by rw [ show deriv parabola_sin_diff = fun x => deriv ( fun x => ( 4 / Real.pi ^ 2 ) * x * ( Real.pi - x ) - Real.sin x ) x from rfl ] ; norm_num [ mul_assoc, mul_comm, mul_left_comm, Real.differentiableAt_sin, Real.differentiableAt_cos, sub_mul ] ; continuity );
          · exact fun z hz => DifferentiableAt.differentiableWithinAt ( by rw [ show deriv parabola_sin_diff = fun z => deriv ( fun z => ( 4 / Real.pi ^ 2 ) * z * ( Real.pi - z ) - Real.sin z ) z from rfl ] ; norm_num [ Real.differentiableAt_sin, mul_assoc, mul_comm, mul_left_comm, sub_mul ] );
        have := h_deriv_pos c ⟨ by linarith [ hc.1.1 ], by linarith [ hc.1.2 ] ⟩ ; rw [ hc.2, ge_iff_le ] at this; rw [ le_div_iff₀ ] at this <;> linarith;
      · rw [ show y = x by linarith [ hy.1, hy.2 ] ];
    -- Since the first derivative is strictly decreasing on [c, pi/2], and it is positive at x, it must be positive at all points in [x, pi/2], contradicting the fact that it is zero at pi/2.
    have h_contradiction : deriv parabola_sin_diff (Real.pi / 2) ≥ deriv parabola_sin_diff x := by
      exact h_deriv_pos _ ⟨ hx.2, le_rfl ⟩;
    linarith [ show deriv parabola_sin_diff ( Real.pi / 2 ) = 0 by exact? ]

/-
The first derivative at c is negative.
-/
lemma parabola_sin_diff_deriv_c_neg : deriv parabola_sin_diff parabola_sin_diff_c < 0 := by
  have h_deriv_c : ∫ x in (parabola_sin_diff_c)..Real.pi / 2, deriv (deriv parabola_sin_diff) x = deriv parabola_sin_diff (Real.pi / 2) - deriv parabola_sin_diff (parabola_sin_diff_c) := by
    rw [ intervalIntegral.integral_deriv_eq_sub' ] <;> norm_num;
    · unfold parabola_sin_diff; norm_num [ Real.differentiableAt_sin, Real.differentiableAt_cos, mul_comm ] ;
      unfold deriv ; norm_num [ fderiv_deriv, Real.differentiableAt_sin, Real.differentiableAt_cos, sub_mul ];
    · exact Continuous.continuousOn ( by rw [ show deriv ( deriv parabola_sin_diff ) = _ from funext fun x => parabola_sin_diff_deriv_deriv x ] ; continuity );
  have h_integral_pos : ∫ x in (parabola_sin_diff_c)..Real.pi / 2, deriv (deriv parabola_sin_diff) x > 0 := by
    have h_integral_pos : ∀ x ∈ Set.Ioo parabola_sin_diff_c (Real.pi / 2), deriv (deriv parabola_sin_diff) x > 0 := by
      exact fun x hx => parabola_sin_diff_deriv_deriv_pos_of_gt_c x <| Set.Ioo_subset_Ioc_self hx;
    field_simp;
    rw [ intervalIntegral.integral_of_le ];
    · rw [ MeasureTheory.integral_Ioc_eq_integral_Ioo, MeasureTheory.integral_pos_iff_support_of_nonneg_ae ];
      · simp +zetaDelta at *;
        exact lt_of_lt_of_le ( by exact ( show 0 < ( MeasureTheory.MeasureSpace.volume : Set ℝ → ENNReal ) ( Set.Ioo parabola_sin_diff_c ( Real.pi / 2 ) ) from by rw [ Real.volume_Ioo ] ; exact ENNReal.ofReal_pos.mpr ( by linarith [ Real.pi_pos, show parabola_sin_diff_c < Real.pi / 2 from by exact Classical.choose_spec exists_unique_parabola_sin_diff_deriv_deriv_eq_zero |>.1 |>.1.2 ] ) ) ) ( MeasureTheory.measure_mono <| show Set.Ioo parabola_sin_diff_c ( Real.pi / 2 ) ⊆ Function.support ( deriv ( deriv parabola_sin_diff ) ) ∩ Set.Ioo parabola_sin_diff_c ( Real.pi / 2 ) from fun x hx => ⟨ ne_of_gt <| h_integral_pos x hx.1 hx.2, hx ⟩ );
      · filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Ioo ] with x hx using le_of_lt ( h_integral_pos x hx );
      · exact ( Continuous.integrableOn_Icc ( by rw [ show deriv ( deriv parabola_sin_diff ) = fun x => - ( 8 / Real.pi ^ 2 ) + Real.sin x from funext fun x => parabola_sin_diff_deriv_deriv x ] ; continuity ) ) |> fun h => h.mono_set <| Set.Ioo_subset_Icc_self;
    · exact le_of_lt ( Classical.choose_spec exists_unique_parabola_sin_diff_deriv_deriv_eq_zero |>.1.1.2 );
  linarith! [ show deriv parabola_sin_diff ( Real.pi / 2 ) = 0 from by simpa using parabola_sin_diff_deriv_pi_div_two_eq_zero ]

/-
There is a unique point d in (0, c) where the first derivative is zero.
-/
lemma exists_unique_parabola_sin_diff_deriv_eq_zero_of_lt_c :
  ∃! d, d ∈ Set.Ioo 0 parabola_sin_diff_c ∧ deriv parabola_sin_diff d = 0 := by
    -- Since the first derivative is strictly decreasing on (0, c), there can be at most one point where it is zero.
    have h_unique : ∀ x y : ℝ, 0 < x → x < y → y < parabola_sin_diff_c → deriv parabola_sin_diff x > deriv parabola_sin_diff y := by
      intros x y hx hy hxy;
      have h_mean_val : ∃ c ∈ Set.Ioo x y, deriv (deriv parabola_sin_diff) c = (deriv parabola_sin_diff y - deriv parabola_sin_diff x) / (y - x) := by
        apply_rules [ exists_deriv_eq_slope ];
        · exact Continuous.continuousOn ( by rw [ show deriv parabola_sin_diff = fun x => deriv ( fun x => ( 4 / Real.pi ^ 2 ) * x * ( Real.pi - x ) - Real.sin x ) x from rfl ] ; norm_num [ mul_assoc, mul_comm, mul_left_comm, Real.differentiableAt_sin, Real.differentiableAt_cos, sub_mul ] ; continuity );
        · exact fun u hu => DifferentiableAt.differentiableWithinAt ( by rw [ show deriv parabola_sin_diff = fun u => deriv ( fun u => ( 4 / Real.pi ^ 2 ) * u * ( Real.pi - u ) - Real.sin u ) u from funext fun u => rfl ] ; norm_num [ Real.differentiableAt_sin, mul_assoc, mul_comm, mul_left_comm, sub_mul ] );
      obtain ⟨ c, ⟨ hxc, hcy ⟩, hcd ⟩ := h_mean_val; have := parabola_sin_diff_deriv_deriv_neg_of_lt_c c ⟨ by linarith, by linarith ⟩ ; rw [ hcd, div_lt_iff₀ ] at this <;> linarith;
    -- By the Intermediate Value Theorem, since the first derivative is continuous on (0, c) and changes sign from positive to negative, there must be a point d in (0, c) where the derivative is zero.
    obtain ⟨d, hd⟩ : ∃ d ∈ Set.Ioo 0 parabola_sin_diff_c, deriv parabola_sin_diff d = 0 := by
      apply_rules [ intermediate_value_Ioo', Continuous.continuousOn ];
      · exact le_of_lt ( Classical.choose_spec exists_unique_parabola_sin_diff_deriv_deriv_eq_zero |>.1.1.1 );
      · unfold parabola_sin_diff;
        fun_prop;
      · exact ⟨ by linarith [ parabola_sin_diff_deriv_c_neg ], by linarith [ parabola_sin_diff_deriv_zero_gt_zero ] ⟩;
    exact ⟨ d, hd, fun x hx => le_antisymm ( le_of_not_gt fun hx' => by linarith [ hx.2, hd.2, h_unique _ _ hd.1.1 hx' ( by linarith [ hx.1.2, hd.1.2 ] ) ] ) ( le_of_not_gt fun hx' => by linarith [ hx.2, hd.2, h_unique _ _ hx.1.1 hx' ( by linarith [ hx.1.2, hd.1.2 ] ) ] ) ⟩

/-
d is the unique point in (0, c) where the first derivative is zero.
-/
noncomputable def parabola_sin_diff_d : ℝ := Classical.choose exists_unique_parabola_sin_diff_deriv_eq_zero_of_lt_c

lemma parabola_sin_diff_d_spec :
  parabola_sin_diff_d ∈ Set.Ioo 0 parabola_sin_diff_c ∧ deriv parabola_sin_diff parabola_sin_diff_d = 0 := by
  exact Classical.choose_spec exists_unique_parabola_sin_diff_deriv_eq_zero_of_lt_c |>.1

/-
The first derivative is positive before d.
-/
lemma parabola_sin_diff_deriv_pos_of_lt_d (x : ℝ) (hx : x ∈ Set.Ico 0 parabola_sin_diff_d) :
  deriv parabola_sin_diff x > 0 := by
    -- Apply the Mean Value Theorem to the interval [x, d] to find a point c where the derivative equals the average rate of change.
    obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo x parabola_sin_diff_d, deriv (deriv parabola_sin_diff) c = (deriv parabola_sin_diff parabola_sin_diff_d - deriv parabola_sin_diff x) / (parabola_sin_diff_d - x) := by
      apply_rules [ exists_deriv_eq_slope ] ; aesop;
      · exact Continuous.continuousOn ( by rw [ show deriv parabola_sin_diff = fun x => deriv ( fun x => ( 4 / Real.pi ^ 2 ) * x * ( Real.pi - x ) - Real.sin x ) x from rfl ] ; norm_num [ Real.differentiableAt_sin, mul_assoc, mul_comm, mul_left_comm, sub_mul ] ; continuity );
      · exact fun y hy => DifferentiableAt.differentiableWithinAt ( by rw [ show deriv parabola_sin_diff = fun x => deriv ( fun x => ( 4 / Real.pi ^ 2 ) * x * ( Real.pi - x ) - Real.sin x ) x from rfl ] ; norm_num [ Real.differentiableAt_sin, mul_assoc, mul_comm, mul_left_comm, sub_mul ] );
    -- Since $c \in (x, d)$ and $d \in (0, c)$, we have $deriv (deriv parabola_sin_diff) c < 0$.
    have h_second_deriv_neg : deriv (deriv parabola_sin_diff) c < 0 := by
      exact parabola_sin_diff_deriv_deriv_neg_of_lt_c c ⟨ by linarith [ hx.1, hc.1.1 ], by linarith [ hx.2, hc.1.2, parabola_sin_diff_d_spec.1.2 ] ⟩;
    rw [ eq_div_iff ] at hc <;> nlinarith [ hx.2, hc.1.1, hc.1.2, parabola_sin_diff_d_spec.2 ]

/-
The first derivative is negative for x in (d, c].
-/
lemma parabola_sin_diff_deriv_neg_of_gt_d_le_c (x : ℝ) (hx : x ∈ Set.Ioc parabola_sin_diff_d parabola_sin_diff_c) :
  deriv parabola_sin_diff x < 0 := by
    -- By definition of $parabola\_sin\_diff\_d$, we know that $deriv parabola\_sin\_diff x$ is negative for $x \in (parabola\_sin\_diff\_d, parabola\_sin\_diff\_c)$ because the derivative of the derivative is negative.
    have h_deriv_deriv_neg : ∀ x ∈ Set.Ioo parabola_sin_diff_d parabola_sin_diff_c, deriv (deriv parabola_sin_diff) x < 0 := by
      exact fun x hx => parabola_sin_diff_deriv_deriv_neg_of_lt_c x ⟨ hx.1.le.trans' ( le_of_lt ( parabola_sin_diff_d_spec.1.1 ) ), hx.2 ⟩;
    -- Apply the mean value theorem to the interval $[d, x]$.
    obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo parabola_sin_diff_d x, deriv (deriv parabola_sin_diff) c = (deriv parabola_sin_diff x - deriv parabola_sin_diff parabola_sin_diff_d) / (x - parabola_sin_diff_d) := by
      apply_rules [ exists_deriv_eq_slope ] ; aesop;
      · refine' Continuous.continuousOn _;
        rw [ show deriv parabola_sin_diff = fun x => deriv ( fun x => ( 4 / Real.pi ^ 2 ) * x * ( Real.pi - x ) - Real.sin x ) x from funext fun x => rfl ] ; norm_num [ mul_assoc, mul_comm, mul_left_comm, Real.differentiableAt_sin, Real.differentiableAt_cos, sub_mul ] ; continuity;
      · exact fun y hy => DifferentiableAt.differentiableWithinAt ( by exact differentiableAt_of_deriv_ne_zero ( ne_of_lt ( h_deriv_deriv_neg y ⟨ hy.1, hy.2.trans_le hx.2 ⟩ ) ) );
    have := h_deriv_deriv_neg c ⟨ hc.1.1, hc.1.2.trans_le hx.2 ⟩ ; rw [ hc.2, div_lt_iff₀ ] at this <;> linarith [ hx.1, hx.2, parabola_sin_diff_d_spec.2 ] ;

/-
The first derivative is non-positive for x >= d.
-/
lemma parabola_sin_diff_deriv_neg_of_ge_d (x : ℝ) (hx : x ∈ Set.Icc parabola_sin_diff_d (Real.pi / 2)) :
  deriv parabola_sin_diff x ≤ 0 := by
    by_cases h_cases : x ≤ parabola_sin_diff_c;
    · by_cases h_cases : x = parabola_sin_diff_d;
      · have := parabola_sin_diff_d_spec.2; aesop;
      · exact le_of_lt ( parabola_sin_diff_deriv_neg_of_gt_d_le_c x ⟨ lt_of_le_of_ne hx.1 ( Ne.symm h_cases ), by linarith [ hx.2 ] ⟩ );
    · -- Since $x > c$, we can apply the lemma parabola_sin_diff_deriv_neg_of_ge_c.
      apply parabola_sin_diff_deriv_neg_of_ge_c; exact ⟨by linarith [hx.1, parabola_sin_diff_d_spec.1.1], by linarith [hx.2, parabola_sin_diff_c_spec.1.2]⟩

/-
For x in [0, pi/2], sin(x) is less than or equal to the parabola 4/pi^2 * x * (pi - x).
-/
theorem sin_le_parabola_left (x : ℝ) (hx : x ∈ Set.Icc 0 Real.pi) (h2 : x ≤ Real.pi / 2) :
  Real.sin x ≤ (4 / Real.pi ^ 2) * x * (Real.pi - x) := by
    -- Since the derivative of the difference function is negative on [d, pi/2], the difference function is decreasing on this interval.
    have h_decreasing : ∀ x ∈ Set.Icc (parabola_sin_diff_d) (Real.pi / 2), deriv (fun x => (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x) x ≤ 0 := by
      apply_rules [ parabola_sin_diff_deriv_neg_of_ge_d ];
    -- Since the difference function is decreasing on [d, pi/2], we have g(x) ≥ g(pi/2) for x in [d, pi/2].
    have h_g_ge_g_pi_div_two : ∀ x ∈ Set.Icc (parabola_sin_diff_d) (Real.pi / 2), (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x ≥ (4 / Real.pi ^ 2) * (Real.pi / 2) * (Real.pi - Real.pi / 2) - Real.sin (Real.pi / 2) := by
      intro x hx
      by_contra h_contra
      have h_exists_x : ∃ c ∈ Set.Ioo x (Real.pi / 2), deriv (fun x => (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x) c = ( (4 / Real.pi ^ 2) * (Real.pi / 2) * (Real.pi - Real.pi / 2) - Real.sin (Real.pi / 2) - ( (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x ) ) / (Real.pi / 2 - x) := by
        apply_rules [ exists_deriv_eq_slope ];
        · exact hx.2.lt_of_ne ( by rintro rfl; norm_num at h_contra );
        · fun_prop;
        · exact Differentiable.differentiableOn ( by norm_num [ Real.differentiable_sin, mul_assoc, mul_comm, mul_left_comm, sub_mul ] );
      obtain ⟨ c, hc₁, hc₂ ⟩ := h_exists_x; have := h_decreasing c ⟨ by linarith [ hc₁.1, hx.1 ], by linarith [ hc₁.2, hx.2 ] ⟩ ; rw [ hc₂, div_le_iff₀ ] at this <;> nlinarith [ hc₁.1, hc₁.2 ] ;
    -- Since the difference function is increasing on [0, d], we have g(x) ≥ g(0) for x in [0, d].
    have h_g_ge_g_zero : ∀ x ∈ Set.Icc 0 (parabola_sin_diff_d), (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x ≥ (4 / Real.pi ^ 2) * 0 * (Real.pi - 0) - Real.sin 0 := by
      intros x hx
      by_contra h_contra;
      -- Apply the mean value theorem to the interval [0, x].
      obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo 0 x, deriv (fun x => (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x) c = ( (4 / Real.pi ^ 2) * x * (Real.pi - x) - Real.sin x - ( (4 / Real.pi ^ 2) * 0 * (Real.pi - 0) - Real.sin 0 ) ) / (x - 0) := by
        apply_rules [ exists_deriv_eq_slope ];
        · exact hx.1.lt_of_ne ( by rintro rfl; norm_num at h_contra );
        · fun_prop;
        · exact Differentiable.differentiableOn ( by norm_num [ mul_assoc, mul_sub, Real.differentiable_sin ] );
      rw [ eq_div_iff ] at hc <;> nlinarith [ hc.1.1, hc.1.2, hx.1, hx.2, show deriv ( fun x => 4 / Real.pi ^ 2 * x * ( Real.pi - x ) - Real.sin x ) c > 0 from by simpa using parabola_sin_diff_deriv_pos_of_lt_d c ⟨ by linarith [ hc.1.1, hx.1 ], by linarith [ hc.1.2, hx.2, parabola_sin_diff_d_spec.1.2 ] ⟩ ];
    simp +zetaDelta at *;
    exact if h : x ≤ parabola_sin_diff_d then h_g_ge_g_zero x hx.1 h else by linarith [ h_g_ge_g_pi_div_two x ( le_of_not_ge h ) h2, show ( 4 / Real.pi ^ 2 ) * ( Real.pi / 2 ) * ( Real.pi - Real.pi / 2 ) ≥ 1 by ring_nf; nlinarith [ Real.pi_gt_three, mul_inv_cancel₀ Real.pi_ne_zero ] ] ;