Stat.Nonparametric.Approximation

theorem holder_taylor_remainder {f : ℝ → ℝ} {M β lo hi t a : ℝ} (hβ : 0 < β) (hM : 0 ≤ M) (ht : t ∈ Icc lo hi) (ha : a ∈ Icc lo hi) (hf : ContDiff ℝ ((holderDerivOrder β)) f) (hb : ∀ x ∈ Icc lo hi, ∀ y ∈ Icc lo hi, |iteratedDeriv (holderDerivOrder β) f x - iteratedDeriv (holderDerivOrder β) f y| ≤ M * |x - y| ^ (β - ((holderDerivOrder β) : ℝ))) : |f a - taylorPoly (holderDerivOrder β) f t a| ≤ M / ((holderDerivOrder β)).factorial * |a - t| ^ β := by have hRHS : 0 ≤ M / (((holderDerivOrder β)).factorial : ℝ) * |a - t| ^ β := mul_nonneg (div_nonneg hM (by positivity)) (Real.rpow_nonneg (abs_nonneg _) _) rcases eq_or_ne a t with rfl | hne · -- a = t : both sides reduce, LHS = 0 rw [taylorPoly_eval_base, sub_self, abs_zero]; exact hRHS rcases Nat.eq_zero_or_pos (holderDerivOrder β) with hp0 | hppos · -- p = 0 : the bound is exactly the order-β Hölder condition on f itself have htp : taylorPoly (holderDerivOrder β) f t a = f t := by rw [hp0]; simp [taylorPoly, iteratedDeriv_zero] rw [htp] have hbb := hb a ha t ht rw [hp0] at hbb simp only [iteratedDeriv_zero, cast_zero, sub_zero] at hbb rw [hp0] simp only [Nat.factorial_zero, cast_one, div_one] exact hbb · -- p ≥ 1 : Lagrange remainder at order p−1 + Hölder bound on f⁽ᵖ⁾. set p : ℕ := (holderDerivOrder β) with hp have hp_pos : 0 < p := by simpa [hp] using hppos have hp_le_beta : (p : ℝ) ≤ β := by simpa [hp] using (holderDerivOrder_lt hβ).le have hexp_nonneg : 0 ≤ β - (p : ℝ) := sub_nonneg.mpr hp_le_beta have habs_pos : 0 < |a - t| := abs_pos.mpr (sub_ne_zero.mpr hne) rcases lt_or_gt_of_ne hne.symm with hlt | hgt · -- t < a set n : ℕ := p - 1 with hn have hn_succ : n + 1 = p := by simpa [hn] using Nat.succ_pred_eq_of_pos hp_pos have hcont : ContDiffOn ℝ (n + 1) f (uIcc t a) := by change ContDiffOn ℝ (((n + 1 : ℕ) : WithTop ℕ∞)) f (uIcc t a) rw [hn_succ] exact hf.contDiffOn rcases taylor_mean_remainder_lagrange_iteratedDeriv (f := f) (x := a) (x₀ := t) (n := n) hlt.ne hcont with ⟨ξ, hξ, hrem⟩ rw [Set.uIcc_of_le hlt.le] at hrem rw [Set.uIoo_of_le hlt.le] at hξ have hwithin_eq : taylorWithinEval f n (Icc t a) t a = taylorPoly n f t a := taylorWithinEval_eq_taylorPoly hf (by rw [← hn_succ] exact Nat.le_succ n) hlt have hrem_poly : f a - taylorPoly n f t a = iteratedDeriv p f ξ * (a - t) ^ p / (p.factorial : ℝ) := by rw [← hwithin_eq] simpa [hn_succ] using hrem have hpoly_succ : taylorPoly p f t a = taylorPoly n f t a + iteratedDeriv p f t / (p.factorial : ℝ) * (a - t) ^ p := by rw [← hn_succ] exact taylorPoly_succ n f t a have hdiff : f a - taylorPoly p f t a = (iteratedDeriv p f ξ - iteratedDeriv p f t) / (p.factorial : ℝ) * (a - t) ^ p := by rw [hpoly_succ] rw [sub_add_eq_sub_sub, hrem_poly] have hfac : (p.factorial : ℝ) ≠ 0 := by positivity field_simp [hfac] have hξ_window : ξ ∈ Icc lo hi := ⟨ht.1.trans hξ.1.le, hξ.2.le.trans ha.2⟩ have hdist : |ξ - t| ≤ |a - t| := by rw [abs_of_nonneg (sub_nonneg.mpr hξ.1.le), abs_of_nonneg (sub_nonneg.mpr hlt.le)] exact sub_le_sub_right hξ.2.le t have hpow_le : |ξ - t| ^ (β - (p : ℝ)) ≤ |a - t| ^ (β - (p : ℝ)) := Real.rpow_le_rpow (abs_nonneg _) hdist hexp_nonneg have htop : |iteratedDeriv p f ξ - iteratedDeriv p f t| ≤ M * |a - t| ^ (β - (p : ℝ)) := by simpa [hp] using (hb ξ hξ_window t ht).trans (mul_le_mul_of_nonneg_left hpow_le hM) rw [hdiff] calc |(iteratedDeriv p f ξ - iteratedDeriv p f t) / (p.factorial : ℝ) * (a - t) ^ p| = |iteratedDeriv p f ξ - iteratedDeriv p f t| / (p.factorial : ℝ) * |a - t| ^ p := by rw [abs_mul, abs_div, abs_pow, abs_of_nonneg (by positivity : 0 ≤ (p.factorial : ℝ))] _ ≤ (M * |a - t| ^ (β - (p : ℝ))) / (p.factorial : ℝ) * |a - t| ^ p := by gcongr _ = M / (p.factorial : ℝ) * |a - t| ^ β := by have hcombine : |a - t| ^ (β - (p : ℝ)) * |a - t| ^ p = |a - t| ^ β := by rw [← Real.rpow_natCast] rw [← Real.rpow_add habs_pos] ring_nf rw [← hcombine] ring · -- a < t set b : ℝ := 2 * t - a with hb_def have htb : t < b := by rw [hb_def] linarith have ht_ref : t ∈ Icc t b := Set.left_mem_Icc.mpr htb.le have hb_ref : b ∈ Icc t b := Set.right_mem_Icc.mpr htb.le have hf_ref : ContDiff ℝ p (fun x => f (2 * t - x)) := by fun_prop have hholder_ref : ∀ x ∈ Icc t b, ∀ y ∈ Icc t b, |iteratedDeriv p (fun x => f (2 * t - x)) x - iteratedDeriv p (fun x => f (2 * t - x)) y| ≤ M * |x - y| ^ (β - (p : ℝ)) := by intro x hx y hy have hx_window : 2 * t - x ∈ Icc lo hi := by have hax : a ≤ 2 * t - x := by have hxb : x ≤ 2 * t - a := by simpa [hb_def] using hx.2 linarith have hxt : 2 * t - x ≤ t := by linarith [hx.1] exact ⟨ha.1.trans hax, hxt.trans ht.2⟩ have hy_window : 2 * t - y ∈ Icc lo hi := by have hay : a ≤ 2 * t - y := by have hyb : y ≤ 2 * t - a := by simpa [hb_def] using hy.2 linarith have hyt : 2 * t - y ≤ t := by linarith [hy.1] exact ⟨ha.1.trans hay, hyt.trans ht.2⟩ have hxder := congrFun (iteratedDeriv_comp_const_sub (n := p) (f := f) (s := 2 * t)) x have hyder := congrFun (iteratedDeriv_comp_const_sub (n := p) (f := f) (s := 2 * t)) y rw [hxder, hyder] simp only [smul_eq_mul] have hsign : |(-1 : ℝ) ^ p| = 1 := by simp calc |(-1 : ℝ) ^ p * iteratedDeriv p f (2 * t - x) - (-1 : ℝ) ^ p * iteratedDeriv p f (2 * t - y)| = |iteratedDeriv p f (2 * t - x) - iteratedDeriv p f (2 * t - y)| := by rw [← mul_sub, abs_mul, hsign, one_mul] _ ≤ M * |(2 * t - x) - (2 * t - y)| ^ (β - (p : ℝ)) := hb (2 * t - x) hx_window (2 * t - y) hy_window _ = M * |x - y| ^ (β - (p : ℝ)) := by congr 2 rw [show (2 * t - x) - (2 * t - y) = y - x by ring, abs_sub_comm] have href := holder_taylor_remainder_of_lt (f := fun x => f (2 * t - x)) (M := M) (β := β) (lo := t) (hi := b) (t := t) (a := b) (p := p) hM ht_ref hb_ref hf_ref hholder_ref hp_pos hp_le_beta htb have hgb : (fun x => f (2 * t - x)) b = f a := by have harg : 2 * t - (2 * t - a) = a := by ring simp [hb_def, harg] have hb_abs : |b - t| = |a - t| := by rw [hb_def] rw [show 2 * t - a - t = t - a by ring, abs_sub_comm] have href' : |f a - taylorPoly p f t a| ≤ M / (p.factorial : ℝ) * |b - t| ^ β := by simpa [hgb, hb_def, taylorPoly_reflect] using href simpa [hb_abs] using href'

