2.3 Smoothness and algebraic decay

The decay of Chebyshev coefficients controls truncation error. Finite smoothness gives algebraic rates, with the last derivative allowed to have bounded variation.

2.3.1 From smoothness to coefficient decay

Total variation measures the sum of absolute increments over partitions. The derivative relation below can be iterated when the intermediate functions are absolutely continuous; the final derivative may have jumps.

Theorem 2.3.1 Derivative relation for coefficients

✓ 🤖

Suppose \(f\) is absolutely continuous on \([-1,1]\) with derivative representative \(g\) almost everywhere, and \(\theta \mapsto g(\cos \theta )\) is integrable on \([0,\pi ]\). Then \(f(\cos \theta )\) is absolutely continuous, with derivative \(-g(\cos \theta )\sin \theta \) almost everywhere. For \(n\ge 2\),

\[ a_n(f)=\frac{a_{n-1}(g)-a_{n+1}(g)}{2n}. \]

The exceptional first-degree case is \(a_1(f)=a_0(g)-a_2(g)/2\), with the full constant coefficient convention. The integrability assumption holds in particular when \(g\) has bounded variation.

Reference: the repeated-integration step in [ATAP, Chapter 7].

Lean Formalisation

theorem Polynomial.Chebyshev.absolutelyContinuous_cosine_pullback {f g : ℝ → ℝ} (hf : AbsolutelyContinuousOnInterval f (-1) 1)
  (hd : ∀ᵐ (x : ℝ), x ∈ Set.Icc (-1) 1 → HasDerivAt f (g x) x)
  (hg : IntervalIntegrable (fun θ => g (Real.cos θ)) MeasureTheory.volume 0 Real.pi) :
  AbsolutelyContinuousOnInterval (fun θ => f (Real.cos θ)) 0 Real.pi ∧
    ∀ᵐ (θ : ℝ), θ ∈ Set.Icc 0 Real.pi → HasDerivAt (fun θ => f (Real.cos θ)) (g (Real.cos θ) * -Real.sin θ) θ

Lean proof

/-- The cosine pullback of an absolutely continuous function is absolutely
continuous when the supplied derivative representative has an integrable cosine
pullback. The derivative identity is retained almost everywhere. -/
theorem absolutelyContinuous_cosine_pullback {f g : ℝ → ℝ}
    (hf : AbsolutelyContinuousOnInterval f (-1) 1)
    (hd : ∀ᵐ x ∂volume, x ∈ Icc (-1) 1 → HasDerivAt f (g x) x)
    (hg : IntervalIntegrable (fun θ ↦ g (cos θ)) volume 0 π) :
    AbsolutelyContinuousOnInterval (fun θ ↦ f (cos θ)) 0 π ∧
      ∀ᵐ θ ∂volume, θ ∈ Icc 0 π →
        HasDerivAt (fun θ ↦ f (cos θ)) (g (cos θ) * (-sin θ)) θ := by
  let H : ℝ → ℝ := fun θ ↦ g (cos θ) * (-sin θ)
  have hH : IntervalIntegrable H volume 0 π := hg.mul_continuousOn (by fun_prop)
  let J : ℝ → ℝ := (uIcc 0 π).indicator H
  have hJ : Integrable J := (integrable_indicator_iff measurableSet_uIcc).mpr
    ((intervalIntegrable_iff').mp hH)
  have heq : EqOn (fun θ ↦ f 1 + ∫ t in 0..θ, J t) (fun θ ↦ f (cos θ)) (Icc 0 π) := by
    intro θ hθ
    have he : (∫ t in 0..θ, J t) = ∫ t in 0..θ, H t := by
      apply intervalIntegral.integral_congr
      intro t ht
      have hm : t ∈ uIcc 0 π := by
        rw [uIcc_of_le pi_pos.le]
        rw [uIcc_of_le hθ.1] at ht
        exact ⟨ht.1, ht.2.trans hθ.2⟩
      exact Set.indicator_of_mem hm H
    change f 1 + (∫ t in 0..θ, J t) = f (cos θ)
    rw [he]
    exact (cosine_pullback_eq_integral hf hd hθ).symm
  have hac := hJ.intervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral
    (a := 0) (b := π) (c := 0) (by simp)
  have hc : AbsolutelyContinuousOnInterval (fun _ : ℝ ↦ f 1) 0 π :=
    (show ContDiff ℝ 1 (fun _ : ℝ ↦ f 1) by fun_prop).contDiffOn.absolutelyContinuousOnInterval
  constructor
  · exact (hc.fun_add hac).congr (by simpa only [uIcc_of_le pi_pos.le] using heq)
  · filter_upwards [(hJ.intervalIntegrable (a := 0) (b := π)).ae_hasDerivAt_integral,
      (countable_singleton (0 : ℝ)).ae_notMem volume,
      (countable_singleton π).ae_notMem volume] with θ hθ hzero hpi hmem
    have hθ' : θ ∈ Ioo 0 π := by simpa using (show 0 < θ ∧ θ < π by grind)
    have hder := (hθ (by simpa only [uIcc_of_le pi_pos.le] using hmem) 0 (by simp)).const_add (f 1)
    have hm : θ ∈ uIcc 0 π := by simpa only [uIcc_of_le pi_pos.le] using hmem
    simp only [J, Set.indicator_of_mem hm] at hder
    apply hder.congr_of_eventuallyEq
    filter_upwards [Ioo_mem_nhds hθ'.1 hθ'.2] with t ht
    exact (heq (Ioo_subset_Icc_self ht)).symm

2.3 Smoothness and algebraic decay

2.3.1 From smoothness to coefficient decay

2.3.2 From coefficient decay to approximation error