Mathlib.Analysis.Calculus

Calculus — Mathlib-shaped helpers: HolderTaylor.

Cube­Interpolation 64 core · 51 supporting · 33 submodules This package proves a finite-dimensional interpolation estimate on the normalized cube. Cube­Extension 121 core · 135 supporting · 75 submodules This package supplies extension-independent coordinate jets on closed finite-dimensional cubes, quantitative Hölder completion, affine transport, and controlled global extensions. Finite­Product 15 core · 20 supporting · 4 submodules This package gives explicit coordinate-specific Leibniz formulas, derivative certificates, support-visible decompositions, and elementary bounds for mixed jets of finite products of real-valued two-coordinate functions. Holder­Taylor 18 core · 17 supporting · 15 submodules Hölder–Taylor remainder bounds for approximating a smooth regression function near a target point by its degree-⌊β⌋ Taylor polynomial.
Rectangular­Remainder 2 core · 0 supporting This module gives a one-dimensional quadratic remainder bound with constant one half from explicit derivative witnesses and its iterated two-coordinate consequence. ★ quadratic_remainder_bound★ fourth_rectangular_remainder_bound

Rectangular derivative remainders

This module gives a one-dimensional quadratic remainder bound with constant one half from explicit derivative witnesses and its iterated two-coordinate consequence. The latter converts a uniform mixed fourth-derivative envelope into a rectangular fourth-order bound.

lemma quadratic_remainder_bound reviewed
Causalean.Mathlib.Analysis.Calculus

Let f be a real function with derivative f₁ and second derivative f₂ at every point of the interval from 0 to a nonnegative endpoint a. If f₂ is bounded in absolute value by B on that interval, and both f and f₁ vanish at 0, then the value of f at a is at most B·a²/2 in absolute value.

Formal statement
hypotheses
f f₁ f₂ :
ℝ → ℝ
a B :
ℝ
ha :
0 ≤ a
hf :
∀ x ∈ Icc 0 a, HasDerivAt f (f₁ x) x
hf₁ :
∀ x ∈ Icc 0 a, HasDerivAt f₁ (f₂ x) x
hf₂ :
∀ x ∈ Icc 0 a, |f₂ x| ≤ B
h0 :
f 0 = 0
h10 :
f₁ 0 = 0
conclusion
|f a| ≤ B*a^2/2
Proof (Lean source)
lemma quadratic_remainder_bound (f f₁ f₂ : ℝ → ℝ) (a B : ℝ) (ha : 0 ≤ a) (hf : ∀ x ∈ Icc 0 a, HasDerivAt f (f₁ x) x) (hf₁ : ∀ x ∈ Icc 0 a, HasDerivAt f₁ (f₂ x) x) (hf₂ : ∀ x ∈ Icc 0 a, |f₂ x| ≤ B) (h0 : f 0 = 0) (h10 : f₁ 0 = 0) : |f a| ≤ B*a^2/2 := by have hfirst (x : ℝ) (hx : x ∈ Icc 0 a) : |f₁ x| ≤ B*x := by have hm := Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (fun t ht => (hf₁ t ht).hasDerivWithinAt) (fun t ht => by simpa only [Real.norm_eq_abs] using hf₂ t ht) (convex_Icc 0 a) (left_mem_Icc.mpr ha) hx simpa only [Real.norm_eq_abs, h10, sub_zero, abs_of_nonneg hx.1] using hm have hderiv (s : ℝ) (hs : |s| = 1) (x : ℝ) (hx : x ∈ Icc 0 a) : HasDerivAt (fun t => B*t^2/2+s*f t) (B*x+s*f₁ x) x := by convert ((((hasDerivAt_id x).pow 2).const_mul B).div_const 2).add ((hf x hx).const_mul s) using 1 <;> first | rfl | (simp [id]; ring) have hmono (s : ℝ) (hs : |s| = 1) : MonotoneOn (fun t => B*t^2/2+s*f t) (Icc 0 a) := by apply monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc 0 a) · exact fun x hx => (hderiv s hs x hx).continuousAt.continuousWithinAt · intro x hx exact (hderiv s hs x (interior_subset hx)).hasDerivWithinAt · intro x hx have hbound := hfirst x (interior_subset hx) have habs : |s*f₁ x| ≤ B*x := by simpa only [abs_mul, hs, one_mul] using hbound linarith [(abs_le.mp habs).1] have hp := hmono 1 (by norm_num) (left_mem_Icc.mpr ha) (right_mem_Icc.mpr ha) ha have hn := hmono (-1) (by norm_num) (left_mem_Icc.mpr ha) (right_mem_Icc.mpr ha) ha simp only [h0, mul_zero, zero_pow (by decide : 2 ≠ 0), zero_div, add_zero, one_mul, neg_one_mul] at hp hn exact abs_le.mpr ⟨by linarith, by linarith⟩
Causalean.Mathlib.Analysis.Calculus.quadratic_remainder_bound · Causalean/Mathlib/Analysis/Calculus/RectangularRemainder.lean:23
lemma fourth_rectangular_remainder_bound reviewed
Causalean.Mathlib.Analysis.Calculus