theorem holder_taylor_monomial_approx {d p : ℕ} {β L r : ℝ} {x0 : Fin d → ℝ} {S : Set (Fin d → ℝ)} (hβ : 0 < β) (hL : 0 < L) (_hr : 0 < r) (hS : {x : Fin d → ℝ | ∀ i, |x i - x0 i| ≤ r} ⊆ S) (expo : Fin p → (Fin d → ℕ)) (hcover : ∀ e : Fin d → ℕ, (∑ j, e j) ≤ ⌈β⌉₊ - 1 → ∃ k, expo k = e) : ∃ Cb : ℝ, 0 ≤ Cb ∧ ∀ f : (Fin d → ℝ) → ℝ, HolderBallStd f β L S → ∀ h : ℝ, 0 < h → h < r → ∃ θ : Fin p → ℝ, ∀ u : Fin d → ℝ, (∀ j, |u j| ≤ 1) → |f (x0 + h • u) - ∑ k, θ k * ∏ j, (u j) ^ (expo k j)| ≤ Cb * L * h ^ β := by classical let m := ⌈β⌉₊ - 1 refine ⟨1 / (Nat.factorial m : ℝ), by positivity, ?_⟩ intro f hf h hh hhr let pick : ∀ (j : Fin (m + 1)) (ι : Fin j → Fin d), Fin p := fun j ι => choose (hcover (indexCount ι) (by rw [sum_indexCount]; omega)) have hpick : ∀ (j : Fin (m + 1)) (ι : Fin j → Fin d), expo (pick j ι) = indexCount ι := fun j ι => Classical.choose_spec (hcover (indexCount ι) (by rw [sum_indexCount]; omega)) let θ : Fin p → ℝ := fun k => ∑ j : Fin (m + 1), ∑ ι : Fin j → Fin d, if pick j ι = k then (1 / (Nat.factorial j : ℝ)) * h ^ (j : ℕ) * iteratedFDeriv ℝ (j : ℕ) f x0 (fun l => single (ι l) 1) else 0 refine ⟨θ, ?_⟩ intro u hu have hpoly : (∑ k, θ k * ∏ i, u i ^ expo k i) = ∑ j : Fin (m + 1), (1 / (Nat.factorial (j : ℕ) : ℝ)) * iteratedFDeriv ℝ (j : ℕ) f x0 (fun _ => h • u) := by simp only [θ, Finset.sum_mul] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro j hj rw [Finset.sum_comm, diagonal_expansion, Finset.mul_sum] apply Finset.sum_congr rfl intro ι hι rw [Finset.sum_eq_single (pick j ι)] · simp [hpick] ring · intro k hk hne simp [hne.symm] · simp have hpoly' : (∑ j ∈ range (m + 1), (1 / (Nat.factorial j : ℝ)) * iteratedFDeriv ℝ j f x0 (fun _ => h • u)) = ∑ k, θ k * ∏ i, u i ^ expo k i := by rw [hpoly] exact (Fin.sum_univ_eq_sum_range _ (m + 1)).symm set U : Set (Fin d → ℝ) := {x | ∀ i, |x i - x0 i| < r} have hU : IsOpen U := by rw [show U = ⋂ i, {x : Fin d → ℝ | |x i - x0 i| < r} by ext x; simp [U]] exact isOpen_iInter_of_finite (fun i => isOpen_lt (by fun_prop) continuous_const) have hUS : U ⊆ S := fun x hx => hS (fun i => le_of_lt (hx i)) have hseg : ∀ t ∈ Icc (0 : ℝ) 1, x0 + t • (h • u) ∈ U := by intro t ht i have he : (x0 + t • (h • u)) i - x0 i = t * (h * u i) := by simp [Pi.add_apply, Pi.smul_apply, smul_eq_mul] rw [he, abs_mul, abs_mul, abs_of_nonneg ht.1, abs_of_pos hh] calc t * (h * |u i|) ≤ 1 * (h * |u i|) := mul_le_mul_of_nonneg_right ht.2 (mul_nonneg hh.le (abs_nonneg _)) _ ≤ h := by simpa using mul_le_mul_of_nonneg_left (hu i) hh.le _ < r := hhr have hb := holder_line_taylor hβ hf hU hUS x0 (h • u) hseg rw [show ⌈β⌉₊ - 1 = m from rfl, hpoly'] at hb have hunorm : ‖u‖ ≤ 1 := by rw [pi_norm_le_iff_of_nonneg (by norm_num)] intro i simpa using hu i have hy : ‖h • u‖ ≤ h := by rw [norm_smul, Real.norm_eq_abs, abs_of_pos hh] calc h * ‖u‖ ≤ h * 1 := mul_le_mul_of_nonneg_left hunorm hh.le _ = h := mul_one h calc _ ≤ (L / (Nat.factorial m : ℝ)) * ‖h • u‖ ^ β := hb _ ≤ (L / (Nat.factorial m : ℝ)) * h ^ β := by gcongr _ = (1 / (Nat.factorial m : ℝ)) * L * h ^ β := by ring

