Mathlib.Analysis.Calculus.HolderTaylor
Quantitative Hölder calculus on compact real intervals: affine normalization, lower-jet interpolation, primitive and exponential closure, product closure, and uniform endpoint Taylor remainders.
HolderTaylor 3 core · 6 supporting Hölder–Taylor remainder bounds for approximating a smooth regression function near a target point by its degree-⌊β⌋ Taylor polynomial. ★ holder_taylor_remainder
Hölder–Taylor remainder bound
Hölder–Taylor remainder bounds for approximating a smooth regression function near a target point
by its degree-⌊β⌋ Taylor polynomial.
This file proves the standard nonparametric Hölder–Taylor remainder estimate
(Tsybakov, Introduction to Nonparametric Estimation, 2009, Chapter 1): if a
scalar function f is ⌊β⌋-times continuously differentiable and its top
derivative is (β − ⌊β⌋)-Hölder with constant M, then f is approximated near
t by its degree-⌊β⌋ Taylor polynomial with error O(|a − t|^β):
|f a − T_p(a; t)| ≤ (M / p!) · |a − t|^β.
For noninteger β, p = ⌊β⌋. For positive integer β, p = β − 1 and the
Hölder exponent is 1, matching the usual Tsybakov-style convention.
This is the bias-controlling lemma behind interior local-polynomial / kernel
regression: a kernel of order at least p annihilates the Taylor polynomial, leaving
only this remainder, which is the source of the O(h^β) smoothing bias.
def holderDerivOrder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.HolderTaylor
Given a real smoothness index, the Hölder derivative order is the nonnegative integer obtained by subtracting one, with truncation at zero, from the least nonnegative integer that is at least the smoothness index. For positive noninteger this equals , and for positive integer it equals .
Definition (Lean source)
parameters
β :
ℝ
def
holderDerivOrder β :
ℕ
given by
⌈β⌉₊ - 1
def taylorPoly reviewed
⚑ flagged
Causalean.Mathlib.Analysis.HolderTaylor
Given a nonnegative degree, a real-valued function, a real base point, and a real evaluation point, the degree- Taylor polynomial evaluated at the evaluation point is .
Definition (Lean source)
parameters
p :
ℕ
f :
ℝ → ℝ
t a :
ℝ
def
taylorPoly p f t a :
ℝ
given by
∑ k ∈ range (p + 1), iteratedDeriv k f t / (k.factorial : ℝ) * (a - t) ^ k
theorem holder_taylor_remainder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.HolderTaylor
Hölder–Taylor remainder bound under the standard Hölder convention. Let p denote the largest natural number strictly below the smoothness index β. If β is positive, the Hölder constant M is nonnegative, the expansion point t lies in a window [lo,hi], the evaluation point a lies in the same window, f is p times continuously differentiable, and its p-th derivative is (β − p)-Hölder with constant M on the window, then the error of the degree-p Taylor approximation of f at t, evaluated at a, is bounded by (M / p!) · |a − t|^β. For positive integer β = m, this uses derivative order m - 1 and Hölder exponent 1.
Formal statement
hypotheses
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 :
conclusion
|f a - taylorPoly (holderDerivOrder β) f t a|
≤ M / ((holderDerivOrder β)).factorial * |a - t| ^ β
Proof (Lean source)
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, Nat.cast_zero, sub_zero] at hbb
rw [hp0]
simp only [Nat.factorial_zero, Nat.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 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'
6 supporting declarations (lemmas, instances)
-
holderDerivOrder_ltlemmahypothesesβ :ℝhβ :0 < βconclusion(holderDerivOrder β : ℝ) < βProof (Lean source)
lemma holderDerivOrder_lt {β : ℝ} (hβ : 0 < β) : (holderDerivOrder β : ℝ) < β := by have hceil_one : 1 ≤ ⌈β⌉₊ := Nat.one_le_ceil_iff.mpr hβ have hcast : ((⌈β⌉₊ - 1 : ℕ) : ℝ) = (⌈β⌉₊ : ℝ) - 1 := by rw [Nat.cast_sub hceil_one, Nat.cast_one] rw [holderDerivOrder, hcast] linarith [Nat.ceil_lt_add_one hβ.le] -
taylorPoly_eval_basetheorem — The Taylor polynomial of f at base point t, evaluated at t itself, is f t (every positive-degree term carries a (t − t)^k = 0 factor).Proof (Lean source)
theorem taylorPoly_eval_base (p : ℕ) (f : ℝ → ℝ) (t : ℝ) : taylorPoly p f t t = f t := by have h : taylorPoly p f t t = iteratedDeriv 0 f t / (factorial 0 : ℝ) * (t - t) ^ 0 := by unfold taylorPoly refine Finset.sum_eq_single 0 (fun k _ hk => ?_) (fun h => ?_) · rw [sub_self, zero_pow hk, mul_zero] · exact absurd (Finset.mem_range.mpr p.succ_pos) h simpa [iteratedDeriv_zero] using h -
taylorWithinEval_eq_taylorPolylemma — On an interval with distinct endpoints, the Taylor polynomial computed from derivatives restricted to the interval equals the usual Taylor polynomial computed from ordinary derivatives.hypothesesconclusionProof (Lean source)
lemma taylorWithinEval_eq_taylorPoly {f : ℝ → ℝ} {p n : ℕ} {x₀ x : ℝ} (hf : ContDiff ℝ p f) (hn : n ≤ p) (hx : x₀ < x) : taylorWithinEval f n (Icc x₀ x) x₀ x = taylorPoly n f x₀ x := by rw [taylor_within_apply] unfold taylorPoly refine Finset.sum_congr rfl ?_ intro k hk have hk_le_n : k ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) have hk_le_p : k ≤ p := hk_le_n.trans hn have hwithin : iteratedDerivWithin k f (Icc x₀ x) x₀ = iteratedDeriv k f x₀ := by exact iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc hx) ((hf.of_le (WithTop.coe_le_coe.mpr (ENat.coe_le_coe.mpr hk_le_p))).contDiffAt) (Set.left_mem_Icc.mpr hx.le) rw [hwithin] simp [smul_eq_mul, div_eq_mul_inv, mul_comm, mul_left_comm] -
taylorPoly_succlemma — Split the last term off the Taylor polynomial.hypothesesn :ℕf :ℝ → ℝt a :ℝconclusiontaylorPoly (n + 1) f t a= taylorPoly n f t a+ iteratedDeriv (n + 1) f t / ((n + 1).factorial : ℝ) * (a - t) ^ (n + 1)Proof (Lean source)
lemma taylorPoly_succ (n : ℕ) (f : ℝ → ℝ) (t a : ℝ) : taylorPoly (n + 1) f t a = taylorPoly n f t a + iteratedDeriv (n + 1) f t / ((n + 1).factorial : ℝ) * (a - t) ^ (n + 1) := by unfold taylorPoly rw [Finset.sum_range_succ] -
taylorPoly_reflectlemma — Reflecting across the base point preserves the Taylor polynomial value at the reflected evaluation point.hypothesesp :ℕf :ℝ → ℝt a :ℝconclusiontaylorPoly p (fun x => f (2 * t - x)) t (2 * t - a) = taylorPoly p f t aProof (Lean source)
lemma taylorPoly_reflect (p : ℕ) (f : ℝ → ℝ) (t a : ℝ) : taylorPoly p (fun x => f (2 * t - x)) t (2 * t - a) = taylorPoly p f t a := by unfold taylorPoly refine Finset.sum_congr rfl ?_ intro k hk have hder := congrFun (iteratedDeriv_comp_const_sub (n := k) (f := f) (s := 2 * t)) t rw [hder] simp only [smul_eq_mul] have hbase : 2 * t - t = t := by ring have harg : 2 * t - a - t = t - a := by ring have hpow : (-1 : ℝ) ^ k * (t - a) ^ k = (a - t) ^ k := by rw [← mul_pow] congr 1 ring rw [hbase, harg, div_eq_mul_inv] calc ((-1 : ℝ) ^ k * iteratedDeriv k f t) * (↑k.factorial)⁻¹ * (t - a) ^ k = iteratedDeriv k f t * (↑k.factorial)⁻¹ * ((-1 : ℝ) ^ k * (t - a) ^ k) := by ring _ = iteratedDeriv k f t * (↑k.factorial)⁻¹ * (a - t) ^ k := by rw [hpow] -
holder_taylor_remainder_of_ltlemma — Hölder-Taylor remainder when the evaluation point lies to the right of the base.hypothesesf :ℝ → ℝM β lo hi t a :ℝp :ℕhM :0 ≤ Mht :t ∈ Icc lo hiha :a ∈ Icc lo hihf :ContDiff ℝ p fhb :∀ x ∈ Icc lo hi,∀ y ∈ Icc lo hi,|iteratedDeriv p f x - iteratedDeriv p f y| ≤ M * |x - y| ^ (β - (p : ℝ))hp_pos :0 < php_le_beta :(p : ℝ) ≤ βhlt :t < aconclusion|f a - taylorPoly p f t a| ≤ M / (p.factorial : ℝ) * |a - t| ^ βProof (Lean source)
lemma holder_taylor_remainder_of_lt {f : ℝ → ℝ} {M β lo hi t a : ℝ} {p : ℕ} (hM : 0 ≤ M) (ht : t ∈ Icc lo hi) (ha : a ∈ Icc lo hi) (hf : ContDiff ℝ p f) (hb : ∀ x ∈ Icc lo hi, ∀ y ∈ Icc lo hi, |iteratedDeriv p f x - iteratedDeriv p f y| ≤ M * |x - y| ^ (β - (p : ℝ))) (hp_pos : 0 < p) (hp_le_beta : (p : ℝ) ≤ β) (hlt : t < a) : |f a - taylorPoly p f t a| ≤ M / (p.factorial : ℝ) * |a - t| ^ β := by have hexp_nonneg : 0 ≤ β - (p : ℝ) := sub_nonneg.mpr hp_le_beta have habs_pos : 0 < |a - t| := abs_pos.mpr (sub_ne_zero.mpr hlt.ne') 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 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 : ℝ)) := (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
AffineHolder 1 core · 0 supporting The top within-interval Hölder modulus transfers to the intrinsic top coordinate jet on the one-dimensional normalized cube. ★ affine_cube_topHolderOn
Hölder data under interval normalization
The top within-interval Hölder modulus transfers to the intrinsic top coordinate jet on the one-dimensional normalized cube. This supplies the data expected by the existing fixed-cube interpolation theorem.
theorem affine_cube_topHolderOn reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Let f be a function of one real variable on the closed interval from a to a + d, with a derivative order k, where the length d is positive, and suppose its order-k derivative taken within that interval changes between any two points of the interval by at most L times their distance to the power α. Then the rescaled function z ↦ f(a + d/2 + (d/2)·z) on the one-dimensional normalized cube, the interval from −1 to 1, satisfies the intrinsic (within-cube) top-order Hölder condition of order k with exponent α and constant L·(d/2)^k·(d/2)^α.
Formal statement
hypotheses
k :
ℕ
α a d L :
ℝ
hd :
0 < d
f :
ℝ → ℝ
hholder :
∀ x ∈ Icc a (a + d),
∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k f (Icc a (a + d)) x
- iteratedDerivWithin k f (Icc a (a + d)) y|
≤ L * |x - y| ^ α
conclusion
TopHolderOn (cube 1) k α (L * (d / 2) ^ k * (d / 2) ^ α) (fun z : Fin 1 → ℝ => f (a + d / 2 + (d / 2) * z 0))
Proof (Lean source)
theorem affine_cube_topHolderOn
(k : ℕ) (α a d L : ℝ) (hd : 0 < d)
(f : ℝ → ℝ)
(hholder : ∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k f (Icc a (a + d)) x -
iteratedDerivWithin k f (Icc a (a + d)) y| ≤
L * |x - y| ^ α) :
TopHolderOn (cube 1) k α
(L * (d / 2) ^ k * (d / 2) ^ α)
(fun z : Fin 1 → ℝ => f (a + d / 2 + (d / 2) * z 0)) := by
intro q x hx y hy
have hc : 0 < d / 2 := by linarith
have hmap (z : Fin 1 → ℝ) (hz : z ∈ cube 1) :
a + d / 2 + (d / 2) * z 0 ∈ Icc a (a + d) := by
have hz0 := hz 0
constructor <;> nlinarith [hz0.1, hz0.2]
have hnorm : ‖x - y‖ = |x 0 - y 0| := by
simp [Pi.norm_def, Real.norm_eq_abs]
have hdist :
|(a + d / 2 + (d / 2) * x 0) -
(a + d / 2 + (d / 2) * y 0)| = (d / 2) * ‖x - y‖ := by
rw [hnorm]
have heq : (a + d / 2 + (d / 2) * x 0) -
(a + d / 2 + (d / 2) * y 0) = (d / 2) * (x 0 - y 0) := by ring
rw [heq, abs_mul, abs_of_pos hc]
rw [affine_cube_coordJetOn k a d hd f q x hx,
affine_cube_coordJetOn k a d hd f q y hy]
calc
|(d / 2) ^ k * iteratedDerivWithin k f (Icc a (a + d))
(a + d / 2 + (d / 2) * x 0) -
(d / 2) ^ k * iteratedDerivWithin k f (Icc a (a + d))
(a + d / 2 + (d / 2) * y 0)| =
(d / 2) ^ k *
|iteratedDerivWithin k f (Icc a (a + d))
(a + d / 2 + (d / 2) * x 0) -
iteratedDerivWithin k f (Icc a (a + d))
(a + d / 2 + (d / 2) * y 0)| := by
rw [← mul_sub, abs_mul, abs_of_nonneg (pow_nonneg (le_of_lt hc) _)]
_ ≤ (d / 2) ^ k *
(L * |(a + d / 2 + (d / 2) * x 0) -
(a + d / 2 + (d / 2) * y 0)| ^ α) := by
exact mul_le_mul_of_nonneg_left
(hholder _ (hmap x hx) _ (hmap y hy)) (pow_nonneg (le_of_lt hc) _)
_ = (L * (d / 2) ^ k * (d / 2) ^ α) * ‖x - y‖ ^ α := by
rw [hdist, Real.mul_rpow (le_of_lt hc) (norm_nonneg _)]
ring
AffineWithin 1 core · 1 supporting These lemmas transport within-set derivatives from a translated real interval to the normalized one-dimensional cube. ★ affine_cube_coordJetOn
Affine transfer of intrinsic interval jets
These lemmas transport within-set derivatives from a translated real interval to the normalized one-dimensional cube. They are the geometric adapter for fixed-cube Hölder interpolation, including the interval endpoints.
theorem affine_cube_coordJetOn reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
For a function f, a derivative order j, and the closed interval from a to a + d of positive length, at every point z of the closed one-dimensional unit cube and for every choice of j coordinate directions, the order-j within-cube coordinate derivative of the affine pullback of f equals (d/2)^j times the order-j within-interval derivative of f at the image point. This includes both endpoints and order zero.
Formal statement
hypotheses
conclusion
coordJetOn (cube 1) j (fun w : Fin 1 → ℝ => f (a + d / 2 + (d / 2) * w 0)) q z
= (d / 2) ^ j * iteratedDerivWithin j f (Icc a (a + d)) (a + d / 2 + (d / 2) * z 0)
Proof (Lean source)
theorem affine_cube_coordJetOn
(j : ℕ) (a d : ℝ) (hd : 0 < d) (f : ℝ → ℝ)
(q : Fin j → Fin 1) (z : Fin 1 → ℝ) (hz : z ∈ cube 1) :
coordJetOn (cube 1) j
(fun w : Fin 1 → ℝ => f (a + d / 2 + (d / 2) * w 0)) q z =
(d / 2) ^ j *
iteratedDerivWithin j f (Icc a (a + d))
(a + d / 2 + (d / 2) * z 0) := by
let c : ℝ := d / 2
have hc : 0 < c := by dsimp [c]; linarith
have hdc : d = 2 * c := by dsimp [c]; ring
let e₁ := ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ
let e₂ := (LinearEquiv.smulOfNeZero ℝ ℝ c (ne_of_gt hc)).toContinuousLinearEquiv
let e := e₁.trans e₂
let S : Set ℝ := Icc (-c) c
have he (w : Fin 1 → ℝ) : e w = c * w 0 := by
simp [e, e₁, e₂, LinearEquiv.smulOfNeZero_apply, smul_eq_mul]
have hpre : e ⁻¹' S = cube 1 := by
ext w
simp only [Set.mem_preimage, he]
constructor
· intro hw i
have hi : i = 0 := Fin.fin_one_eq_zero i
subst i
constructor <;> nlinarith [hw.1, hw.2]
· intro hw
have hw0 := hw 0
constructor <;> nlinarith [hw0.1, hw0.2]
have hshift : (a + c) +ᵥ S = Icc a (a + d) := by
ext x
simp only [Set.mem_vadd_set, Set.mem_Icc]
constructor
· rintro ⟨y, hy, rfl⟩
change -c ≤ y ∧ y ≤ c at hy
simp only [vadd_eq_add]
constructor <;> nlinarith [hy.1, hy.2, hdc]
· intro hx
refine ⟨x - (a + c), ?_, ?_⟩
· change -c ≤ x - (a + c) ∧ x - (a + c) ≤ c
constructor <;> nlinarith [hx.1, hx.2, hdc]
· simp only [vadd_eq_add]
ring
have huniq : UniqueDiffOn ℝ S := uniqueDiffOn_Icc (by linarith)
have hmap : e z ∈ S := by change z ∈ e ⁻¹' S; rw [hpre]; exact hz
have h₁ := e.iteratedFDerivWithin_comp_right
(fun x : ℝ => f ((a + c) + x)) huniq hmap j
have h₂ := iteratedFDerivWithin_comp_add_left (𝕜 := ℝ)
(f := f) (s := S) j (a + c) (e z)
have h₃ := congrArg (fun T : (Fin 1 → ℝ) [×j]→L[ℝ] ℝ =>
T (fun i => single (q i) (1 : ℝ))) h₁
rw [h₂] at h₃
have hedir (i : Fin j) : e (single (q i) (1 : ℝ)) = c := by
rw [he]
simp [Fin.fin_one_eq_zero]
simpa [coordJetOn, hpre, hshift, Function.comp_def, he, hedir,
ContinuousMultilinearMap.compContinuousLinearMap_apply,
iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod,
Finset.prod_const, Fin.fin_one_eq_zero] using h₃
1 supporting declaration (lemmas, instances)
-
affine_cube_contDiffOntheorem — If a function f is k times continuously differentiable on the closed interval from a to a + d of positive length, then its pullback by the affine map sending the closed one-dimensional unit cube onto that interval is k times continuously differentiable on the cube.hypothesesconclusionContDiffOn ℝ k (fun z : Fin 1 → ℝ => f (a + d / 2 + (d / 2) * z 0)) (cube 1)Proof (Lean source)
theorem affine_cube_contDiffOn (k : ℕ) (a d : ℝ) (hd : 0 < d) (f : ℝ → ℝ) (hf : ContDiffOn ℝ k f (Icc a (a + d))) : ContDiffOn ℝ k (fun z : Fin 1 → ℝ => f (a + d / 2 + (d / 2) * z 0)) (cube 1) := by have hmap (z : Fin 1 → ℝ) (hz : z ∈ cube 1) : a + d / 2 + (d / 2) * z 0 ∈ Icc a (a + d) := by have hz0 : z 0 ∈ Icc (-1 : ℝ) 1 := hz 0 rcases hz0 with ⟨hzlo, hzhi⟩ constructor <;> nlinarith have hinner : ContDiff ℝ k (fun z : Fin 1 → ℝ => a + d / 2 + (d / 2) * z 0) := by fun_prop exact hf.comp hinner.contDiffOn (fun z hz => hmap z hz)
AmbientGrid 1 core · 0 supporting This one-dimensional adapter isolates the finite-grid estimate behind interval interpolation. ★ uniform_interior_ambient_jet_bound
Interior interpolation from ambient Hölder data
This one-dimensional adapter isolates the finite-grid estimate behind interval interpolation. It uses ambient derivatives only at points where the function is smooth in a neighborhood. The later local-window bridge applies it to within derivative data without imposing ambient regularity at the original endpoints.
theorem uniform_interior_ambient_jet_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, a Hölder exponent α with α positive, an interval length d that is positive, and a nonnegative value envelope M and a nonnegative Hölder constant L. Then there is one nonnegative constant B such that, for every interval from a to a + d and every function f that is k times continuously differentiable on it, bounded by M there, and whose ambient k-th derivative is Hölder with constant L and exponent α there, every ambient derivative of f of order at most k is bounded by B at the interior points. This includes order zero.
Formal statement
hypotheses
k :
ℕ
α d M L :
ℝ
hα :
0 < α
hd :
0 < d
hM :
0 ≤ M
hL :
0 ≤ L
conclusion
∃ B : ℝ,
0 ≤ B
conclusion 1
a :
ℝ
f :
ℝ → ℝ
ContDiffOn ℝ k f (Icc a (a + d))
(∀ x ∈ Icc a (a + d), |f x| ≤ M)
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDeriv k f x - iteratedDeriv k f y| ≤ L * |x - y| ^ α)
j ≤ k :
x ∈ Set.Ioo a (a + d) :
|iteratedDeriv j f x| ≤ B
Proof (Lean source)
theorem uniform_interior_ambient_jet_bound
(k : ℕ) (α d M L : ℝ) (hα : 0 < α)
(hd : 0 < d) (hM : 0 ≤ M) (hL : 0 ≤ L) :
∃ B : ℝ, 0 ≤ B ∧
∀ (a : ℝ) (f : ℝ → ℝ),
ContDiffOn ℝ k f (Icc a (a + d)) →
(∀ x ∈ Icc a (a + d), |f x| ≤ M) →
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDeriv k f x - iteratedDeriv k f y| ≤
L * |x - y| ^ α) →
∀ j ≤ k, ∀ x ∈ Ioo a (a + d),
|iteratedDeriv j f x| ≤ B := by
let c : ℝ := d / 2
have hc : 0 < c := by dsimp [c]; linarith
have hdc : d = 2 * c := by dsimp [c]; ring
obtain ⟨K, hK, hfixed⟩ :=
fixed_cube_interpolation
1 k α hα
let R : ℝ := K * (M + L * c ^ k * c ^ α)
let B : ℝ := ∑ j ∈ range (k + 1), R / c ^ j
have hR : 0 ≤ R := by dsimp [R]; positivity
refine ⟨B, Finset.sum_nonneg (fun j hj => div_nonneg hR (pow_nonneg hc.le _)), ?_⟩
intro a f hf hval hholder j hj x hx
let u : (Fin 1 → ℝ) → ℝ := fun z => f (a + c + c * z 0)
have hmap (z : Fin 1 → ℝ)
(hz : z ∈ cube 1) :
a + c + c * z 0 ∈ Icc a (a + d) := by
have hz0 : z 0 ∈ Icc (-1 : ℝ) 1 := hz 0
rcases hz0 with ⟨hzlo, hzhi⟩
constructor <;> nlinarith [hdc]
have hreg : ContDiffOn ℝ k u
(cube 1) := by
have hinner : ContDiff ℝ k (fun z : Fin 1 → ℝ => a + c + c * z 0) := by fun_prop
exact hf.comp hinner.contDiffOn (fun z hz => hmap z hz)
have hjet (i : ℕ) (q : Fin i → Fin 1) (z : Fin 1 → ℝ) :
coordPartial i u q z =
c ^ i * iteratedDeriv i f (a + c + c * z 0) := by
exact (coordPartial_finOne_eq_iteratedDeriv i
(fun t => f (a + c + c * t)) z q).trans
(iteratedDeriv_comp_affine_nonzero i f (a + c) c (ne_of_gt hc) (z 0))
have hval' : ∀ z ∈ cube 1,
|u z| ≤ M := by
intro z hz
exact hval _ (hmap z hz)
have hholder' :
TopHolder
1 k α (L * c ^ k * c ^ α) u := by
intro q z hz w hw
have hdist : |(a + c + c * z 0) - (a + c + c * w 0)| ≤ c * ‖z - w‖ := by
calc
_ = c * |z 0 - w 0| := by
rw [show (a + c + c * z 0) - (a + c + c * w 0) =
c * (z 0 - w 0) by ring, abs_mul, abs_of_pos hc]
_ ≤ c * ‖z - w‖ := by
apply mul_le_mul_of_nonneg_left _ hc.le
simpa [Pi.sub_apply, Real.norm_eq_abs] using norm_le_pi_norm (z - w) 0
have hpow : |(a + c + c * z 0) - (a + c + c * w 0)| ^ α ≤
c ^ α * ‖z - w‖ ^ α := by
calc
_ ≤ (c * ‖z - w‖) ^ α :=
Real.rpow_le_rpow (abs_nonneg _) hdist hα.le
_ = c ^ α * ‖z - w‖ ^ α := Real.mul_rpow hc.le (norm_nonneg _)
rw [hjet k q z, hjet k q w, ← mul_sub, abs_mul, abs_of_nonneg (pow_nonneg hc.le _)]
calc
c ^ k * |iteratedDeriv k f (a + c + c * z 0) -
iteratedDeriv k f (a + c + c * w 0)| ≤
c ^ k * (L * |(a + c + c * z 0) - (a + c + c * w 0)| ^ α) :=
mul_le_mul_of_nonneg_left
(hholder _ (hmap z hz) _ (hmap w hw)) (pow_nonneg hc.le _)
_ ≤ c ^ k * (L * (c ^ α * ‖z - w‖ ^ α)) :=
mul_le_mul_of_nonneg_left
(mul_le_mul_of_nonneg_left hpow hL) (pow_nonneg hc.le _)
_ = (L * c ^ k * c ^ α) * ‖z - w‖ ^ α := by ring
have hbound := hfixed u M (L * c ^ k * c ^ α) hM (by positivity)
hreg hval' hholder'
let z : Fin 1 → ℝ := fun _ => (x - (a + c)) / c
have hz : z ∈ cube 1 := by
intro i
have hi : i = 0 := Subsingleton.elim i 0
subst i
change -1 ≤ (x - (a + c)) / c ∧ (x - (a + c)) / c ≤ 1
constructor
· apply (le_div_iff₀ hc).2
nlinarith [hx.1, hx.2]
· apply (div_le_iff₀ hc).2
nlinarith [hx.1, hx.2]
have hzx : a + c + c * z 0 = x := by
dsimp [z]
field_simp
ring
have hjbound := hbound j hj (fun _ => 0) z hz
rw [hjet j (fun _ => 0) z, hzx] at hjbound
have hsmall : |iteratedDeriv j f x| ≤ R / c ^ j := by
apply (le_div_iff₀ (pow_pos hc j)).2
simpa [abs_mul, abs_of_nonneg (pow_nonneg hc.le _), R, mul_comm] using hjbound
exact hsmall.trans (Finset.single_le_sum
(fun i _ => div_nonneg hR (pow_nonneg hc.le i)) (Finset.mem_range.mpr (Nat.lt_succ_of_le hj)))
BoundaryTransfer 1 core · 0 supporting Continuity of the within jet on a compact interval carries any common interior bound to both endpoints. ★ within_jet_bound_of_interior_ambient_bound
Transfer of interior derivative bounds to endpoint within derivatives
Continuity of the within jet on a compact interval carries any common interior bound to both endpoints. The statement makes no global smoothness assumption outside the interval.
theorem within_jet_bound_of_interior_ambient_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
If a function f is k times continuously differentiable on a compact interval from a to b that is nondegenerate, and for one constant B all its ordinary (ambient) derivatives of order at most k are bounded in absolute value by B at every interior point, then all its within-interval derivatives of order at most k are bounded in absolute value by B at every point of the closed interval, both endpoints included. No smoothness outside the interval is assumed.
Formal statement
hypotheses
k :
ℕ
a b B :
ℝ
hab :
a < b
f :
ℝ → ℝ
hf :
ContDiffOn ℝ k f (Set.Icc a b)
hinterior :
∀ j ≤ k, ∀ x ∈ Ioo a b, |iteratedDeriv j f x| ≤ B
j ≤ k :
x ∈ Set.Icc a b :
conclusion
|iteratedDerivWithin j f (Set.Icc a b) x| ≤ B
Proof (Lean source)
theorem within_jet_bound_of_interior_ambient_bound
(k : ℕ) (a b B : ℝ) (hab : a < b)
(f : ℝ → ℝ) (hf : ContDiffOn ℝ k f (Icc a b))
(hinterior : ∀ j ≤ k, ∀ x ∈ Ioo a b,
|iteratedDeriv j f x| ≤ B) :
∀ j ≤ k, ∀ x ∈ Icc a b,
|iteratedDerivWithin j f (Icc a b) x| ≤ B := by
/- On Ioo, the within derivative equals the ambient derivative because
Icc is a neighborhood of each interior point. `ContDiffOn` and
`uniqueDiffOn_Icc` make every within jet continuous on Icc. Since Ioo is
dense in Icc, extend the interior bound with `le_on_closure`. -/
intro j hj x hx
have hu : UniqueDiffOn ℝ (Icc a b) := uniqueDiffOn_Icc hab
have hcont : ContinuousOn
(fun y => |iteratedDerivWithin j f (Icc a b) y|) (Icc a b) :=
(hf.continuousOn_iteratedDerivWithin (by exact_mod_cast hj) hu).abs
have hbound : ∀ y ∈ Ioo a b,
|iteratedDerivWithin j f (Icc a b) y| ≤ B := by
intro y hy
have hreg : ContDiffAt ℝ j f y :=
((hf.mono Set.Ioo_subset_Icc_self).contDiffAt
(isOpen_Ioo.mem_nhds hy)).of_le (by exact_mod_cast hj)
rw [iteratedDerivWithin_eq_iteratedDeriv hu hreg
(Set.Ioo_subset_Icc_self hy)]
exact hinterior j hj y hy
exact le_on_closure hbound
(by simpa [closure_Ioo hab.ne] using hcont)
continuousOn_const (by simpa [closure_Ioo hab.ne] using hx)
BoundedTopGrid 1 core · 0 supporting This isolates the finite-grid estimate for a bounded highest derivative. ★ uniform_interior_ambient_jet_bound_of_top_bound
Interior interpolation from a bounded top derivative
This isolates the finite-grid estimate for a bounded highest derivative.
The boundary trace is handled separately by BoundaryTransfer.
theorem uniform_interior_ambient_jet_bound_of_top_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, an interval length d that is positive, a nonnegative value envelope M and a nonnegative top-derivative envelope T. Then there is one nonnegative constant B such that, for every interval from a to a + d and every function f that is k times continuously differentiable on it, bounded by M there, and whose k-th within-interval derivative is bounded by T there, every ambient derivative of f of order at most k is bounded by B at the interior points.
Formal statement
hypotheses
k :
ℕ
d M T :
ℝ
hd :
0 < d
hM :
0 ≤ M
hT :
0 ≤ T
conclusion
∃ B : ℝ,
0 ≤ B
conclusion 1
a :
ℝ
f :
ℝ → ℝ
ContDiffOn ℝ k f (Icc a (a + d))
(∀ x ∈ Icc a (a + d), |f x| ≤ M)
j ≤ k :
x ∈ Set.Ioo a (a + d) :
|iteratedDeriv j f x| ≤ B
Proof (Lean source)
theorem uniform_interior_ambient_jet_bound_of_top_bound
(k : ℕ) (d M T : ℝ) (hd : 0 < d) (hM : 0 ≤ M) (hT : 0 ≤ T) :
∃ B : ℝ, 0 ≤ B ∧
∀ (a : ℝ) (f : ℝ → ℝ),
ContDiffOn ℝ k f (Icc a (a + d)) →
(∀ x ∈ Icc a (a + d), |f x| ≤ M) →
(∀ x ∈ Icc a (a + d),
|iteratedDerivWithin k f (Icc a (a + d)) x| ≤ T) →
∀ j ≤ k, ∀ x ∈ Ioo a (a + d),
|iteratedDeriv j f x| ≤ B := by
cases k with
| zero =>
refine ⟨M, hM, ?_⟩
intro a f hf hval htop j hj x hx
have hj0 : j = 0 := Nat.eq_zero_of_le_zero hj
subst j
simpa using hval x (Set.Ioo_subset_Icc_self hx)
| succ n =>
obtain ⟨B, hB, hbound⟩ :=
uniform_interior_ambient_jet_bound n 1 (d / 2) M T
(by norm_num) (by linarith) hM hT
refine ⟨max B T, le_max_of_le_left hB, ?_⟩
intro a f hf hval htop j hj x hx
have hab : a < a + d := by linarith
have hu : UniqueDiffOn ℝ (Icc a (a + d)) := uniqueDiffOn_Icc hab
have hreg (y : ℝ) (hy : y ∈ Ioo a (a + d)) :
ContDiffAt ℝ (n + 1) f y :=
(hf.mono Set.Ioo_subset_Icc_self).contDiffAt (isOpen_Ioo.mem_nhds hy)
have htop' (y : ℝ) (hy : y ∈ Ioo a (a + d)) :
|iteratedDeriv (n + 1) f y| ≤ T := by
rw [← iteratedDerivWithin_eq_iteratedDeriv hu (hreg y hy)
(Set.Ioo_subset_Icc_self hy)]
exact htop y (Set.Ioo_subset_Icc_self hy)
by_cases hjtop : j = n + 1
· subst j
exact (htop' x hx).trans (le_max_right _ _)
· have hjlow : j ≤ n := by omega
let b : ℝ := (a + x) / 2
have hsub : Icc b (b + d / 2) ⊆ Ioo a (a + d) := by
intro y hy
dsimp [b] at hy
constructor <;> nlinarith [hy.1, hy.2, hx.1, hx.2, hd]
have hx' : x ∈ Ioo b (b + d / 2) := by
dsimp [b]
constructor <;> nlinarith [hx.1, hx.2]
have hf' : ContDiffOn ℝ n f (Icc b (b + d / 2)) :=
(hf.of_le (by exact_mod_cast le_succ n)).mono
(Set.Subset.trans hsub Set.Ioo_subset_Icc_self)
have hval' : ∀ y ∈ Icc b (b + d / 2), |f y| ≤ M := by
intro y hy
exact hval y (Set.Ioo_subset_Icc_self (hsub hy))
have hdiffioo : DifferentiableOn ℝ (iteratedDeriv n f)
(Ioo a (a + d)) := by
exact ((hf.mono Set.Ioo_subset_Icc_self).differentiableOn_iteratedDerivWithin
(Nat.cast_lt.mpr n.lt_succ_self) isOpen_Ioo.uniqueDiffOn).congr
(fun y hy => (iteratedDerivWithin_of_isOpen isOpen_Ioo hy).symm)
have hholder : ∀ y ∈ Icc b (b + d / 2),
∀ z ∈ Icc b (b + d / 2),
|iteratedDeriv n f y - iteratedDeriv n f z| ≤
T * |y - z| ^ (1 : ℝ) := by
intro y hy z hz
have hmv := (convex_Ioo a (a + d)).norm_image_sub_le_of_norm_derivWithin_le
hdiffioo (fun w hw => by
rw [derivWithin_of_isOpen isOpen_Ioo hw, ← iteratedDeriv_succ,
Real.norm_eq_abs]
exact htop' w hw) (hsub hy) (hsub hz)
simpa [Real.norm_eq_abs, abs_sub_comm] using hmv
exact (hbound b f hf' hval' hholder j hjlow x hx').trans (le_max_left _ _)
Endpoint 1 core · 1 supporting The endpoint result needs only within-interval regularity; its coefficients are chosen separately for each function and its constant is uniform over all translated intervals of the same length. ★ endpoint_holder_taylor
Endpoint Taylor remainder from a top Hölder modulus
The endpoint result needs only within-interval regularity; its coefficients are chosen separately for each function and its constant is uniform over all translated intervals of the same length.
theorem endpoint_holder_taylor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, a Hölder exponent α with α positive, an interval length d that is positive, and a nonnegative Hölder constant L. Then there is one nonnegative constant C such that every function f that is k times continuously differentiable on an interval from a to a + d, with k-th within-interval derivative Hölder with constant L and exponent α there, has a polynomial of degree at most k in the distance a + d − t to the right endpoint whose error at every point t of the interval is at most C times that distance to the power k + α. The polynomial coefficients may depend on f; this includes k = 0.
Formal statement
hypotheses
k :
ℕ
α d L :
ℝ
hα :
0 < α
hd :
0 < d
hL :
0 ≤ L
conclusion
∃ C : ℝ,
0 ≤ C
conclusion 1
a :
ℝ
f :
ℝ → ℝ
ContDiffOn ℝ k f (Icc a (a + d))
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x - iteratedDerivWithin k f (Icc a (a + d)) y| ≤ L * |x - y| ^ α)
Proof (Lean source)
theorem endpoint_holder_taylor
(k : ℕ) (α d L : ℝ) (hα : 0 < α)
(hd : 0 < d) (hL : 0 ≤ L) :
∃ C : ℝ, 0 ≤ C ∧
∀ (a : ℝ) (f : ℝ → ℝ),
ContDiffOn ℝ k f (Set.Icc a (a + d)) →
(∀ x ∈ Set.Icc a (a + d), ∀ y ∈ Set.Icc a (a + d),
|iteratedDerivWithin k f (Set.Icc a (a + d)) x -
iteratedDerivWithin k f (Set.Icc a (a + d)) y| ≤
L * |x - y| ^ α) →
∃ coeff : Fin (k + 1) → ℝ,
∀ t ∈ Set.Icc a (a + d),
|f t - ∑ j : Fin (k + 1), coeff j * (a + d - t) ^ j.val| ≤
C * (a + d - t) ^ ((k : ℝ) + α) := by
refine ⟨L, hL, ?_⟩
intro a f hf hholder
let b := a + d
let s := Set.Icc a b
let coeff : Fin (k + 1) → ℝ := fun j =>
(Nat.factorial j.val : ℝ)⁻¹ * iteratedDerivWithin j.val f s b * (-1 : ℝ) ^ j.val
refine ⟨coeff, ?_⟩
intro t ht
have hab : a < b := by dsimp [b]; linarith
have htb : t ≤ b := ht.2
have hpow (j : ℕ) : (t - b) ^ j = (-1 : ℝ) ^ j * (b - t) ^ j := by
rw [show t - b = (-1 : ℝ) * (b - t) by ring, mul_pow]
have hpoly :
(∑ j : Fin (k + 1), coeff j * (b - t) ^ j.val) =
∑ j ∈ range (k + 1),
(Nat.factorial j : ℝ)⁻¹ * iteratedDerivWithin j f s b * (t - b) ^ j := by
rw [← Fin.sum_univ_eq_sum_range]
apply Finset.sum_congr rfl
intro j hj
simp only [coeff]
rw [hpow]
ring
rw [hpoly]
by_cases hzero : k = 0
· subst k
simp only [Finset.range_one, Finset.sum_singleton, Nat.factorial_zero,
Nat.cast_one, inv_one, iteratedDerivWithin_zero, pow_zero, mul_one,
one_mul, Nat.cast_zero, zero_add]
have h := hholder t ht b (Set.right_mem_Icc.mpr hab.le)
simpa [abs_of_nonpos (sub_nonpos.mpr htb), s, b] using h
have hk : 0 < k := Nat.pos_of_ne_zero hzero
have hexp : 0 < (k : ℝ) + α := by positivity
by_cases hteq : t = b
· subst t
have hsum :
(∑ j ∈ range (k + 1),
(Nat.factorial j : ℝ)⁻¹ * iteratedDerivWithin j f s b * (b - b) ^ j) = f b := by
rw [Finset.sum_eq_single 0]
· simp
· intro j hj hj0
simp [hj0]
· simp
rw [hsum]
simpa [b] using (mul_nonneg hL (Real.rpow_nonneg (sub_nonneg.mpr htb) _))
have hlt : t < b := lt_of_le_of_ne htb hteq
have hseg : Set.Icc t b ⊆ s := by
intro z hz
exact ⟨ht.1.trans hz.1, hz.2⟩
have hlocal : s =ᶠ[𝓝 b] Set.Icc t b := by
filter_upwards [Ioi_mem_nhds hlt] with z hz
change (a ≤ z ∧ z ≤ b) = (t ≤ z ∧ z ≤ b)
change t < z at hz
exact propext (by
constructor
· intro h
exact ⟨hz.le, h.2⟩
· intro h
exact ⟨ht.1.trans h.1, h.2⟩)
have hbase (j : ℕ) :
iteratedDerivWithin j f (Set.Icc t b) b = iteratedDerivWithin j f s b := by
rw [iteratedDerivWithin_eq_iteratedFDerivWithin,
iteratedDerivWithin_eq_iteratedFDerivWithin,
iteratedFDerivWithin_congr_set (f := f) hlocal.symm]
let n := k - 1
have hn : n + 1 = k := Nat.succ_pred_eq_of_pos hk
have hcont : ContDiffOn ℝ (n + 1) f (uIcc b t) := by
change ContDiffOn ℝ (↑(n + 1 : ℕ)) f (uIcc b t)
rw [Set.uIcc_of_ge htb, hn]
exact hf.mono hseg
obtain ⟨ξ, hξ, hrem⟩ :=
taylor_mean_remainder_lagrange_iteratedDeriv (f := f) (x := t) (x₀ := b)
(n := n) (Ne.symm hteq) hcont
have hξmem : ξ ∈ s := by
apply hseg
rw [Set.uIoo_of_ge htb] at hξ
exact ⟨hξ.1.le, hξ.2.le⟩
have hξderiv : iteratedDeriv k f ξ = iteratedDerivWithin k f s ξ := by
have hξint : ξ ∈ Ioo a b := by
rw [Set.uIoo_of_ge htb] at hξ
exact ⟨ht.1.trans_lt hξ.1, hξ.2⟩
exact (iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc hab)
(hf.contDiffAt (Icc_mem_nhds hξint.1 hξint.2)) hξmem).symm
have hξdist : |ξ - b| ≤ |t - b| := by
rw [Set.uIoo_of_ge htb] at hξ
rw [abs_of_nonpos (sub_nonpos.mpr hξ.2.le),
abs_of_nonpos (sub_nonpos.mpr htb)]
linarith [hξ.1]
have htop : |iteratedDeriv k f ξ - iteratedDerivWithin k f s b| ≤
L * |t - b| ^ α := by
rw [hξderiv]
exact (hholder ξ hξmem b (Set.right_mem_Icc.mpr hab.le)).trans
(mul_le_mul_of_nonneg_left
(Real.rpow_le_rpow (abs_nonneg _) hξdist hα.le) hL)
have hpolyN : taylorWithinEval f n (uIcc b t) b t =
∑ j ∈ range (n + 1),
(Nat.factorial j : ℝ)⁻¹ * iteratedDerivWithin j f s b * (t - b) ^ j := by
rw [taylor_within_apply]
apply Finset.sum_congr rfl
intro j hj
rw [Set.uIcc_of_ge htb, hbase]
simp only [smul_eq_mul]
ring
have hdiff :
f t - (∑ j ∈ range (k + 1),
(Nat.factorial j : ℝ)⁻¹ * iteratedDerivWithin j f s b * (t - b) ^ j) =
(iteratedDeriv k f ξ - iteratedDerivWithin k f s b) /
(Nat.factorial k : ℝ) * (t - b) ^ k := by
rw [← hn, Finset.sum_range_succ, ← hpolyN, sub_add_eq_sub_sub, hrem, hn]
ring
rw [hdiff]
have hfac : 1 ≤ (Nat.factorial k : ℝ) := by
exact_mod_cast Nat.factorial_pos k
have hdistpos : 0 < |t - b| := abs_pos.mpr (sub_ne_zero.mpr hteq)
calc
|(iteratedDeriv k f ξ - iteratedDerivWithin k f s b) /
(Nat.factorial k : ℝ) * (t - b) ^ k| =
|iteratedDeriv k f ξ - iteratedDerivWithin k f s b| /
(Nat.factorial k : ℝ) * |t - b| ^ k := by
rw [abs_mul, abs_div, abs_pow, abs_of_nonneg (by linarith : (0 : ℝ) ≤ k.factorial)]
_ ≤ L * |t - b| ^ α / (Nat.factorial k : ℝ) * |t - b| ^ k := by
gcongr
_ ≤ L * |t - b| ^ α * |t - b| ^ k := by
gcongr
exact div_le_self (mul_nonneg hL (Real.rpow_nonneg (abs_nonneg _) _)) hfac
_ = L * (b - t) ^ ((k : ℝ) + α) := by
rw [abs_of_nonpos (sub_nonpos.mpr htb)]
have hp : (b - t) ^ α * (b - t) ^ k = (b - t) ^ ((k : ℝ) + α) := by
rw [← Real.rpow_natCast, ← Real.rpow_add (by linarith : 0 < b - t)]
congr 1
ring
rw [neg_sub, mul_assoc, hp]
1 supporting declaration (lemmas, instances)
-
endpoint_holder_taylor_Icctheorem — Fix a derivative order k, a Hölder exponent α with α positive, endpoints a and b with a < b, and a nonnegative Hölder constant L. Then there is one nonnegative constant C such that every function f that is k times continuously differentiable on the interval from a to b, with k-th within-interval derivative Hölder with constant L and exponent α there, has a polynomial of degree at most k in b − t whose error at every point t of the interval is at most C·(b − t)^(k + α). The coefficients may depend on the function, while the remainder constant depends only on the order, exponent, length, and Hölder constant.hypothesesk :ℕα a b L :ℝhα :0 < αhab :a < bhL :0 ≤ Lconclusion∃ C : ℝ,0 ≤ Cconclusion 1f :ℝ → ℝContDiffOn ℝ k f (Icc a b)(∀ x ∈ Icc a b, ∀ y ∈ Icc a b, |iteratedDerivWithin k f (Icc a b) x - iteratedDerivWithin k f (Icc a b) y| ≤ L * |x - y| ^ α)Proof (Lean source)
theorem endpoint_holder_taylor_Icc (k : ℕ) (α a b L : ℝ) (hα : 0 < α) (hab : a < b) (hL : 0 ≤ L) : ∃ C : ℝ, 0 ≤ C ∧ ∀ (f : ℝ → ℝ), ContDiffOn ℝ k f (Icc a b) → (∀ x ∈ Icc a b, ∀ y ∈ Icc a b, |iteratedDerivWithin k f (Icc a b) x - iteratedDerivWithin k f (Icc a b) y| ≤ L * |x - y| ^ α) → ∃ coeff : Fin (k + 1) → ℝ, ∀ t ∈ Icc a b, |f t - ∑ j : Fin (k + 1), coeff j * (b - t) ^ j.val| ≤ C * (b - t) ^ ((k : ℝ) + α) := by obtain ⟨C, hC, hbound⟩ := endpoint_holder_taylor k α (b - a) L hα (sub_pos.mpr hab) hL refine ⟨C, hC, ?_⟩ intro f hf hholder have heq : a + (b - a) = b := by ring simpa [heq] using (hbound a f (by simpa [heq] using hf) (by simpa [heq] using hholder))
Interpolation 1 core · 2 supporting Finite-interval interpolation for scalar functions, stated directly in terms of ContDiffOn and iteratedDerivWithin. ★ uniform_iteratedDerivWithin_bound
Uniform derivative bounds from a top Hölder modulus
Finite-interval interpolation for scalar functions, stated directly in terms of
ContDiffOn and iteratedDerivWithin. The constant is uniform under translation
of an interval of fixed positive length.
theorem uniform_iteratedDerivWithin_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, a Hölder exponent α with α positive, an interval length d that is positive, and a nonnegative value envelope M and a nonnegative Hölder constant L. Then there is one nonnegative constant B such that, for every interval from a to a + d and every function f that is k times continuously differentiable on it, bounded by M there, and whose k-th within-interval derivative is Hölder with constant L and exponent α there, every within-interval derivative of f of order at most k is bounded by B on the whole interval.
Formal statement
hypotheses
k :
ℕ
α d M L :
ℝ
hα :
0 < α
hd :
0 < d
hM :
0 ≤ M
hL :
0 ≤ L
conclusion
∃ B : ℝ,
0 ≤ B
conclusion 1
a :
ℝ
f :
ℝ → ℝ
ContDiffOn ℝ k f (Icc a (a + d))
(∀ x ∈ Icc a (a + d), |f x| ≤ M)
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x - iteratedDerivWithin k f (Icc a (a + d)) y| ≤ L * |x - y| ^ α)
j ≤ k :
x ∈ Set.Icc a (a + d) :
|iteratedDerivWithin j f (Icc a (a + d)) x| ≤ B
Proof (Lean source)
theorem uniform_iteratedDerivWithin_bound
(k : ℕ) (α d M L : ℝ) (hα : 0 < α)
(hd : 0 < d) (hM : 0 ≤ M) (hL : 0 ≤ L) :
∃ B : ℝ, 0 ≤ B ∧
∀ (a : ℝ) (f : ℝ → ℝ),
ContDiffOn ℝ k f (Icc a (a + d)) →
(∀ x ∈ Icc a (a + d), |f x| ≤ M) →
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k f (Icc a (a + d)) x -
iteratedDerivWithin k f (Icc a (a + d)) y| ≤
L * |x - y| ^ α) →
∀ j ≤ k, ∀ x ∈ Icc a (a + d),
|iteratedDerivWithin j f (Icc a (a + d)) x| ≤ B := by
obtain ⟨T, hT, htop⟩ :=
uniform_top_iteratedDerivWithin_bound k α d M L hα hd hM hL
obtain ⟨B, hB, hbound⟩ :=
uniform_lower_iteratedDerivWithin_of_top_bound k d M T hd hM hT
exact ⟨B, hB, fun a f hf hM' hL' =>
hbound a f hf hM' (htop a f hf hM' hL')⟩
2 supporting declarations (lemmas, instances)
-
uniform_top_iteratedDerivWithin_boundtheorem — Fix a derivative order k, a Hölder exponent α with α positive, an interval length d that is positive, and a nonnegative value envelope M and a nonnegative Hölder constant L. Then there is one nonnegative constant B such that, for every interval from a to a + d and every function f that is k times continuously differentiable on it, bounded by M there, and whose k-th within-interval derivative is Hölder with constant L and exponent α there, that k-th derivative is bounded by B on the whole interval. The bound is independent of the interval location and the function.hypothesesk :ℕα d M L :ℝhα :0 < αhd :0 < dhM :0 ≤ MhL :0 ≤ Lconclusion∃ B : ℝ,0 ≤ Bconclusion 1a :ℝf :ℝ → ℝContDiffOn ℝ k f (Icc a (a + d))(∀ x ∈ Icc a (a + d), |f x| ≤ M)(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x - iteratedDerivWithin k f (Icc a (a + d)) y| ≤ L * |x - y| ^ α)x ∈ Set.Icc a (a + d) :|iteratedDerivWithin k f (Icc a (a + d)) x| ≤ BProof (Lean source)
theorem uniform_top_iteratedDerivWithin_bound (k : ℕ) (α d M L : ℝ) (hα : 0 < α) (hd : 0 < d) (hM : 0 ≤ M) (hL : 0 ≤ L) : ∃ B : ℝ, 0 ≤ B ∧ ∀ (a : ℝ) (f : ℝ → ℝ), ContDiffOn ℝ k f (Icc a (a + d)) → (∀ x ∈ Icc a (a + d), |f x| ≤ M) → (∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x - iteratedDerivWithin k f (Icc a (a + d)) y| ≤ L * |x - y| ^ α) → ∀ x ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x| ≤ B := by obtain ⟨K, hK, hfixed⟩ := fixed_cube_interpolation_within 1 k α hα let c : ℝ := d / 2 have hc : 0 < c := by dsimp [c]; linarith let R : ℝ := K * (M + L * c ^ k * c ^ α) let B : ℝ := R / c ^ k have hR : 0 ≤ R := by dsimp [R]; positivity refine ⟨B, div_nonneg hR (pow_nonneg hc.le _), ?_⟩ intro a f hf hval hholder x hx let u : (Fin 1 → ℝ) → ℝ := fun z => f (a + c + c * z 0) have hmap (z : Fin 1 → ℝ) (hz : z ∈ cube 1) : a + c + c * z 0 ∈ Icc a (a + d) := by have hz0 := hz 0 dsimp [c] at * constructor <;> nlinarith [hz0.1, hz0.2] have hu : ContDiffOn ℝ k u (cube 1) := by simpa [u, c] using affine_cube_contDiffOn k a d hd f hf have hval' : ∀ z ∈ cube 1, |u z| ≤ M := by intro z hz exact hval _ (hmap z hz) have hL' : 0 ≤ L * c ^ k * c ^ α := by positivity have hholder' : TopHolderOn (cube 1) k α (L * c ^ k * c ^ α) u := by simpa [u, c] using affine_cube_topHolderOn k α a d L hd f hholder let z : Fin 1 → ℝ := fun _ => (x - a - c) / c have hz : z ∈ cube 1 := by intro i have hi : i = 0 := Fin.fin_one_eq_zero i subst i change -1 ≤ (x - a - c) / c ∧ (x - a - c) / c ≤ 1 constructor · apply (le_div_iff₀ hc).2 dsimp [c] nlinarith [hx.1] · apply (div_le_iff₀ hc).2 dsimp [c] nlinarith [hx.2] have heq : a + c + c * z 0 = x := by dsimp [z] field_simp ring have hbound := hfixed u M (L * c ^ k * c ^ α) hM hL' hu hval' hholder' k (le_refl k) (fun _ => (0 : Fin 1)) z hz rw [affine_cube_coordJetOn k a d hd f (fun _ => (0 : Fin 1)) z hz] at hbound change |c ^ k * iteratedDerivWithin k f (Icc a (a + d)) (a + c + c * z 0)| ≤ R at hbound rw [heq, abs_mul, abs_of_pos (pow_pos hc _)] at hbound change |iteratedDerivWithin k f (Icc a (a + d)) x| ≤ R / c ^ k apply (le_div_iff₀ (pow_pos hc _)).2 nlinarith [hbound] -
uniform_lower_iteratedDerivWithin_of_top_boundtheorem — Fix a derivative order k, an interval length d that is positive, a nonnegative value envelope M and a nonnegative top-derivative envelope T. Then there is one nonnegative constant B such that, for every interval from a to a + d and every function f that is k times continuously differentiable on it, bounded by M there, and whose k-th within-interval derivative is bounded by T there, every within-interval derivative of f of order at most k is bounded by B on the whole interval, endpoints included.hypothesesk :ℕd M T :ℝhd :0 < dhM :0 ≤ MhT :0 ≤ Tconclusion∃ B : ℝ,0 ≤ Bconclusion 1a :ℝf :ℝ → ℝContDiffOn ℝ k f (Icc a (a + d))(∀ x ∈ Icc a (a + d), |f x| ≤ M)j ≤ k :x ∈ Set.Icc a (a + d) :|iteratedDerivWithin j f (Icc a (a + d)) x| ≤ BProof (Lean source)
theorem uniform_lower_iteratedDerivWithin_of_top_bound (k : ℕ) (d M T : ℝ) (hd : 0 < d) (hM : 0 ≤ M) (hT : 0 ≤ T) : ∃ B : ℝ, 0 ≤ B ∧ ∀ (a : ℝ) (f : ℝ → ℝ), ContDiffOn ℝ k f (Icc a (a + d)) → (∀ x ∈ Icc a (a + d), |f x| ≤ M) → (∀ x ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x| ≤ T) → ∀ j ≤ k, ∀ x ∈ Icc a (a + d), |iteratedDerivWithin j f (Icc a (a + d)) x| ≤ B := by obtain ⟨B, hB, hinterior⟩ := uniform_interior_ambient_jet_bound_of_top_bound k d M T hd hM hT refine ⟨B, hB, ?_⟩ intro a f hf hval htop exact within_jet_bound_of_interior_ambient_bound k a (a + d) B (by linarith) f hf (hinterior a f hf hval htop)
JetHolder 1 core · 0 supporting A bound on one more derivative gives a Lipschitz estimate on a compact interval and hence a Hölder estimate at every exponent up to one. ★ lower_jet_holder_of_next_bound
Hölder control of a lower within-interval jet
A bound on one more derivative gives a Lipschitz estimate on a compact interval and hence a Hölder estimate at every exponent up to one.
theorem lower_jet_holder_of_next_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
If a function f is j + 1 times continuously differentiable on the closed interval from a to a + d of positive length, and its within-interval derivative of order j + 1 is bounded in absolute value by B on that interval, with B nonnegative, then for every exponent α that is positive and at most one, the order-j within-interval derivative is Hölder with exponent α and constant B·d^(1 − α): at any two points x, y of the interval its values differ by at most B·d^(1 − α)·|x − y|^α. Pairs involving either endpoint are included.
Formal statement
hypotheses
j :
ℕ
α a d B :
ℝ
hα :
0 < α
hα1 :
α ≤ 1
hd :
0 < d
hB :
0 ≤ B
f :
ℝ → ℝ
hf :
ContDiffOn ℝ (j + 1) f (Icc a (a + d))
hbound :
x ∈ Set.Icc a (a + d) :
y ∈ Set.Icc a (a + d) :
conclusion
|iteratedDerivWithin j f (Icc a (a + d)) x
- iteratedDerivWithin j f (Icc a (a + d)) y|
≤ (B * d ^ (1 - α)) * |x - y| ^ α
Proof (Lean source)
theorem lower_jet_holder_of_next_bound
(j : ℕ) (α a d B : ℝ) (hα : 0 < α) (hα1 : α ≤ 1)
(hd : 0 < d) (hB : 0 ≤ B) (f : ℝ → ℝ)
(hf : ContDiffOn ℝ (j + 1) f (Icc a (a + d)))
(hbound : ∀ t ∈ Icc a (a + d),
|iteratedDerivWithin (j + 1) f (Icc a (a + d)) t| ≤ B) :
∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin j f (Icc a (a + d)) x -
iteratedDerivWithin j f (Icc a (a + d)) y| ≤
(B * d ^ (1 - α)) * |x - y| ^ α := by
let s := Icc a (a + d)
have hu : UniqueDiffOn ℝ s := uniqueDiffOn_Icc (by linarith)
have hdiff : DifferentiableOn ℝ (iteratedDerivWithin j f s) s :=
hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr (lt_succ_self j)) hu
intro x hx y hy
have hmv : |iteratedDerivWithin j f s x - iteratedDerivWithin j f s y| ≤
B * |x - y| := by
have h := (convex_Icc a (a + d)).norm_image_sub_le_of_norm_derivWithin_le
hdiff (fun t ht => by
rw [← iteratedDerivWithin_succ, Real.norm_eq_abs]
exact hbound t ht) hy hx
simpa only [Real.norm_eq_abs] using h
have hxy : |x - y| ≤ d := by
rw [abs_le]
constructor <;> linarith [hx.1, hx.2, hy.1, hy.2]
have hnonneg : 0 ≤ |x - y| := abs_nonneg _
have hexp : 0 ≤ 1 - α := by linarith
have hpow : |x - y| ^ (1 - α) ≤ d ^ (1 - α) :=
Real.rpow_le_rpow hnonneg hxy hexp
have hfactor : |x - y| = |x - y| ^ α * |x - y| ^ (1 - α) := by
conv_lhs => rw [← Real.rpow_one |x - y|]
rw [← Real.rpow_add_of_nonneg hnonneg hα.le hexp]
congr 1
ring
calc
|iteratedDerivWithin j f s x - iteratedDerivWithin j f s y| ≤
B * |x - y| := hmv
_ = B * (|x - y| ^ α * |x - y| ^ (1 - α)) :=
congrArg (B * ·) hfactor
_ ≤ B * (|x - y| ^ α * d ^ (1 - α)) := by
gcongr
_ = (B * d ^ (1 - α)) * |x - y| ^ α := by ring
PrimitiveExp 1 core · 1 supporting Quantitative regularity of an interval primitive and of its survival-type exponential, using only a value bound and a top derivative Hölder bound for the integrand. ★ survival_holder_closure
Primitive and exponential closure on an interval
Quantitative regularity of an interval primitive and of its survival-type exponential, using only a value bound and a top derivative Hölder bound for the integrand. All constants are uniform under translation of the interval.
theorem survival_holder_closure reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, a Hölder exponent α with α positive and at most one, an interval length d that is positive, and a nonnegative value envelope M and a nonnegative Hölder constant L. Then there is one nonnegative constant B such that, for every interval from a to a + d and every integrand h that is k times continuously differentiable on it, bounded by M there, and whose k-th within-interval derivative is Hölder with constant L and exponent α there, the survival-type function exp(−∫ from a to t of h) is k times continuously differentiable on the interval, bounded by B there, and has k-th within-interval derivative Hölder with constant B and exponent α. The constant depends only on the order, exponent, length, and the two envelopes.
Formal statement
hypotheses
k :
ℕ
α d M L :
ℝ
hα :
0 < α
hα1 :
α ≤ 1
hd :
0 < d
hM :
0 ≤ M
hL :
0 ≤ L
conclusion
∃ B : ℝ,
0 ≤ B
conclusion 1
a :
ℝ
h :
ℝ → ℝ
ContDiffOn ℝ k h (Icc a (a + d))
(∀ x ∈ Icc a (a + d), |h x| ≤ M)
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k h (Icc a (a + d)) x - iteratedDerivWithin k h (Icc a (a + d)) y| ≤ L * |x - y| ^ α)
S :
fun t : ℝ => exp (-(∫ x in a..t, h x))
ContDiffOn ℝ k S (Icc a (a + d))
x ∈ Set.Icc a (a + d) :
|S x| ≤ B
x ∈ Set.Icc a (a + d) :
y ∈ Set.Icc a (a + d) :
|iteratedDerivWithin k S (Icc a (a + d)) x
- iteratedDerivWithin k S (Icc a (a + d)) y|
≤ B * |x - y| ^ α
Proof (Lean source)
theorem survival_holder_closure
(k : ℕ) (α d M L : ℝ) (hα : 0 < α) (hα1 : α ≤ 1)
(hd : 0 < d) (hM : 0 ≤ M) (hL : 0 ≤ L) :
∃ B : ℝ, 0 ≤ B ∧
∀ (a : ℝ) (h : ℝ → ℝ),
ContDiffOn ℝ k h (Icc a (a + d)) →
(∀ x ∈ Icc a (a + d), |h x| ≤ M) →
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k h (Icc a (a + d)) x -
iteratedDerivWithin k h (Icc a (a + d)) y| ≤
L * |x - y| ^ α) →
let S := fun t : ℝ => exp (-(∫ x in a..t, h x))
ContDiffOn ℝ k S (Icc a (a + d)) ∧
(∀ x ∈ Icc a (a + d), |S x| ≤ B) ∧
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k S (Icc a (a + d)) x -
iteratedDerivWithin k S (Icc a (a + d)) y| ≤
B * |x - y| ^ α) := by
/- First use `uniform_iteratedDerivWithin_bound` to bound the integrand's
whole jet, and use its value bound to bound the primitive and hence `S`.
`survival_jet_bound_of_integrand_jet_bound` then bounds `S` through order
`k+1`. Apply `lower_jet_holder_of_next_bound` at order `k`; this also
covers `k=0`. Differentiability follows from `interval_primitive_contDiffOn`
and composition with `exp`. -/
obtain ⟨C, hC, hjet⟩ :=
uniform_iteratedDerivWithin_bound k α d M L hα hd hM hL
obtain ⟨P, hP, hprim⟩ :=
primitive_quantitative_closure k α d M L hα hd hM hL
have hE : 0 ≤ exp P := (Real.exp_pos P).le
obtain ⟨J, hJ, hsurvjet⟩ :=
survival_jet_bound_of_integrand_jet_bound k d C (exp P) hd hC hE
refine ⟨Real.exp P + J * d ^ (1 - α),
add_nonneg hE (mul_nonneg hJ (Real.rpow_nonneg hd.le _)), ?_⟩
intro a h hh hval hholder
let s := Icc a (a + d)
let H := fun t : ℝ => ∫ x in a..t, h x
let S := fun t : ℝ => exp (-H t)
obtain ⟨hH, hHjet, _⟩ := hprim a h hh hval hholder
have hS : ContDiffOn ℝ (k + 1) S s := hH.neg.exp
have hSvalue : ∀ t ∈ s, |S t| ≤ exp P := by
intro t ht
have hHval := hHjet 0 (zero_le _) t ht
have hHabs : |H t| ≤ P := by simpa only [iteratedDerivWithin_zero] using hHval
have hneg : -H t ≤ P := by rcases abs_le.mp hHabs with ⟨hlo, _⟩; linarith
rw [abs_of_pos (Real.exp_pos _)]
exact Real.exp_le_exp.mpr hneg
have hSj : ∀ j ≤ k + 1, ∀ t ∈ s,
|iteratedDerivWithin j S s t| ≤ J :=
hsurvjet a h hh (hjet a h hh hval hholder) hSvalue
refine ⟨hS.of_le (by exact_mod_cast le_succ k), ?_, ?_⟩
· intro t ht
exact (hSvalue t ht).trans (le_add_of_nonneg_right
(mul_nonneg hJ (Real.rpow_nonneg hd.le _)))
· intro x hx y hy
have hhold := lower_jet_holder_of_next_bound k α a d J hα hα1 hd hJ S hS
(hSj (k + 1) le_rfl)
have hpow : 0 ≤ |x - y| ^ α := Real.rpow_nonneg (abs_nonneg _) _
calc
|iteratedDerivWithin k S s x - iteratedDerivWithin k S s y| ≤
(J * d ^ (1 - α)) * |x - y| ^ α := hhold x hx y hy
_ ≤ (exp P + J * d ^ (1 - α)) * |x - y| ^ α := by
exact mul_le_mul_of_nonneg_right (le_add_of_nonneg_left hE) hpow
1 supporting declaration (lemmas, instances)
-
primitive_quantitative_closuretheorem — Fix a derivative order k, a Hölder exponent α with α positive, an interval length d that is positive, and a nonnegative value envelope M and a nonnegative Hölder constant L. Then there is one nonnegative constant B such that, for every interval from a to a + d and every integrand h that is k times continuously differentiable on it, bounded by M there, and whose k-th within-interval derivative is Hölder with constant L and exponent α there, the primitive of h from a is k + 1 times continuously differentiable on the interval, all its within-interval derivatives up to order k + 1 are bounded by B there, and its (k + 1)-th within-interval derivative is Hölder with constant B and exponent α.hypothesesk :ℕα d M L :ℝhα :0 < αhd :0 < dhM :0 ≤ MhL :0 ≤ Lconclusion∃ B : ℝ,0 ≤ Bconclusion 1a :ℝh :ℝ → ℝContDiffOn ℝ k h (Icc a (a + d))(∀ x ∈ Icc a (a + d), |h x| ≤ M)(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k h (Icc a (a + d)) x - iteratedDerivWithin k h (Icc a (a + d)) y| ≤ L * |x - y| ^ α)H :fun t : ℝ => ∫ x in a..t, h xContDiffOn ℝ (k + 1) H (Icc a (a + d))j ≤ k + 1 :x ∈ Set.Icc a (a + d) :|iteratedDerivWithin j H (Icc a (a + d)) x| ≤ Bx ∈ Set.Icc a (a + d) :y ∈ Set.Icc a (a + d) :|iteratedDerivWithin (k + 1) H (Icc a (a + d)) x- iteratedDerivWithin (k + 1) H (Icc a (a + d)) y|≤ B * |x - y| ^ αProof (Lean source)
theorem primitive_quantitative_closure (k : ℕ) (α d M L : ℝ) (hα : 0 < α) (hd : 0 < d) (hM : 0 ≤ M) (hL : 0 ≤ L) : ∃ B : ℝ, 0 ≤ B ∧ ∀ (a : ℝ) (h : ℝ → ℝ), ContDiffOn ℝ k h (Icc a (a + d)) → (∀ x ∈ Icc a (a + d), |h x| ≤ M) → (∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k h (Icc a (a + d)) x - iteratedDerivWithin k h (Icc a (a + d)) y| ≤ L * |x - y| ^ α) → let H := fun t : ℝ => ∫ x in a..t, h x ContDiffOn ℝ (k + 1) H (Icc a (a + d)) ∧ (∀ j ≤ k + 1, ∀ x ∈ Icc a (a + d), |iteratedDerivWithin j H (Icc a (a + d)) x| ≤ B) ∧ (∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin (k + 1) H (Icc a (a + d)) x - iteratedDerivWithin (k + 1) H (Icc a (a + d)) y| ≤ B * |x - y| ^ α) := by obtain ⟨C, hC, hbound⟩ := uniform_iteratedDerivWithin_bound k α d M L hα hd hM hL refine ⟨d * M + C + L, by positivity, ?_⟩ intro a h hh hval hholder let s := Icc a (a + d) let H := fun t : ℝ => ∫ x in a..t, h x have hjet := interval_primitive_iteratedDerivWithin_succ k a d hd h hh have hCb := hbound a h hh hval hholder refine ⟨interval_primitive_contDiffOn k a d hd h hh, ?_, ?_⟩ · intro j hj x hx cases j with | zero => have hsub : ∀ t ∈ Set.uIoc a x, ‖h t‖ ≤ M := by intro t ht have ht' : t ∈ Ioc a x := by simpa [Set.uIoc_of_le hx.1] using ht simpa [Real.norm_eq_abs] using hval t ⟨ht'.1.le, ht'.2.trans hx.2⟩ have hi := intervalIntegral.norm_integral_le_of_norm_le_const hsub have hlen : |x - a| ≤ d := by rw [abs_of_nonneg (sub_nonneg.mpr hx.1)] linarith [hx.2] have hmul : M * |x - a| ≤ M * d := mul_le_mul_of_nonneg_left hlen hM simpa only [iteratedDerivWithin_zero, Real.norm_eq_abs] using (hi.trans (hmul.trans (by linarith [hC, hL]))) | succ j => have hjk : j ≤ k := by omega rw [hjet j hjk x hx] exact (hCb j hjk x hx).trans (by linarith [mul_nonneg hd.le hM, hL]) · intro x hx y hy rw [hjet k (le_refl k) x hx, hjet k (le_refl k) y hy] exact (hholder x hx y hy).trans (by have hp : 0 ≤ |x - y| ^ α := Real.rpow_nonneg (abs_nonneg _) _ nlinarith [mul_nonneg (add_nonneg (mul_nonneg hd.le hM) hC) hp])
PrimitiveJet 1 core · 2 supporting These identities isolate the fundamental theorem of calculus and its finite-order within-interval consequences, including both endpoints. ★ interval_primitive_contDiffOn
Within-interval jets of an interval primitive
These identities isolate the fundamental theorem of calculus and its finite-order within-interval consequences, including both endpoints.
theorem interval_primitive_contDiffOn reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
If an integrand h is k times continuously differentiable on the closed interval from a to a + d of positive length, then its primitive from a is k + 1 times continuously differentiable on that same interval.
Formal statement
hypotheses
conclusion
ContDiffOn ℝ (k + 1) (fun t : ℝ => ∫ x in a..t, h x) (Icc a (a + d))
Proof (Lean source)
theorem interval_primitive_contDiffOn
(k : ℕ) (a d : ℝ) (hd : 0 < d) (h : ℝ → ℝ)
(hh : ContDiffOn ℝ k h (Icc a (a + d))) :
ContDiffOn ℝ (k + 1) (fun t : ℝ => ∫ x in a..t, h x)
(Icc a (a + d)) := by
/- Use interval_primitive_derivWithin for the base derivative and the
local derivative characterization of ContDiffOn for the higher orders. -/
let s := Icc a (a + d)
let H := fun t : ℝ => ∫ x in a..t, h x
have hab : a < a + d := lt_add_of_pos_right a hd
have hcont : ContinuousOn h s := hh.continuousOn
have hdiff : DifferentiableOn ℝ H s := by
intro t ht
have : Fact (t ∈ s) := ⟨ht⟩
have hint : IntervalIntegrable h MeasureTheory.volume a t :=
(hcont.mono (by
intro x hx
exact ⟨hx.1, hx.2.trans ht.2⟩)).intervalIntegrable_of_Icc ht.1
have hmeas : StronglyMeasurableAtFilter h (nhdsWithin t s) :=
hcont.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc t
exact (intervalIntegral.integral_hasDerivWithinAt_right
(s := s) (t := s) hint hmeas (hcont t ht)).differentiableWithinAt
have hderiv : EqOn (derivWithin H s) h s :=
interval_primitive_derivWithin a d hd h (hh.of_le (by norm_num))
have hjet : ContDiffOn ℝ k (derivWithin H s) s :=
hh.congr (fun t ht => hderiv ht)
exact (contDiffOn_succ_iff_derivWithin (uniqueDiffOn_Icc hab)).2
⟨hdiff, by simp, hjet⟩
2 supporting declarations (lemmas, instances)
-
interval_primitive_derivWithintheorem — If an integrand h is continuous on the closed interval from a to a + d of positive length, then at every point t of the interval, endpoints included, the within-interval derivative of the primitive of h from a equals h(t).hypothesesconclusionderivWithin (fun u : ℝ => ∫ x in a..u, h x) (Icc a (a + d)) t = h tProof (Lean source)
theorem interval_primitive_derivWithin (a d : ℝ) (hd : 0 < d) (h : ℝ → ℝ) (hh : ContDiffOn ℝ 0 h (Icc a (a + d))) : ∀ t ∈ Icc a (a + d), derivWithin (fun u : ℝ => ∫ x in a..u, h x) (Icc a (a + d)) t = h t := by /- Apply the interval FTC at interior points and transfer the derivative identity to each endpoint through the one-sided within derivative. -/ have hab : a < a + d := lt_add_of_pos_right a hd have hcont : ContinuousOn h (Icc a (a + d)) := hh.continuousOn intro t ht have : Fact (t ∈ Icc a (a + d)) := ⟨ht⟩ have hint : IntervalIntegrable h MeasureTheory.volume a t := (hcont.mono (by intro x hx exact ⟨hx.1, hx.2.trans ht.2⟩)).intervalIntegrable_of_Icc ht.1 have hmeas : StronglyMeasurableAtFilter h (nhdsWithin t (Icc a (a + d))) := hcont.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc t exact (intervalIntegral.integral_hasDerivWithinAt_right (s := Icc a (a + d)) (t := Icc a (a + d)) hint hmeas (hcont t ht)).derivWithin ((uniqueDiffOn_Icc hab) t ht) -
interval_primitive_iteratedDerivWithin_succtheorem — If an integrand h is k times continuously differentiable on the closed interval from a to a + d of positive length, then for every order j at most k and every point t of the interval, endpoints included, the (j + 1)-th within-interval derivative of the primitive of h from a equals the j-th within-interval derivative of h.hypothesesk :ℕa d :ℝhd :0 < dh :ℝ → ℝhh :ContDiffOn ℝ k h (Icc a (a + d))j ≤ k :t ∈ Set.Icc a (a + d) :conclusioniteratedDerivWithin (j + 1) (fun u : ℝ => ∫ x in a..u, h x) (Icc a (a + d)) t= iteratedDerivWithin j h (Icc a (a + d)) tProof (Lean source)
theorem interval_primitive_iteratedDerivWithin_succ (k : ℕ) (a d : ℝ) (hd : 0 < d) (h : ℝ → ℝ) (hh : ContDiffOn ℝ k h (Icc a (a + d))) : ∀ j ≤ k, ∀ t ∈ Icc a (a + d), iteratedDerivWithin (j + 1) (fun u : ℝ => ∫ x in a..u, h x) (Icc a (a + d)) t = iteratedDerivWithin j h (Icc a (a + d)) t := by /- Rewrite the successor iterated derivative as the derivative of the preceding jet and use the base FTC identity inductively. -/ intro j hj t ht rw [iteratedDerivWithin_succ'] exact (iteratedDerivWithin_congr (n := j) (interval_primitive_derivWithin a d hd h (hh.of_le (by norm_num)))) ht
Product 1 core · 1 supporting The product estimate uses only the two factors' value and top-derivative Hölder bounds. ★ survival_product_holder_closure
Quantitative product closure for interval Hölder jets
The product estimate uses only the two factors' value and top-derivative Hölder bounds. A specialization covers an exponential primitive times a second Hölder-smooth function.
theorem survival_product_holder_closure reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, a Hölder exponent α with α positive and at most one, an interval length d that is positive, and nonnegative value envelopes Mh and Mg and Hölder constants Lh and Lg. Then there is one nonnegative constant B such that, for every interval from a to a + d and every integrand h and second factor g that are k times continuously differentiable on it, bounded there by Mh and Mg, and whose k-th within-interval derivatives are Hölder with exponent α and constants Lh and Lg there, the survival-weighted product t ↦ exp(−∫ from a to t of h)·g(t) is k times continuously differentiable on the interval, bounded by B there, and has k-th within-interval derivative Hölder with constant B and exponent α. No product seminorm is an input.
Formal statement
hypotheses
k :
ℕ
α d Mh Lh Mg Lg :
ℝ
hα :
0 < α
hα1 :
α ≤ 1
hd :
0 < d
hMh :
0 ≤ Mh
hLh :
0 ≤ Lh
hMg :
0 ≤ Mg
hLg :
0 ≤ Lg
conclusion
∃ B : ℝ,
0 ≤ B
conclusion 1
a :
ℝ
h g :
ℝ → ℝ
ContDiffOn ℝ k h (Icc a (a + d))
ContDiffOn ℝ k g (Icc a (a + d))
(∀ x ∈ Icc a (a + d), |h x| ≤ Mh)
(∀ x ∈ Icc a (a + d), |g x| ≤ Mg)
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k h (Icc a (a + d)) x - iteratedDerivWithin k h (Icc a (a + d)) y| ≤ Lh * |x - y| ^ α)
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k g (Icc a (a + d)) x - iteratedDerivWithin k g (Icc a (a + d)) y| ≤ Lg * |x - y| ^ α)
f :
fun t : ℝ => exp (-(∫ x in a..t, h x)) * g t
ContDiffOn ℝ k f (Icc a (a + d))
x ∈ Set.Icc a (a + d) :
|f x| ≤ B
x ∈ Set.Icc a (a + d) :
y ∈ Set.Icc a (a + d) :
|iteratedDerivWithin k f (Icc a (a + d)) x
- iteratedDerivWithin k f (Icc a (a + d)) y|
≤ B * |x - y| ^ α
Proof (Lean source)
theorem survival_product_holder_closure
(k : ℕ) (α d Mh Lh Mg Lg : ℝ)
(hα : 0 < α) (hα1 : α ≤ 1) (hd : 0 < d)
(hMh : 0 ≤ Mh) (hLh : 0 ≤ Lh) (hMg : 0 ≤ Mg) (hLg : 0 ≤ Lg) :
∃ B : ℝ, 0 ≤ B ∧
∀ (a : ℝ) (h g : ℝ → ℝ),
ContDiffOn ℝ k h (Icc a (a + d)) →
ContDiffOn ℝ k g (Icc a (a + d)) →
(∀ x ∈ Icc a (a + d), |h x| ≤ Mh) →
(∀ x ∈ Icc a (a + d), |g x| ≤ Mg) →
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k h (Icc a (a + d)) x -
iteratedDerivWithin k h (Icc a (a + d)) y| ≤
Lh * |x - y| ^ α) →
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k g (Icc a (a + d)) x -
iteratedDerivWithin k g (Icc a (a + d)) y| ≤
Lg * |x - y| ^ α) →
let f := fun t : ℝ => exp (-(∫ x in a..t, h x)) * g t
ContDiffOn ℝ k f (Icc a (a + d)) ∧
(∀ x ∈ Icc a (a + d), |f x| ≤ B) ∧
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k f (Icc a (a + d)) x -
iteratedDerivWithin k f (Icc a (a + d)) y| ≤
B * |x - y| ^ α) := by
/- Strategy: take the uniform constant from `survival_holder_closure`,
then feed its three conclusions and the assumptions on g into
`product_holder_closure`. -/
obtain ⟨Bs, hBs, hs⟩ :=
survival_holder_closure k α d Mh Lh hα hα1 hd hMh hLh
obtain ⟨B, hB, hp⟩ :=
product_holder_closure k α d Bs Bs Mg Lg
hα hα1 hd hBs hBs hMg hLg
refine ⟨B, hB, ?_⟩
intro a h g hh hg hMh' hMg' hLh' hLg'
obtain ⟨hSc, hSb, hSh⟩ := hs a h hh hMh' hLh'
exact hp a (fun t : ℝ => exp (-(∫ x in a..t, h x))) g
hSc hg hSb hMg' hSh hLg'
1 supporting declaration (lemmas, instances)
-
product_holder_closuretheorem — Fix a derivative order k, a Hölder exponent α with α positive and at most one, an interval length d that is positive, and nonnegative value envelopes Mf and Mg and Hölder constants Lf and Lg for two factors. Then there is one nonnegative constant B such that, for every interval from a to a + d and all functions f and g that are k times continuously differentiable on it, bounded there by Mf and Mg, and whose k-th within-interval derivatives are Hölder with exponent α and constants Lf and Lg there, the product f·g is k times continuously differentiable on the interval, bounded by B there, and has k-th within-interval derivative Hölder with constant B and exponent α.hypothesesk :ℕα d Mf Lf Mg Lg :ℝhα :0 < αhα1 :α ≤ 1hd :0 < dhMf :0 ≤ MfhLf :0 ≤ LfhMg :0 ≤ MghLg :0 ≤ Lgconclusion∃ B : ℝ,0 ≤ Bconclusion 1a :ℝf g :ℝ → ℝContDiffOn ℝ k f (Icc a (a + d))ContDiffOn ℝ k g (Icc a (a + d))(∀ x ∈ Icc a (a + d), |f x| ≤ Mf)(∀ x ∈ Icc a (a + d), |g x| ≤ Mg)(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x - iteratedDerivWithin k f (Icc a (a + d)) y| ≤ Lf * |x - y| ^ α)(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k g (Icc a (a + d)) x - iteratedDerivWithin k g (Icc a (a + d)) y| ≤ Lg * |x - y| ^ α)ContDiffOn ℝ k (fun t => f t * g t) (Icc a (a + d))x ∈ Set.Icc a (a + d) :|f x * g x| ≤ Bx ∈ Set.Icc a (a + d) :y ∈ Set.Icc a (a + d) :|iteratedDerivWithin k (fun t => f t * g t) (Icc a (a + d)) x- iteratedDerivWithin k (fun t => f t * g t) (Icc a (a + d)) y|≤ B * |x - y| ^ αProof (Lean source)
theorem product_holder_closure (k : ℕ) (α d Mf Lf Mg Lg : ℝ) (hα : 0 < α) (hα1 : α ≤ 1) (hd : 0 < d) (hMf : 0 ≤ Mf) (hLf : 0 ≤ Lf) (hMg : 0 ≤ Mg) (hLg : 0 ≤ Lg) : ∃ B : ℝ, 0 ≤ B ∧ ∀ (a : ℝ) (f g : ℝ → ℝ), ContDiffOn ℝ k f (Icc a (a + d)) → ContDiffOn ℝ k g (Icc a (a + d)) → (∀ x ∈ Icc a (a + d), |f x| ≤ Mf) → (∀ x ∈ Icc a (a + d), |g x| ≤ Mg) → (∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k f (Icc a (a + d)) x - iteratedDerivWithin k f (Icc a (a + d)) y| ≤ Lf * |x - y| ^ α) → (∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k g (Icc a (a + d)) x - iteratedDerivWithin k g (Icc a (a + d)) y| ≤ Lg * |x - y| ^ α) → ContDiffOn ℝ k (fun t => f t * g t) (Icc a (a + d)) ∧ (∀ x ∈ Icc a (a + d), |f x * g x| ≤ B) ∧ (∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k (fun t => f t * g t) (Icc a (a + d)) x - iteratedDerivWithin k (fun t => f t * g t) (Icc a (a + d)) y| ≤ B * |x - y| ^ α) := by obtain ⟨Cf, hCf, hCf_bound⟩ := uniform_iteratedDerivWithin_bound k α d Mf Lf hα hd hMf hLf obtain ⟨Cg, hCg, hCg_bound⟩ := uniform_iteratedDerivWithin_bound k α d Mg Lg hα hd hMg hLg let Hf := Lf + Cf * d ^ (1 - α) let Hg := Lg + Cg * d ^ (1 - α) have hHf : 0 ≤ Hf := by dsimp [Hf]; positivity have hHg : 0 ≤ Hg := by dsimp [Hg]; positivity have hLf_le : Lf ≤ Hf := by dsimp [Hf] exact le_add_of_nonneg_right (mul_nonneg hCf (Real.rpow_nonneg hd.le _)) have hCf_le : Cf * d ^ (1 - α) ≤ Hf := by dsimp [Hf] exact le_add_of_nonneg_left hLf have hLg_le : Lg ≤ Hg := by dsimp [Hg] exact le_add_of_nonneg_right (mul_nonneg hCg (Real.rpow_nonneg hd.le _)) have hCg_le : Cg * d ^ (1 - α) ≤ Hg := by dsimp [Hg] exact le_add_of_nonneg_left hLg let C := Cf * Hg + Cg * Hf have hC : 0 ≤ C := by dsimp [C]; positivity let B := Mf * Mg + ∑ i ∈ range (k + 1), (Nat.choose k i : ℝ) * C have hB : 0 ≤ B := by dsimp [B] apply add_nonneg (mul_nonneg hMf hMg) exact Finset.sum_nonneg fun i hi => mul_nonneg (Nat.cast_nonneg _) hC refine ⟨B, hB, ?_⟩ intro a f g hf hg hfv hgv hfh hgh let s := Icc a (a + d) have hu : UniqueDiffOn ℝ s := uniqueDiffOn_Icc (by linarith) have hfb := hCf_bound a f hf hfv hfh have hgb := hCg_bound a g hg hgv hgh have hfh_all (j : ℕ) (hj : j ≤ k) (x : ℝ) (hx : x ∈ s) (y : ℝ) (hy : y ∈ s) : |iteratedDerivWithin j f s x - iteratedDerivWithin j f s y| ≤ Hf * |x - y| ^ α := by by_cases hk0 : k = 0 · have hj0 : j = 0 := by omega subst k subst j exact (hfh x hx y hy).trans (mul_le_mul_of_nonneg_right hLf_le (Real.rpow_nonneg (abs_nonneg _) _)) by_cases heq : j = k · subst j exact (hfh x hx y hy).trans (mul_le_mul_of_nonneg_right hLf_le (Real.rpow_nonneg (abs_nonneg _) _)) · have hj1 : j + 1 ≤ k := by omega have h := lower_jet_holder_of_next_bound j α a d Cf hα hα1 hd hCf f (hf.of_le (by exact_mod_cast hj1)) (fun t ht => hfb (j + 1) hj1 t ht) x hx y hy exact h.trans (mul_le_mul_of_nonneg_right hCf_le (Real.rpow_nonneg (abs_nonneg _) _)) have hgh_all (j : ℕ) (hj : j ≤ k) (x : ℝ) (hx : x ∈ s) (y : ℝ) (hy : y ∈ s) : |iteratedDerivWithin j g s x - iteratedDerivWithin j g s y| ≤ Hg * |x - y| ^ α := by by_cases hk0 : k = 0 · have hj0 : j = 0 := by omega subst k subst j exact (hgh x hx y hy).trans (mul_le_mul_of_nonneg_right hLg_le (Real.rpow_nonneg (abs_nonneg _) _)) by_cases heq : j = k · subst j exact (hgh x hx y hy).trans (mul_le_mul_of_nonneg_right hLg_le (Real.rpow_nonneg (abs_nonneg _) _)) · have hj1 : j + 1 ≤ k := by omega have h := lower_jet_holder_of_next_bound j α a d Cg hα hα1 hd hCg g (hg.of_le (by exact_mod_cast hj1)) (fun t ht => hgb (j + 1) hj1 t ht) x hx y hy exact h.trans (mul_le_mul_of_nonneg_right hCg_le (Real.rpow_nonneg (abs_nonneg _) _)) refine ⟨hf.mul hg, ?_, ?_⟩ · intro x hx calc |f x * g x| = |f x| * |g x| := abs_mul _ _ _ ≤ Mf * Mg := mul_le_mul (hfv x hx) (hgv x hx) (abs_nonneg _) hMf _ ≤ B := by dsimp [B] exact le_add_of_nonneg_right (Finset.sum_nonneg fun i hi => mul_nonneg (Nat.cast_nonneg _) hC) · intro x hx y hy have hpow : 0 ≤ |x - y| ^ α := Real.rpow_nonneg (abs_nonneg _) _ have hterm (i : ℕ) (hi : i ∈ range (k + 1)) : |(Nat.choose k i : ℝ) * iteratedDerivWithin i f s x * iteratedDerivWithin (k - i) g s x - (Nat.choose k i : ℝ) * iteratedDerivWithin i f s y * iteratedDerivWithin (k - i) g s y| ≤ ((Nat.choose k i : ℝ) * C) * |x - y| ^ α := by have hik : i ≤ k := by have hi' := Finset.mem_range.mp hi omega have hki : k - i ≤ k := sub_le _ _ let u := iteratedDerivWithin i f s x let u' := iteratedDerivWithin i f s y let v := iteratedDerivWithin (k - i) g s x let v' := iteratedDerivWithin (k - i) g s y have huv : |u * v - u' * v'| ≤ C * |x - y| ^ α := by have heq : u * v - u' * v' = (u - u') * v + u' * (v - v') := by ring rw [heq] calc |(u - u') * v + u' * (v - v')| ≤ |u - u'| * |v| + |u'| * |v - v'| := by simpa only [abs_mul] using abs_add_le ((u - u') * v) (u' * (v - v')) _ ≤ (Hf * |x - y| ^ α) * Cg + Cf * (Hg * |x - y| ^ α) := by apply add_le_add · exact mul_le_mul (hfh_all i hik x hx y hy) (hgb (k - i) hki x hx) (abs_nonneg _) (mul_nonneg hHf hpow) · exact mul_le_mul (hfb i hik y hy) (hgh_all (k - i) hki x hx y hy) (abs_nonneg _) hCf _ = C * |x - y| ^ α := by dsimp [C]; ring have hc : 0 ≤ (Nat.choose k i : ℝ) := Nat.cast_nonneg _ calc _ = (Nat.choose k i : ℝ) * |u * v - u' * v'| := by have heq : (Nat.choose k i : ℝ) * iteratedDerivWithin i f s x * iteratedDerivWithin (k - i) g s x - (Nat.choose k i : ℝ) * iteratedDerivWithin i f s y * iteratedDerivWithin (k - i) g s y = (Nat.choose k i : ℝ) * (u * v - u' * v') := by dsimp [u, u', v, v']; ring rw [heq, abs_mul, abs_of_nonneg hc] _ ≤ (Nat.choose k i : ℝ) * (C * |x - y| ^ α) := mul_le_mul_of_nonneg_left huv hc _ = ((Nat.choose k i : ℝ) * C) * |x - y| ^ α := by ring have hsum : |(∑ i ∈ range (k + 1), (Nat.choose k i : ℝ) * iteratedDerivWithin i f s x * iteratedDerivWithin (k - i) g s x) - (∑ i ∈ range (k + 1), (Nat.choose k i : ℝ) * iteratedDerivWithin i f s y * iteratedDerivWithin (k - i) g s y)| ≤ (∑ i ∈ range (k + 1), (Nat.choose k i : ℝ) * C) * |x - y| ^ α := by rw [← Finset.sum_sub_distrib, Finset.sum_mul] exact (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum fun i hi => hterm i hi) change |iteratedDerivWithin k (f * g) s x - iteratedDerivWithin k (f * g) s y| ≤ B * |x - y| ^ α rw [iteratedDerivWithin_mul hx hu (hf x hx) (hg x hx), iteratedDerivWithin_mul hy hu (hf y hy) (hg y hy)] exact hsum.trans (mul_le_mul_of_nonneg_right (by dsimp [B]; exact le_add_of_nonneg_left (mul_nonneg hMf hMg)) hpow)
SurvivalDerivative 1 core · 1 supporting The survival-type exponential satisfies a first-order derivative identity on a nondegenerate closed interval, including both endpoints. ★ survival_iteratedDerivWithin_succ
First within derivative of an exponential primitive
The survival-type exponential satisfies a first-order derivative identity on a nondegenerate closed interval, including both endpoints.
theorem survival_iteratedDerivWithin_succ reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
If an integrand h is k times continuously differentiable on the closed interval from a to a + d of positive length, then for every order j at most k and every point t of the interval, the (j + 1)-th within-interval derivative of the survival function S(t) = exp(−∫ from a to t of h) equals minus the Leibniz sum over i from 0 to j of (j choose i) times the i-th within-interval derivative of h times the (j − i)-th within-interval derivative of S, as obtained from the differential equation S′ = −h·S.
Formal statement
hypotheses
k :
ℕ
a d :
ℝ
hd :
0 < d
h :
ℝ → ℝ
hh :
ContDiffOn ℝ k h (Icc a (a + d))
j ≤ k :
t ∈ Set.Icc a (a + d) :
conclusion
= -(∑ i ∈ range (j + 1), (Nat.choose j i : ℝ) * iteratedDerivWithin i h (Icc a (a + d)) t * iteratedDerivWithin (j - i) (fun u : ℝ => exp (-(∫ x in a..u, h x))) (Icc a (a + d)) t)
Proof (Lean source)
theorem survival_iteratedDerivWithin_succ
(k : ℕ) (a d : ℝ) (hd : 0 < d) (h : ℝ → ℝ)
(hh : ContDiffOn ℝ k h (Icc a (a + d))) :
∀ j ≤ k, ∀ t ∈ Icc a (a + d),
iteratedDerivWithin (j + 1)
(fun u : ℝ => exp (-(∫ x in a..u, h x)))
(Icc a (a + d)) t =
-(∑ i ∈ range (j + 1),
(Nat.choose j i : ℝ) *
iteratedDerivWithin i h (Icc a (a + d)) t *
iteratedDerivWithin (j - i)
(fun u : ℝ => exp (-(∫ x in a..u, h x)))
(Icc a (a + d)) t) := by
/- First identify S' with -h*S on the entire interval using
`survival_derivWithin`. Rewrite the successor derivative as the j-th
derivative of S', then use `iteratedDerivWithin_congr` and Mathlib's
`iteratedDerivWithin_mul`. The hypotheses supply C^j for both factors. -/
intro j hj t ht
let s := Icc a (a + d)
let S := fun u : ℝ => exp (-(∫ x in a..u, h x))
have hS : ContDiffOn ℝ j S s :=
((interval_primitive_contDiffOn k a d hd h hh).neg.exp).of_le (by
exact_mod_cast le_trans hj (le_succ k))
have hhj : ContDiffOn ℝ j h s := hh.of_le (by exact_mod_cast hj)
have hderiv : EqOn (derivWithin S s) (fun u => -(h u * S u)) s := by
intro u hu
simpa only [S, s, neg_mul] using
survival_derivWithin a d hd h (hh.of_le (by norm_num)) u hu
change iteratedDerivWithin (j + 1) S s t =
-(∑ i ∈ range (j + 1),
(Nat.choose j i : ℝ) * iteratedDerivWithin i h s t *
iteratedDerivWithin (j - i) S s t)
rw [iteratedDerivWithin_succ', (iteratedDerivWithin_congr (n := j) hderiv) ht]
rw [iteratedDerivWithin_fun_neg]
exact congrArg neg
(iteratedDerivWithin_mul ht (uniqueDiffOn_Icc (lt_add_of_pos_right a hd))
(hhj t ht) (hS t ht))
1 supporting declaration (lemmas, instances)
-
survival_derivWithintheorem — If an integrand h is continuous on the closed interval from a to a + d of positive length, then at every point t of the interval, endpoints included, the within-interval derivative of the survival function exp(−∫ from a to t of h) equals −h(t) times that survival function at t.hypothesesconclusion= -h t * exp (-(∫ x in a..t, h x))Proof (Lean source)
theorem survival_derivWithin (a d : ℝ) (hd : 0 < d) (h : ℝ → ℝ) (hh : ContDiffOn ℝ 0 h (Icc a (a + d))) : ∀ t ∈ Icc a (a + d), derivWithin (fun u : ℝ => exp (-(∫ x in a..u, h x))) (Icc a (a + d)) t = -h t * exp (-(∫ x in a..t, h x)) := by /- Combine interval_primitive_derivWithin with the within-set chain rule for negation and Real.exp. -/ intro t ht let s := Icc a (a + d) let H := fun u : ℝ => ∫ x in a..u, h x have hHdiff : DifferentiableWithinAt ℝ H s t := (interval_primitive_contDiffOn 0 a d hd h hh).differentiableOn (by norm_num) t ht have hHderiv : derivWithin H s t = h t := interval_primitive_derivWithin a d hd h hh t ht have hHas : HasDerivWithinAt H (h t) s t := by simpa [hHderiv] using hHdiff.hasDerivWithinAt have hsurv := hHas.neg.exp.derivWithin ((uniqueDiffOn_Icc (lt_add_of_pos_right a hd)) t ht) simpa [H, s, mul_comm] using hsurv
SurvivalJetBound 1 core · 0 supporting The differential equation for an exponential primitive bounds each derivative from lower derivatives. ★ survival_jet_bound_of_integrand_jet_bound
Uniform jet bounds for an exponential interval primitive
The differential equation for an exponential primitive bounds each derivative from lower derivatives. This module isolates the finite recurrence from the Hölder argument in the survival closure theorem.
theorem survival_jet_bound_of_integrand_jet_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, an interval length d that is positive, a nonnegative derivative envelope C and a nonnegative value envelope E. Then there is one nonnegative constant B such that, for every interval from a to a + d and every integrand h that is k times continuously differentiable on it, whose within-interval derivatives of every order at most k are bounded by C there, and whose survival-type function exp(−∫ from a to t of h) is bounded by E there, every within-interval derivative of that survival-type function of order at most k + 1 is bounded by B on the whole interval. The constant does not depend on the interval location or on the integrand.
Formal statement
hypotheses
k :
ℕ
d C E :
ℝ
hd :
0 < d
hC :
0 ≤ C
hE :
0 ≤ E
conclusion
∃ B : ℝ,
0 ≤ B
conclusion 1
≤ B
Proof (Lean source)
theorem survival_jet_bound_of_integrand_jet_bound
(k : ℕ) (d C E : ℝ) (hd : 0 < d) (hC : 0 ≤ C) (hE : 0 ≤ E) :
∃ B : ℝ, 0 ≤ B ∧
∀ (a : ℝ) (h : ℝ → ℝ),
ContDiffOn ℝ k h (Icc a (a + d)) →
(∀ j ≤ k, ∀ t ∈ Icc a (a + d),
|iteratedDerivWithin j h (Icc a (a + d)) t| ≤ C) →
(∀ t ∈ Icc a (a + d),
|exp (-(∫ x in a..t, h x))| ≤ E) →
∀ j ≤ k + 1, ∀ t ∈ Icc a (a + d),
|iteratedDerivWithin j
(fun u : ℝ => exp (-(∫ x in a..u, h x)))
(Icc a (a + d)) t| ≤ B := by
let B : ℕ → ℝ := Nat.rec E (fun n b =>
b + ∑ i ∈ range (n + 1), (Nat.choose n i : ℝ) * C * b)
have hBzero : B 0 = E := rfl
have hBstep (n : ℕ) : B (n + 1) =
B n + ∑ i ∈ range (n + 1), (Nat.choose n i : ℝ) * C * B n := rfl
have hBnonneg : ∀ n, 0 ≤ B n := by
intro n
induction n with
| zero => simpa [hBzero] using hE
| succ n ih =>
rw [hBstep]
exact add_nonneg ih (Finset.sum_nonneg fun i hi => by positivity)
have hBmono (n : ℕ) : B n ≤ B (n + 1) := by
rw [hBstep]
exact le_add_of_nonneg_right (Finset.sum_nonneg fun i hi =>
mul_nonneg (mul_nonneg (Nat.cast_nonneg _) hC) (hBnonneg n))
refine ⟨B (k + 1), hBnonneg (k + 1), ?_⟩
intro a h hh hjet hvalue
let s := Icc a (a + d)
let S := fun u : ℝ => exp (-(∫ x in a..u, h x))
have hbound : ∀ n ≤ k + 1, ∀ j ≤ n, ∀ t ∈ s,
|iteratedDerivWithin j S s t| ≤ B n := by
intro n hn
induction n with
| zero =>
intro j hj t ht
have hj0 : j = 0 := by omega
subst j
simpa [S, s, hBzero] using hvalue t ht
| succ n ih =>
intro j hj t ht
by_cases hjn : j ≤ n
· exact (ih (by omega) j hjn t ht).trans (hBmono n)
· have hjeq : j = n + 1 := by omega
subst j
have hnk : n ≤ k := by omega
rw [survival_iteratedDerivWithin_succ k a d hd h hh n hnk t ht]
rw [abs_neg]
calc
|∑ i ∈ range (n + 1),
(Nat.choose n i : ℝ) * iteratedDerivWithin i h s t *
iteratedDerivWithin (n - i) S s t| ≤
∑ i ∈ range (n + 1),
|(Nat.choose n i : ℝ) * iteratedDerivWithin i h s t *
iteratedDerivWithin (n - i) S s t| :=
Finset.abs_sum_le_sum_abs _ _
_ ≤ ∑ i ∈ range (n + 1),
(Nat.choose n i : ℝ) * C * B n := by
apply Finset.sum_le_sum
intro i hi
have hin : i ≤ n := by have := Finset.mem_range.mp hi; omega
have hhi := hjet i (hin.trans hnk) t ht
have hSi := ih (by omega) (n - i) (sub_le _ _) t ht
rw [abs_mul, abs_mul, abs_of_nonneg (Nat.cast_nonneg _)]
calc
(Nat.choose n i : ℝ) * |iteratedDerivWithin i h s t| *
|iteratedDerivWithin (n - i) S s t| =
(Nat.choose n i : ℝ) *
(|iteratedDerivWithin i h s t| *
|iteratedDerivWithin (n - i) S s t|) := by ring
_ ≤ (Nat.choose n i : ℝ) * (C * B n) :=
mul_le_mul_of_nonneg_left
(mul_le_mul hhi hSi (abs_nonneg _) hC) (Nat.cast_nonneg _)
_ = (Nat.choose n i : ℝ) * C * B n := by ring
_ ≤ B (n + 1) := by rw [hBstep]; exact le_add_of_nonneg_left (hBnonneg n)
exact hbound (k + 1) le_rfl
SurvivalTaylor 1 core · 1 supporting For functions h and g that are k times continuously differentiable on an interval, bounded there, and whose k-th derivatives are Hölder with exponent α ∈ (0, 1], the survival-weighted product t ↦ exp(−∫_a^t h)·g(t) is ap ★ survival_product_endpoint_taylor
Endpoint Taylor expansion of exp(−∫h)·g with a uniform constant
For functions h and g that are k times continuously differentiable on an interval, bounded there, and whose k-th derivatives are Hölder with exponent α ∈ (0, 1], the survival-weighted product t ↦ exp(−∫_a^t h)·g(t) is approximated by a polynomial of degree at most k in the distance to the right endpoint b, with error at most C·(b − t)^(k + α) on the whole interval. The constant C depends only on k, α, the interval length and the sup and Hölder bounds on h and g, not on the functions themselves. The functional form is that of a survival function (the exponential of minus a cumulative hazard) times a second factor.
Main results
* survival_product_endpoint_taylor — the expansion on [a, a + d], with C also independent of
the location a of the interval.
* survival_product_endpoint_taylor_Icc — the same statement on a fixed interval [a, b].
theorem survival_product_endpoint_taylor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.HolderTaylor
Fix a derivative order k, a Hölder exponent α with α positive and at most one, an interval length d that is positive, and nonnegative value envelopes Mh and Mg and Hölder constants Lh and Lg. Then there is one nonnegative constant C such that, for every interval from a to a + d and every integrand h and second factor g that are k times continuously differentiable on it, bounded there by Mh and Mg, and whose k-th within-interval derivatives are Hölder with exponent α and constants Lh and Lg there, the survival-weighted product exp(−∫ from a to t of h)·g(t) has a polynomial of degree at most k in the distance a + d − t to the right endpoint whose error at every point t of the interval is at most C times that distance to the power k + α. The constant depends only on the shared input bounds and interval length, not on the functions or interval location.
Formal statement
hypotheses
k :
ℕ
α d Mh Lh Mg Lg :
ℝ
hα :
0 < α
hα1 :
α ≤ 1
hd :
0 < d
hMh :
0 ≤ Mh
hLh :
0 ≤ Lh
hMg :
0 ≤ Mg
hLg :
0 ≤ Lg
conclusion
∃ C : ℝ,
0 ≤ C
conclusion 1
a :
ℝ
h g :
ℝ → ℝ
ContDiffOn ℝ k h (Icc a (a + d))
ContDiffOn ℝ k g (Icc a (a + d))
(∀ x ∈ Icc a (a + d), |h x| ≤ Mh)
(∀ x ∈ Icc a (a + d), |g x| ≤ Mg)
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k h (Icc a (a + d)) x - iteratedDerivWithin k h (Icc a (a + d)) y| ≤ Lh * |x - y| ^ α)
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d), |iteratedDerivWithin k g (Icc a (a + d)) x - iteratedDerivWithin k g (Icc a (a + d)) y| ≤ Lg * |x - y| ^ α)
Proof (Lean source)
theorem survival_product_endpoint_taylor
(k : ℕ) (α d Mh Lh Mg Lg : ℝ)
(hα : 0 < α) (hα1 : α ≤ 1) (hd : 0 < d)
(hMh : 0 ≤ Mh) (hLh : 0 ≤ Lh) (hMg : 0 ≤ Mg) (hLg : 0 ≤ Lg) :
∃ C : ℝ, 0 ≤ C ∧
∀ (a : ℝ) (h g : ℝ → ℝ),
ContDiffOn ℝ k h (Icc a (a + d)) →
ContDiffOn ℝ k g (Icc a (a + d)) →
(∀ x ∈ Icc a (a + d), |h x| ≤ Mh) →
(∀ x ∈ Icc a (a + d), |g x| ≤ Mg) →
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k h (Icc a (a + d)) x -
iteratedDerivWithin k h (Icc a (a + d)) y| ≤
Lh * |x - y| ^ α) →
(∀ x ∈ Icc a (a + d), ∀ y ∈ Icc a (a + d),
|iteratedDerivWithin k g (Icc a (a + d)) x -
iteratedDerivWithin k g (Icc a (a + d)) y| ≤
Lg * |x - y| ^ α) →
∃ coeff : Fin (k + 1) → ℝ,
∀ t ∈ Icc a (a + d),
|exp (-(∫ x in a..t, h x)) * g t -
∑ j : Fin (k + 1), coeff j * (a + d - t) ^ j.val| ≤
C * (a + d - t) ^ ((k : ℝ) + α) := by
/- Strategy: obtain the product's `ContDiffOn` and top Hölder bound from
`survival_product_holder_closure`, then apply `endpoint_holder_taylor`.
The resulting coefficients can be chosen from the endpoint within jet. -/
obtain ⟨B, hB, hclosure⟩ :=
survival_product_holder_closure k α d Mh Lh Mg Lg
hα hα1 hd hMh hLh hMg hLg
obtain ⟨C, hC, htaylor⟩ :=
endpoint_holder_taylor k α d B hα hd hB
refine ⟨C, hC, ?_⟩
intro a h g hh hg hMh' hMg' hLh' hLg'
obtain ⟨hfc, _, hfh⟩ :=
hclosure a h g hh hg hMh' hMg' hLh' hLg'
exact htaylor a (fun t : ℝ => exp (-(∫ x in a..t, h x)) * g t) hfc hfh
1 supporting declaration (lemmas, instances)
-
survival_product_endpoint_taylor_Icctheorem — Fix a derivative order k, a Hölder exponent α with α positive and at most one, endpoints a and b with a < b, and nonnegative value envelopes Mh and Mg and Hölder constants Lh and Lg. Then there is one nonnegative constant C such that, for every integrand h and second factor g that are k times continuously differentiable on the interval from a to b, bounded there by Mh and Mg, and whose k-th within-interval derivatives are Hölder with exponent α and constants Lh and Lg there, the survival-weighted product exp(−∫ from a to t of h)·g(t) has a polynomial of degree at most k in b − t whose error at every point t of the interval is at most C·(b − t)^(k + α). No product seminorm is an input.hypothesesk :ℕα a b Mh Lh Mg Lg :ℝhα :0 < αhα1 :α ≤ 1hab :a < bhMh :0 ≤ MhhLh :0 ≤ LhhMg :0 ≤ MghLg :0 ≤ Lgconclusion∃ C : ℝ,0 ≤ Cconclusion 1h g :ℝ → ℝContDiffOn ℝ k h (Icc a b)ContDiffOn ℝ k g (Icc a b)(∀ x ∈ Icc a b, |h x| ≤ Mh)(∀ x ∈ Icc a b, |g x| ≤ Mg)(∀ x ∈ Icc a b, ∀ y ∈ Icc a b, |iteratedDerivWithin k h (Icc a b) x - iteratedDerivWithin k h (Icc a b) y| ≤ Lh * |x - y| ^ α)(∀ x ∈ Icc a b, ∀ y ∈ Icc a b, |iteratedDerivWithin k g (Icc a b) x - iteratedDerivWithin k g (Icc a b) y| ≤ Lg * |x - y| ^ α)Proof (Lean source)
theorem survival_product_endpoint_taylor_Icc (k : ℕ) (α a b Mh Lh Mg Lg : ℝ) (hα : 0 < α) (hα1 : α ≤ 1) (hab : a < b) (hMh : 0 ≤ Mh) (hLh : 0 ≤ Lh) (hMg : 0 ≤ Mg) (hLg : 0 ≤ Lg) : ∃ C : ℝ, 0 ≤ C ∧ ∀ (h g : ℝ → ℝ), ContDiffOn ℝ k h (Icc a b) → ContDiffOn ℝ k g (Icc a b) → (∀ x ∈ Icc a b, |h x| ≤ Mh) → (∀ x ∈ Icc a b, |g x| ≤ Mg) → (∀ x ∈ Icc a b, ∀ y ∈ Icc a b, |iteratedDerivWithin k h (Icc a b) x - iteratedDerivWithin k h (Icc a b) y| ≤ Lh * |x - y| ^ α) → (∀ x ∈ Icc a b, ∀ y ∈ Icc a b, |iteratedDerivWithin k g (Icc a b) x - iteratedDerivWithin k g (Icc a b) y| ≤ Lg * |x - y| ^ α) → ∃ coeff : Fin (k + 1) → ℝ, ∀ t ∈ Icc a b, |exp (-(∫ x in a..t, h x)) * g t - ∑ j : Fin (k + 1), coeff j * (b - t) ^ j.val| ≤ C * (b - t) ^ ((k : ℝ) + α) := by obtain ⟨C, hC, hbound⟩ := survival_product_endpoint_taylor k α (b - a) Mh Lh Mg Lg hα hα1 (sub_pos.mpr hab) hMh hLh hMg hLg refine ⟨C, hC, ?_⟩ intro h g hh hg hMh' hMg' hLh' hLg' have heq : a + (b - a) = b := by ring simpa [heq] using (hbound a h g (by simpa [heq] using hh) (by simpa [heq] using hg) (by simpa [heq] using hMh') (by simpa [heq] using hMg') (by simpa [heq] using hLh') (by simpa [heq] using hLg'))
Within 1 core · 1 supporting holder_taylor_remainder_within is the counterpart of holder_taylor_remainder for a function that is p times continuously differentiable on a closed interval only, with p-th within-interval derivative Hölder of order β − ★ holder_taylor_remainder_within
Hölder–Taylor remainder for a function smooth only on an interval
holder_taylor_remainder_within is the counterpart of holder_taylor_remainder for a function
that is p times continuously differentiable on a closed interval only, with p-th
within-interval derivative Hölder of order β − p: its within-interval Taylor polynomial at a
point t of the interval has error at most (M / p!) |a − t|^β at every point a of the
interval. The proof applies the Lagrange form of the remainder on the segment between t and
a and identifies the derivatives within that segment with those within the interval.
theorem holder_taylor_remainder_within reviewed
⚑ flagged
Causalean.Mathlib.Analysis.HolderTaylor
Hölder–Taylor remainder for a function that is smooth only on an interval. Let p be the largest integer strictly below the smoothness index β. If β is positive, the Hölder constant M is nonnegative, the expansion point t and the evaluation point a lie in an interval [lo, hi], f is p times continuously differentiable on that interval, and its p-th derivative within the interval is (β − p)-Hölder there with constant M, then the degree-p Taylor polynomial of f at t, built from derivatives within the interval, approximates f(a) with error at most (M / p!) · |a − t|^β.
Formal statement
hypotheses
f :
ℝ → ℝ
M β lo hi t a :
ℝ
hβ :
0 < β
hM :
0 ≤ M
ht :
t ∈ Icc lo hi
ha :
a ∈ Icc lo hi
hf :
hb :
conclusion
≤ M / ((holderDerivOrder β)).factorial * |a - t| ^ β
Proof (Lean source)
theorem holder_taylor_remainder_within {f : ℝ → ℝ} {M β lo hi t a : ℝ}
(hβ : 0 < β) (hM : 0 ≤ M)
(ht : t ∈ Icc lo hi) (ha : a ∈ Icc lo hi)
(hf : ContDiffOn ℝ (holderDerivOrder β) f (Icc lo hi))
(hb : ∀ x ∈ Icc lo hi, ∀ y ∈ Icc lo hi,
|iteratedDerivWithin (holderDerivOrder β) f (Icc lo hi) x -
iteratedDerivWithin (holderDerivOrder β) f (Icc lo hi) y|
≤ M * |x - y| ^ (β - ((holderDerivOrder β) : ℝ))) :
|f a - taylorWithinEval f (holderDerivOrder β) (Icc lo hi) t a|
≤ M / ((holderDerivOrder β)).factorial * |a - t| ^ β := by
rcases eq_or_ne a t with rfl | hne
· rw [taylorWithinEval_self, sub_self, abs_zero]
exact mul_nonneg (div_nonneg hM (by positivity)) (Real.rpow_nonneg (abs_nonneg _) _)
have hlt := (holderDerivOrder_lt hβ).le
generalize holderDerivOrder β = p at hf hb hlt ⊢
cases p with
| zero =>
have hbb := hb a ha t ht
simpa [taylor_within_zero_eval, iteratedDerivWithin_zero] using hbb
| succ n => exact holder_taylor_remainder_within_succ hM ht ha hf hb hlt hne
1 supporting declaration (lemmas, instances)
-
iteratedDerivWithin_eq_of_subsettheorem — Let a set s be contained in a set t, where s and t are sets within which derivatives are unique, and let f be n times continuously differentiable on t. Then at every point of s, the n-th derivative of f taken within s equals the one taken within t.hypothesesf :ℝ → ℝs t :Set ℝn :ℕx :ℝst :s ⊆ ths :UniqueDiffOn ℝ sht :UniqueDiffOn ℝ th :ContDiffOn ℝ n f thx :x ∈ sconclusioniteratedDerivWithin n f s x = iteratedDerivWithin n f t xProof (Lean source)
theorem iteratedDerivWithin_eq_of_subset {f : ℝ → ℝ} {s t : Set ℝ} {n : ℕ} {x : ℝ} (st : s ⊆ t) (hs : UniqueDiffOn ℝ s) (ht : UniqueDiffOn ℝ t) (h : ContDiffOn ℝ n f t) (hx : x ∈ s) : iteratedDerivWithin n f s x = iteratedDerivWithin n f t x := by rw [iteratedDerivWithin, iteratedDerivWithin, iteratedFDerivWithin_subset st hs ht h hx]