Let F be a real function of two real variables and fix nonnegative amplitudes a and u. Suppose that, at the second argument u, F has partial derivative Fa in its first argument and Fa has partial derivative Faa in its first argument at every point of the interval from 0 to a; that on the rectangle 0 ≤ b ≤ a, 0 ≤ v ≤ u Faa has partial derivative FaaU in its second argument, FaaU has partial derivative FaaUU in its second argument, and FaaUU is bounded in absolute value by B; and that F and Fa vanish at the point (0, u), while Faa and FaaU vanish at (b, 0) for every b between 0 and a. Then the value of F at (a, u) is at most B·a²·u²/4 in absolute value.

Formal statement
hypotheses
F Fa Faa FaaU FaaUU :
ℝ → ℝ → ℝ
a u B :
ℝ
ha :
0 ≤ a
hu :
0 ≤ u
hFa :
∀ b ∈ Icc 0 a, HasDerivAt (fun t => F t u) (Fa b u) b
hFaa :
∀ b ∈ Icc 0 a, HasDerivAt (fun t => Fa t u) (Faa b u) b
hFaaU :
∀ b ∈ Icc 0 a, ∀ v ∈ Icc 0 u, HasDerivAt (Faa b) (FaaU b v) v
hFaaUU :
∀ b ∈ Icc 0 a, ∀ v ∈ Icc 0 u, HasDerivAt (FaaU b) (FaaUU b v) v
hbound :
∀ b ∈ Icc 0 a, ∀ v ∈ Icc 0 u, |FaaUU b v| ≤ B
hF0 :
F 0 u = 0
hFa0 :
Fa 0 u = 0
hFaa0 :
∀ b ∈ Icc 0 a, Faa b 0 = 0
hFaaU0 :
∀ b ∈ Icc 0 a, FaaU b 0 = 0
conclusion
|F a u| ≤ B*a^2*u^2/4
Proof (Lean source)
lemma fourth_rectangular_remainder_bound (F Fa Faa FaaU FaaUU : ℝ → ℝ → ℝ) (a u B : ℝ) (ha : 0 ≤ a) (hu : 0 ≤ u) (hFa : ∀ b ∈ Icc 0 a, HasDerivAt (fun t => F t u) (Fa b u) b) (hFaa : ∀ b ∈ Icc 0 a, HasDerivAt (fun t => Fa t u) (Faa b u) b) (hFaaU : ∀ b ∈ Icc 0 a, ∀ v ∈ Icc 0 u, HasDerivAt (Faa b) (FaaU b v) v) (hFaaUU : ∀ b ∈ Icc 0 a, ∀ v ∈ Icc 0 u, HasDerivAt (FaaU b) (FaaUU b v) v) (hbound : ∀ b ∈ Icc 0 a, ∀ v ∈ Icc 0 u, |FaaUU b v| ≤ B) (hF0 : F 0 u = 0) (hFa0 : Fa 0 u = 0) (hFaa0 : ∀ b ∈ Icc 0 a, Faa b 0 = 0) (hFaaU0 : ∀ b ∈ Icc 0 a, FaaU b 0 = 0) : |F a u| ≤ B*a^2*u^2/4 := by have hcurv (b : ℝ) (hb : b ∈ Icc 0 a) : |Faa b u| ≤ B*u^2/2 := quadratic_remainder_bound (Faa b) (FaaU b) (FaaUU b) u B hu (hFaaU b hb) (hFaaUU b hb) (hbound b hb) (hFaa0 b hb) (hFaaU0 b hb) have hr := quadratic_remainder_bound (fun b => F b u) (fun b => Fa b u) (fun b => Faa b u) a (B*u^2/2) ha hFa hFaa hcurv hF0 hFa0 calc _ ≤ (B*u^2/2)*a^2/2 := hr _ = _ := by ring
Causalean.Mathlib.Analysis.Calculus.fourth_rectangular_remainder_bound · Causalean/Mathlib/Analysis/Calculus/RectangularRemainder.lean:61