theorem kernelSmoothingBias_bound {f K : ℝ → ℝ} {β M t h : ℝ} (hβ : 0 < β) (hM : 0 ≤ M) (hh : 0 < h) (hK : KernelOrder K (holderDerivOrder β)) (hf : ContDiff ℝ ((holderDerivOrder β)) f) (hb : ∀ x ∈ Icc (t - h) (t + h), ∀ y ∈ Icc (t - h) (t + h), |iteratedDeriv (holderDerivOrder β) f x - iteratedDeriv (holderDerivOrder β) f y| ≤ M * |x - y| ^ (β - ((holderDerivOrder β) : ℝ))) : |kernelSmoothingBias f K t h| ≤ (M / ((holderDerivOrder β)).factorial * ∫ u, |K u|) * h ^ β := by have hKi : Integrable K := hK.integrable have hsupp : ∀ u : ℝ, 1 < |u| → K u = 0 := hK.supp set C : ℝ := M / (((holderDerivOrder β)).factorial : ℝ) * h ^ β with hCdef have hcoef : (0 : ℝ) ≤ M / (((holderDerivOrder β)).factorial : ℝ) := div_nonneg hM (by positivity) have hhb : (0 : ℝ) ≤ h ^ β := Real.rpow_nonneg hh.le β have hCnn : 0 ≤ C := by rw [hCdef]; exact mul_nonneg hcoef hhb -- Monomials `v^k K v` are integrable (bounded by `|K|` on `[-1,1]`, zero off it). have hmono_int : ∀ k : ℕ, Integrable (fun v => v ^ k * K v) := by intro k refine integrable_of_abs_le_const_mul_kernel hKi ((continuous_pow k).aestronglyMeasurable.mul hKi.aestronglyMeasurable) (C := 1) ?_ intro v by_cases hv : |v| ≤ 1 · rw [abs_mul, one_mul] refine mul_le_of_le_one_left (abs_nonneg _) ?_ rw [abs_pow]; exact pow_le_one₀ (abs_nonneg _) hv · exact le_of_eq (by simp [hsupp v (lt_of_not_ge hv)]) -- Pointwise: `K v · Taylor` is a finite sum of scaled monomials in `v K v`. have htay : ∀ v : ℝ, K v * taylorPoly (holderDerivOrder β) f t (t + h * v) = ∑ k ∈ range ((holderDerivOrder β) + 1), (iteratedDeriv k f t / (k.factorial : ℝ) * h ^ k) * (v ^ k * K v) := by intro v unfold taylorPoly rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ have hsub : t + h * v - t = h * v := by ring rw [hsub, mul_pow]; ring have hKtaylor_int : Integrable (fun v => K v * taylorPoly (holderDerivOrder β) f t (t + h * v)) := by have e : (fun v => K v * taylorPoly (holderDerivOrder β) f t (t + h * v)) = (fun v => ∑ k ∈ range ((holderDerivOrder β) + 1), (iteratedDeriv k f t / (k.factorial : ℝ) * h ^ k) * (v ^ k * K v)) := funext htay rw [e] exact integrable_finset_sum _ (fun k _ => (hmono_int k).const_mul _) have hKtay_int : Integrable (fun v => K v * (taylorPoly (holderDerivOrder β) f t (t + h * v) - f t)) := by have e : (fun v => K v * (taylorPoly (holderDerivOrder β) f t (t + h * v) - f t)) = (fun v => K v * taylorPoly (holderDerivOrder β) f t (t + h * v) - K v * f t) := by funext v; rw [mul_sub] rw [e]; exact hKtaylor_int.sub (hKi.mul_const (f t)) -- Moment annihilation: `∫ K · Taylor = f t` (only the constant term survives). have hKtaylor_eq : (∫ v, K v * taylorPoly (holderDerivOrder β) f t (t + h * v)) = f t := by have e : (fun v => K v * taylorPoly (holderDerivOrder β) f t (t + h * v)) = (fun v => ∑ k ∈ range ((holderDerivOrder β) + 1), (iteratedDeriv k f t / (k.factorial : ℝ) * h ^ k) * (v ^ k * K v)) := funext htay rw [e, integral_finset_sum _ (fun k _ => (hmono_int k).const_mul _)] simp_rw [integral_const_mul] rw [Finset.sum_eq_single 0] · have h0 : (∫ v, v ^ (0 : ℕ) * K v) = 1 := by simp only [pow_zero, one_mul]; exact hK.mass rw [h0]; simp [iteratedDeriv_zero] · intro k hk hk0 have hkp : k ≤ (holderDerivOrder β) := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk0 rw [hK.moments k hk1 hkp, mul_zero] · intro h0 exact absurd (Finset.mem_range.mpr (Nat.succ_pos _)) h0 have hmom : (∫ v, K v * (taylorPoly (holderDerivOrder β) f t (t + h * v) - f t)) = 0 := by have e : (fun v => K v * (taylorPoly (holderDerivOrder β) f t (t + h * v) - f t)) = (fun v => K v * taylorPoly (holderDerivOrder β) f t (t + h * v) - K v * f t) := by funext v; rw [mul_sub] rw [e, integral_sub hKtaylor_int (hKi.mul_const (f t)), hKtaylor_eq, integral_mul_const, hK.mass, one_mul, sub_self] -- Remainder: `|K v · (f(t+hv) − Taylor)| ≤ C |K v|` with `C = (M/p!) h^β`. have hRbd : ∀ v : ℝ, |K v * (f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v))| ≤ C * |K v| := by intro v by_cases hv : |v| ≤ 1 · have hvb := abs_le.mp hv have hav : t + h * v ∈ Icc (t - h) (t + h) := by refine ⟨?_, ?_⟩ · nlinarith [hvb.1, hh.le] · nlinarith [hvb.2, hh.le] have htm : t ∈ Icc (t - h) (t + h) := by constructor <;> linarith [hh.le] have hrem := holder_taylor_remainder (lo := t - h) (hi := t + h) (t := t) (a := t + h * v) hβ hM htm hav hf hb have hRvC : |f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v)| ≤ C := by refine le_trans hrem ?_ have h1 : (t + h * v) - t = h * v := by ring rw [h1, abs_mul, abs_of_pos hh, Real.mul_rpow hh.le (abs_nonneg v), hCdef, ← mul_assoc] have h3 : |v| ^ β ≤ 1 := Real.rpow_le_one (abs_nonneg _) hv hβ.le nth_rewrite 2 [← mul_one (M / (((holderDerivOrder β)).factorial : ℝ) * h ^ β)] exact mul_le_mul_of_nonneg_left h3 (mul_nonneg hcoef hhb) calc |K v * (f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v))| = |K v| * |f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v)| := by rw [abs_mul] _ ≤ |K v| * C := mul_le_mul_of_nonneg_left hRvC (abs_nonneg _) _ = C * |K v| := mul_comm _ _ · exact le_of_eq (by simp [hsupp v (lt_of_not_ge hv)]) have hKR_int : Integrable (fun v => K v * (f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v))) := by refine integrable_of_abs_le_const_mul_kernel hKi ?_ hRbd refine hKi.aestronglyMeasurable.mul (Continuous.sub ?_ ?_).aestronglyMeasurable · exact hf.continuous.comp (by fun_prop) · have hcont : Continuous (fun v : ℝ => taylorPoly (holderDerivOrder β) f t (t + h * v)) := by unfold taylorPoly exact continuous_finset_sum _ (fun k _ => by fun_prop) exact hcont -- Assemble: change of variables, split off the annihilated polynomial, bound the rest. rw [kernelSmoothingBias_changeOfVar f K t h hh] have hsplit : (∫ v, K v * (f (t + h * v) - f t)) = (∫ v, K v * (f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v))) + (∫ v, K v * (taylorPoly (holderDerivOrder β) f t (t + h * v) - f t)) := by rw [← integral_add hKR_int hKtay_int] refine integral_congr_ae (Filter.Eventually.of_forall (fun v => ?_)) ring rw [hsplit, hmom, add_zero] calc |∫ v, K v * (f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v))| ≤ ∫ v, |K v * (f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v))| := by have := MeasureTheory.norm_integral_le_integral_norm (μ := volume) (fun v : ℝ => K v * (f (t + h * v) - taylorPoly (holderDerivOrder β) f t (t + h * v))) simpa only [Real.norm_eq_abs] using this _ ≤ ∫ v, C * |K v| := integral_mono hKR_int.abs (hKi.abs.const_mul C) hRbd _ = C * ∫ v, |K v| := by rw [integral_const_mul] _ = (M / ((holderDerivOrder β)).factorial * ∫ u, |K u|) * h ^ β := by rw [hCdef]; ring