Ensemble Prover

theorem mini_putnam_1962_a4_two_sided_taylor_remainder_p1_c1_v1 : ∀ (f : ℝ → ℝ) (a b : ℝ), Differentiable ℝ f → Differentiable ℝ (deriv f) → (∀ t ∈ Set.Icc a b, |iteratedDeriv 2 f t| ≤ 1) → ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f y - f x - (y - x) * deriv f x| ≤ (y - x) ^ 2 / 2 := by
  intro f a b h1 h2 hb x hx y hy
  by_cases hxy : x ≤ y
  · have ht := mini_putnam_1962_a4_taylor_forward_bound_p1_c2_v1 f a b h1 h2 hb x (y - x) hx.1 (sub_nonneg.mpr hxy) (by linarith [hy.2])
    simpa only [add_sub_cancel] using ht
  · let g : ℝ → ℝ := fun t => f (-t)
    have dg : deriv g = fun t => -deriv f (-t) := by
      funext t
      exact deriv_comp_neg f t
    have hg1 : Differentiable ℝ g := h1.comp differentiable_neg
    have hg2 : Differentiable ℝ (deriv g) := by
      rw [dg]
      exact (h2.comp differentiable_neg).neg
    have ddg (t : ℝ) : deriv (deriv g) t = deriv (deriv f) (-t) := by
      rw [dg]
      simpa using (((h2 (-t)).hasDerivAt.comp t (hasDerivAt_id t).neg).neg).deriv
    have hgb : ∀ t ∈ Set.Icc (-b) (-a), |iteratedDeriv 2 g t| ≤ 1 := by
      intro t ht
      have hf := hb (-t) (show -t ∈ Set.Icc a b from ⟨by linarith [ht.2], by linarith [ht.1]⟩)
      rw [iteratedDeriv_succ, iteratedDeriv_one] at hf ⊢
      rw [ddg]
      exact hf
    have ht := mini_putnam_1962_a4_taylor_forward_bound_p1_c2_v1 g (-b) (-a) hg1 hg2 hgb (-x) (x - y) (by linarith [hx.2]) (by linarith) (by linarith [hy.1])
    rw [show -x + (x - y) = -y by ring, dg] at ht
    simp only [g, neg_neg] at ht
    convert ht using 1 <;> ring_nf

theorem putnam_1962_a4 : ∀ (f : ℝ → ℝ) (a b : ℝ), Differentiable ℝ f ∧ Differentiable ℝ (deriv f) → (∀ x ∈ Set.Icc a b, |f x| ≤ 1) → (∀ x ∈ Set.Icc a b, |iteratedDeriv 2 f x| ≤ 1) → b - a ≥ 2 → ∀ x ∈ Set.Icc a b, |iteratedDeriv 1 f x| ≤ 2 := by
  intro f a b hd hf hf2 hab x hx
  obtain ⟨hax, hxb⟩ := hx
  have hend : ∃ p : ℝ, a ≤ p ∧ p ≤ x ∧ x ≤ p + 2 ∧ p + 2 ≤ b := by
    by_cases h : x ≤ a + 2
    · exact ⟨a, le_rfl, hax, h, by linarith⟩
    · refine ⟨x - 2, ?_, ?_, ?_, ?_⟩ <;> linarith
  obtain ⟨p, hap, hpx, hxq, hqb⟩ := hend
  have hp : p ∈ Set.Icc a b := ⟨hap, by linarith⟩
  have hq : p + 2 ∈ Set.Icc a b := ⟨by linarith, hqb⟩
  have ht := mini_putnam_1962_a4_two_sided_taylor_remainder_p1_c1_v1
    f a b hd.1 hd.2 hf2 x ⟨hax, hxb⟩
  obtain ⟨hrpl, hrpu⟩ := abs_le.mp (ht p hp)
  obtain ⟨hrql, hrqu⟩ := abs_le.mp (ht (p + 2) hq)
  obtain ⟨hfpl, hfpu⟩ := abs_le.mp (hf p hp)
  obtain ⟨hfql, hfqu⟩ := abs_le.mp (hf (p + 2) hq)
  have hsq : (p - x) ^ 2 + (p + 2 - x) ^ 2 ≤ 4 := by
    nlinarith [mul_nonneg (sub_nonneg.mpr hpx) (sub_nonneg.mpr hxq)]
  have hd_bound : |deriv f x| ≤ 2 := by
    apply abs_le.mpr
    constructor <;> nlinarith
  simpa only [iteratedDeriv_one] using hd_bound