Mathlib.Analysis.Calculus.CubeInterpolation
This package proves a finite-dimensional interpolation estimate on the normalized cube.
Basic 6 core · 0 supporting This module defines coordinate partial derivatives and their fixed-cube bounds, using the ambient iterated Fréchet derivative convention needed by the paper adapter.
Coordinate Hölder data on a fixed cube
This module defines coordinate partial derivatives and their fixed-cube bounds, using the ambient iterated Fréchet derivative convention needed by the paper adapter.
abbrev cube reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
A finite dimension determines the closed normalized cube, whose coordinates lie between minus one and one.
Definition (Lean source)
def openCube reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
A finite dimension determines the open normalized cube, whose coordinates lie strictly between minus one and one.
def coordPartial reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
A finite dimension, derivative order, response, coordinate-direction sequence, and evaluation point determine the corresponding coordinate partial derivative, given by the order-j iterated derivative of the response at the point, taken in the whole space and applied to the standard basis vectors of the listed coordinate directions.
def TopHolder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension and derivative order, a Hölder exponent s and a constant L, and a real function of d variables, this is the top-order Hölder condition on the normalized cube: every coordinate partial derivative of order m, taken in the whole space, changes between any two points of the closed cube by at most L times their distance in the coordinatewise-maximum norm raised to the power s.
Definition (Lean source)
parameters
def
TopHolder d m s L u :
Prop
given by
|coordPartial m u f x - coordPartial m u f y| ≤ L * ‖x - y‖ ^ s
def DerivBound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension and derivative order, a radius R, and a real function of d variables, this is the uniform derivative bound on the normalized cube: every coordinate partial derivative of every order from zero up to m, taken in the whole space, is at most R in absolute value at every point of the closed cube.
Definition (Lean source)
structure HolderBall reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
A finite dimension, derivative order, Hölder exponent, radius, and response specify a fixed-cube Hölder ball through m-times continuous differentiability on the closed normalized cube, the bound R on every coordinate partial of order at most m at every point of the cube, and the top-order Hölder condition with exponent s and the same constant R on the order-m coordinate partials.
Definition (Lean source)
parameters
assumes
regularity :
ContDiffOn ℝ m u (cube d)
derivBound :
DerivBound d m R u
modulus :
TopHolder d m s R u
Multiindex 9 core · 6 supporting Natural count vectors, bounded-degree indices, and their sorted coordinate words. ★ coordinate_le_order
Finite coordinate multi-indices
Natural count vectors, bounded-degree indices, and their sorted coordinate words. The finite index type uses natural coordinates, so it can be identified directly with existing sorted-partial Taylor definitions. No function or polynomial representation is assumed in this combinatorial layer.
def multiOrder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The total order of a vector of coordinate counts is the sum of its entries.
Definition (Lean source)
def multiFactorial reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The multi-index factorial of a vector of coordinate counts is the product of the factorials of its entries.
abbrev MultiIndex reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension d and a degree bound m, this is the type of bounded-degree multi-indices: vectors of d natural-number counts whose total order is at most m.
Definition (Lean source)
theorem coordinate_le_order reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a vector of coordinate counts and any coordinate, the count at that coordinate is at most the vector's total order.
Formal statement
Proof (Lean source)
theorem coordinate_le_order {d : ℕ} (κ : Fin d → ℕ) (i : Fin d) :
κ i ≤ multiOrder κ := by
exact Finset.single_le_sum (fun j _ => zero_le (κ j)) (Finset.mem_univ i)
abbrev ExactIndex reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension d and an order k, this is the type of fixed-order multi-indices: vectors of d natural-number counts whose total order is exactly k.
Definition (Lean source)
def countList reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The increasing coordinate list of a vector of coordinate counts lists the coordinates in increasing order, repeating each one as many times as its count.
def sortedWord reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The sorted word of a vector of coordinate counts is the coordinate word, of length equal to the total order, whose entry at each position is the entry of the increasing coordinate list at that position.
Definition (Lean source)
def sortedWordOfOrder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The sorted word of fixed length k of a count vector whose total order is exactly k is its sorted word, with positions relabelled to run over the k positions.
Definition (Lean source)
def centeredMonomial reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The centred coordinate monomial for a centre a and a point x and a vector of coordinate counts is the product over coordinates of the difference between the coordinates of x and a, raised to that coordinate's count.
Definition (Lean source)
parameters
def
centeredMonomial a x κ :
ℝ
given by
∏ i, (x i - a i) ^ κ i
6 supporting declarations (lemmas, instances)
-
multiIndex_finiteinstance — For any dimension d and degree bound m, including dimension zero, there are only finitely many count vectors of total order at most m.parametersd m :ℕinstancegiven by=> ⟨κ.1 i, Nat.lt_succ_of_le ((coordinate_le_order κ.1 i).trans κ.2)⟩ apply Finite.of_injective encode intro κ κ' h apply Subtype.ext funext i exact congrArg val (congrFun h i) -
multiIndex_fintypeinstance — For any dimension d and degree bound m, this supplies a finite enumeration of the count vectors of total order at most m, so that sums over them make sense. -
exactIndex_finiteinstance — For any dimension d and order k, there are only finitely many count vectors of total order exactly k.parametersd k :ℕinstancegiven byby let encode : ExactIndex d k → MultiIndex d k := fun κ=> ⟨κ.1, κ.2.le⟩ apply Finite.of_injective encode intro κ κ' h exact Subtype.ext (congrArg (fun q : MultiIndex d k => q.1) h) -
exactIndex_fintypeinstance — For any dimension d and order k, this supplies a finite enumeration of the count vectors of total order exactly k, so that sums over them make sense. -
countList_lengththeorem — For a vector of coordinate counts, the length of its increasing coordinate list equals its total order.Proof (Lean source)
theorem countList_length {d : ℕ} (κ : Fin d → ℕ) : (countList κ).length = multiOrder κ := by simp [countList, List.length_flatten, List.sum_ofFn, multiOrder] -
multiFactorial_postheorem — For a vector of coordinate counts, its multi-index factorial is strictly positive.Proof (Lean source)
theorem multiFactorial_pos {d : ℕ} (κ : Fin d → ℕ) : 0 < multiFactorial κ := by exact Finset.prod_pos (fun i _ => Nat.factorial_pos (κ i))
Geometry 2 core · 4 supporting Arbitrary centers and side lengths are supported. ★ centeredCube_norm_sub_le
Geometry of centered Euclidean cubes
Arbitrary centers and side lengths are supported. Positive-side cubes have unique within derivatives and are closures of their interiors. The local Euclidean radius is bounded by sqrt(d) times half the side length. These geometric facts are independent of the Taylor and Legendre proof chains.
def centeredCube reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The closed coordinate cube with centre a and side length h is the set of points each of whose coordinates is within h / 2 of the matching coordinate of a.
Definition (Lean source)
parameters
def
given by
{x | ∀ i, |x i - a i| ≤ h / 2}
theorem centeredCube_norm_sub_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a centre a and a side length h that is nonnegative, every point of the cube is at Euclidean distance at most the square root of the dimension times h / 2 from the centre.
Formal statement
hypotheses
d :
ℕ
a :
EuclideanSpace ℝ (Fin d)
h :
ℝ
hh :
0 ≤ h
x :
EuclideanSpace ℝ (Fin d)
hx :
x ∈ centeredCube a h
conclusion
‖x - a‖ ≤ sqrt d * (h / 2)
Proof (Lean source)
theorem centeredCube_norm_sub_le {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
(h : ℝ) (hh : 0 ≤ h) {x : EuclideanSpace ℝ (Fin d)}
(hx : x ∈ centeredCube a h) : ‖x - a‖ ≤ sqrt d * (h / 2) := by
-- EuclideanSpace.norm_eq bounds the square sum coordinate by coordinate.
have hhalf : 0 ≤ h / 2 := by positivity
rw [EuclideanSpace.norm_eq]
calc
sqrt (∑ i, ‖(x - a) i‖ ^ 2) ≤ sqrt (∑ _ : Fin d, (h / 2) ^ 2) := by
apply Real.sqrt_le_sqrt
apply Finset.sum_le_sum
intro i _
rw [PiLp.sub_apply, Real.norm_eq_abs]
exact (sq_le_sq₀ (abs_nonneg _) hhalf).mpr (hx i)
_ = sqrt d * (h / 2) := by
simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
rw [Real.sqrt_mul (Nat.cast_nonneg d), Real.sqrt_sq hhalf]
4 supporting declarations (lemmas, instances)
-
centeredCube_convextheorem — For any centre and any side length, the centred coordinate cube is convex.Proof (Lean source)
theorem centeredCube_convex {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (h : ℝ) : Convex ℝ (centeredCube a h) := by intro x hx y hy u v hu hv huv i have hxi : x i ∈ Icc (a i - h / 2) (a i + h / 2) := by have hi := (abs_le.mp (hx i)) constructor <;> linarith have hyi : y i ∈ Icc (a i - h / 2) (a i + h / 2) := by have hi := (abs_le.mp (hy i)) constructor <;> linarith have hi := (convex_Icc (a i - h / 2) (a i + h / 2)) hxi hyi hu hv huv simp only [Set.mem_Icc, smul_eq_mul] at hi rw [PiLp.add_apply, PiLp.smul_apply, PiLp.smul_apply, smul_eq_mul, smul_eq_mul] apply abs_le.mpr constructor <;> linarith -
center_mem_interior_cubetheorem — For a centre and a side length that is positive, the centre lies in the interior of its cube.hypothesesconclusiona ∈ interior (centeredCube a h)Proof (Lean source)
theorem center_mem_interior_cube {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (h : ℝ) (hh : 0 < h) : a ∈ interior (centeredCube a h) := by -- Use the finite intersection of open coordinate intervals, including d=0. let U : Fin d → Set (EuclideanSpace ℝ (Fin d)) := fun i => (fun x => x i) ⁻¹' Ioo (a i - h / 2) (a i + h / 2) have hU : IsOpen (⋂ i, U i) := isOpen_iInter_of_finite fun i => isOpen_Ioo.preimage (PiLp.continuous_apply 2 (fun _ : Fin d => ℝ) i) have hsub : (⋂ i, U i) ⊆ centeredCube a h := by intro x hx i have hi : a i - h / 2 < x i ∧ x i < a i + h / 2 := Set.mem_iInter.mp hx i apply abs_le.mpr constructor <;> linarith apply interior_maximal hsub hU apply Set.mem_iInter.mpr intro i change a i - h / 2 < a i ∧ a i < a i + h / 2 constructor <;> linarith -
uniqueDiffOn_centeredCubetheorem — For a centre and a side length that is positive, derivatives taken within the cube are uniquely determined at every point of the cube.hypothesesconclusionUniqueDiffOn ℝ (centeredCube a h)Proof (Lean source)
theorem uniqueDiffOn_centeredCube {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (h : ℝ) (hh : 0 < h) : UniqueDiffOn ℝ (centeredCube a h) := by -- Apply uniqueDiffOn_convex using the preceding two geometry lemmas. exact uniqueDiffOn_convex (centeredCube_convex a h) ⟨a, center_mem_interior_cube a h hh⟩ -
centeredCube_subset_closure_interiortheorem — For a centre and a side length that is positive, every point of the cube lies in the closure of the cube's interior.hypothesesconclusionProof (Lean source)
theorem centeredCube_subset_closure_interior {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (h : ℝ) (hh : 0 < h) : centeredCube a h ⊆ closure (interior (centeredCube a h)) := by -- Contract a boundary point toward the center, or use convex topology. rw [(centeredCube_convex a h).closure_interior_eq_closure_of_nonempty_interior ⟨a, center_mem_interior_cube a h hh⟩] exact subset_closure
Counts 2 core · 0 supporting A list of coordinate directions of length m determines a multiindex of total degree m. ★ sum_coordCount
Counting coordinate directions
A list of coordinate directions of length m determines a multiindex of total
degree m. This translates between sequence and multiindex Hölder conventions.
def coordCount reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The multiplicity of coordinate i in a sequence of coordinate directions.
theorem sum_coordCount reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a sequence of m coordinate directions, the numbers of times each coordinate occurs in the sequence add up to m.
Formal statement
Proof (Lean source)
theorem sum_coordCount {d m : ℕ} (f : Fin m → Fin d) :
(∑ i : Fin d, coordCount f i) = m := by
classical
simpa only [coordCount, Finset.sum_card_fiberwise_eq_card_filter,
Finset.mem_univ, true_and, Finset.filter_true, Finset.card_fin]
using (Finset.sum_card_fiberwise_eq_card_filter
(Finset.univ : Finset (Fin m)) (Finset.univ : Finset (Fin d)) f)
AffineGeometry 3 core · 3 supporting The coordinatewise map x ↦ 2x-1 identifies the unit cube with the normalized cube and doubles distances in the finite-product norm. ★ cubeAffine_preimage_cube
Geometry of the affine map between fixed cubes
The coordinatewise map x ↦ 2x-1 identifies the unit cube with the normalized
cube and doubles distances in the finite-product norm.
def cubeAffine reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The coordinatewise affine map that sends a point x to the point whose every coordinate is 2x − 1; it carries the unit cube [0,1]^d onto the normalized cube [-1,1]^d.
def unitCube reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The unit cube consists of points whose coordinates lie in [0,1].
theorem cubeAffine_preimage_cube reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
In any dimension, the set of points that the affine map x ↦ 2x − 1 (applied to each coordinate) sends into the normalized cube is exactly the unit cube.
Formal statement
Proof (Lean source)
theorem cubeAffine_preimage_cube (d : ℕ) :
cubeAffine ⁻¹' cube d = unitCube d := by
ext x
constructor
· intro hx
apply Set.mem_univ_pi.mpr
intro i
have hi : cubeAffine x i ∈ Icc (-1 : ℝ) 1 := hx i
change -1 ≤ 2 * x i - 1 ∧ 2 * x i - 1 ≤ 1 at hi
constructor <;> linarith
· exact cubeAffine_mem_cube
3 supporting declarations (lemmas, instances)
-
cubeAffine_mem_cubetheorem — The affine image of each point of the unit cube lies in the normalized cube.Proof (Lean source)
theorem cubeAffine_mem_cube {d : ℕ} {x : Fin d → ℝ} (hx : x ∈ unitCube d) : cubeAffine x ∈ cube d := by intro i have hi : x i ∈ Icc (0 : ℝ) 1 := (Set.mem_univ_pi.mp hx) i change -1 ≤ 2 * x i - 1 ∧ 2 * x i - 1 ≤ 1 constructor <;> linarith [hi.1, hi.2] -
cubeAffine_norm_subtheorem — Affine transport doubles distances in the ambient finite-product norm.Proof (Lean source)
theorem cubeAffine_norm_sub {d : ℕ} (x y : Fin d → ℝ) : ‖cubeAffine x - cubeAffine y‖ = 2 * ‖x - y‖ := by have h : cubeAffine x - cubeAffine y = (2 : ℝ) • (x - y) := by ext i simp [cubeAffine, Pi.sub_apply, Pi.smul_apply, smul_eq_mul] ring rw [h, norm_smul] norm_num -
cubeAffine_contDifftheorem — The coordinatewise affine map is smooth to every finite order.Proof (Lean source)
theorem cubeAffine_contDiff {d m : ℕ} : ContDiff ℝ m (cubeAffine : (Fin d → ℝ) → (Fin d → ℝ)) := by unfold cubeAffine fun_prop
EuclideanJets 2 core · 1 supporting Arbitrary-order Euclidean within derivatives expand along coordinate words. ★ euclidean_within_jet_perm
Euclidean coordinate expansion and symmetry of within jets
Arbitrary-order Euclidean within derivatives expand along coordinate words. On uniquely differentiable sets, finite within smoothness and approach from the interior give permutation invariance. These analytic prerequisites use neither word-fiber cardinality nor Taylor polynomial grouping, allowing their proofs to be filled independently of the combinatorial and Legendre layers.
The coordinate expansion uses the multilinearity argument of CubeInterpolation.Directional.diagonal_derivative_coordinate_expansion. Permutation invariance reuses CubeExtension.ProductJetSymmetry through the continuous linear equivalence between Euclidean and ordinary Pi coordinates.
def wordPartialWithin reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The ordered coordinate partial of a function on its derivative domain along a word of coordinates at an evaluation point is the iterated derivative taken within the domain at that point, in the coordinate directions listed by the word.
Definition (Lean source)
parameters
def
wordPartialWithin S u w x :
ℝ
given by
iteratedFDerivWithin ℝ k u S x (fun r => single (w r) 1)
theorem euclidean_within_jet_perm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
If a function is k times continuously differentiable on a set on which derivatives are unique, then at a point of the set lying in the closure of the set's interior, the order-k derivative within the set is unchanged when its directions are reordered by any permutation of any k directions.
Formal statement
hypotheses
d k :
ℕ
huniq :
UniqueDiffOn ℝ S
u :
EuclideanSpace ℝ (Fin d) → ℝ
hu :
ContDiffOn ℝ k u S
a :
EuclideanSpace ℝ (Fin d)
ha :
a ∈ S
v :
conclusion
iteratedFDerivWithin ℝ k u S a (v ∘ σ) = iteratedFDerivWithin ℝ k u S a v
Proof (Lean source)
theorem euclidean_within_jet_perm {d k : ℕ}
{S : Set (EuclideanSpace ℝ (Fin d))} (huniq : UniqueDiffOn ℝ S)
{u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ k u S)
{a : EuclideanSpace ℝ (Fin d)} (ha : a ∈ S)
(hacl : a ∈ closure (interior S)) (σ : Perm (Fin k))
(v : Fin k → EuclideanSpace ℝ (Fin d)) :
iteratedFDerivWithin ℝ k u S a (v ∘ σ) = iteratedFDerivWithin ℝ k u S a v := by
-- Reuse ProductJetSymmetry.iteratedFDerivWithin_comp_perm_of_contDiffOn
-- across e = PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin d => ℝ).
-- ContinuousLinearEquiv.iteratedFDerivWithin_comp_right (ContDiff/Basic)
-- transports evaluations through e and needs no added smoothness.
-- Transport UniqueDiffOn and closure(interior S) through e.toHomeomorph;
-- apply the Pi-space theorem to u ∘ e.symm on e.symm ⁻¹' S.
-- Do not replace finite ContDiffOn regularity by analyticity or infinity.
let e := PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin d => ℝ)
have huniq' : UniqueDiffOn ℝ (e.symm ⁻¹' S) :=
e.symm.uniqueDiffOn_preimage_iff.mpr huniq
have hu' : ContDiffOn ℝ k (u ∘ e.symm) (e.symm ⁻¹' S) :=
e.symm.contDiffOn_comp_iff.mpr hu
have ha' : e a ∈ e.symm ⁻¹' S := by simpa using ha
have hacl' : e a ∈ closure (interior (e.symm ⁻¹' S)) := by
change e a ∈ closure (interior (e.symm.toHomeomorph ⁻¹' S))
rw [← e.symm.toHomeomorph.preimage_interior,
← e.symm.toHomeomorph.preimage_closure]
change e.symm (e a) ∈ closure (interior S)
simpa using hacl
have hperm := iteratedFDerivWithin_comp_perm_of_contDiffOn
huniq' hu' ha' hacl' σ (e ∘ v)
rw [e.symm.iteratedFDerivWithin_comp_right u huniq (by simpa using ha) k] at hperm
simpa [ContinuousMultilinearMap.compContinuousLinearMap_apply, Function.comp_def]
using hperm
1 supporting declaration (lemmas, instances)
-
within_diagonal_derivative_coordinate_expansiontheorem — For a function on its derivative domain and a point a and a direction z, the order-k derivative within the domain at a, taken k times in the direction z, equals the sum over all length-k coordinate words of the product of the matching coordinates of z times the ordered coordinate partial along that word at a.hypothesesconclusioniteratedFDerivWithin ℝ k u S a (fun _ => z)Proof (Lean source)
theorem within_diagonal_derivative_coordinate_expansion {d k : ℕ} (S : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ) (a z : EuclideanSpace ℝ (Fin d)) : iteratedFDerivWithin ℝ k u S a (fun _ => z) = ∑ w : Fin k → Fin d, (∏ r, z (w r)) * wordPartialWithin S u w a := by -- Directional.diagonal_derivative_coordinate_expansion gives the existing -- Pi-space argument. Here apply ContinuousMultilinearMap.map_sum and -- map_smul_univ directly to F = iteratedFDerivWithin; reconstruct z as -- the sum of single i (z i). This needs no regularity -- premise, since F is multilinear even when the derivative defaults to zero. classical let F := iteratedFDerivWithin ℝ k u S a have hz : (∑ i : Fin d, single i (z i)) = z := by apply (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin d => ℝ)).injective rw [map_sum] change (∑ i : Fin d, single i (z i)) = (fun i => z i) exact Finset.univ_sum_single _ calc F (fun _ => z) = F (fun _ => ∑ i : Fin d, single i (z i)) := by rw [hz] _ = ∑ w : Fin k → Fin d, F (fun r => single (w r) (z (w r))) := F.map_sum (fun _ i => single i (z i)) _ = ∑ w : Fin k → Fin d, (∏ r, z (w r)) * wordPartialWithin S u w a := by apply Finset.sum_congr rfl intro w _ have heq : (fun r => single (w r) (z (w r))) = (fun r => z (w r) • single (w r) (1 : ℝ)) := by funext r ext i simp [PiLp.single_apply] rw [heq, F.map_smul_univ] rfl
MultiindexTaylor 5 core · 3 supporting Coordinate derivatives use Euclidean coordinate vectors and iterated within-set Fréchet derivatives, so boundary values never presume a smooth ambient extension. ★ diagonal_taylor_eq_multiindex_taylor
Within-cube diagonal and sorted multi-index Taylor polynomials
Coordinate derivatives use Euclidean coordinate vectors and iterated within-set Fréchet derivatives, so boundary values never presume a smooth ambient extension. The algebraic conversion accepts permutation invariance; a separate lemma derives that invariance from within-cube regularity. Multinomial grouping is at arbitrary order, and the degree-two adapter later specializes it to orders zero, one, two.
def coordinatePartial reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The sorted coordinate partial of a function on its derivative domain for a vector of coordinate counts at an evaluation point is the ordered coordinate partial along the increasing word that repeats each coordinate as many times as its count.
Definition (Lean source)
parameters
def
coordinatePartial S u κ x :
ℝ
given by
wordPartialWithin S u (sortedWord κ) x
def diagonalTaylor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The diagonal Taylor polynomial of a function on its derivative domain of degree m with centre a, evaluated at x, is the sum over orders k from 0 to m of one over k factorial times the order-k derivative within the domain at a, taken k times in the direction x − a.
Definition (Lean source)
parameters
def
diagonalTaylor S u m a x :
ℝ
given by
∑ k ∈ range (m + 1), (k.factorial : ℝ)⁻¹ * iteratedFDerivWithin ℝ k u S a (fun _ => x - a)
def taylorCoefficient reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The sorted Taylor coefficient of a function on its derivative domain at a centre for a vector of coordinate counts of total order at most m is the sorted coordinate partial for those counts at the centre divided by the product of the factorials of the counts.
Definition (Lean source)
parameters
def
taylorCoefficient S u a κ :
ℝ
given by
coordinatePartial S u κ.1 a / (multiFactorial κ.1 : ℝ)
def multiindexTaylor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The multi-index Taylor polynomial of a function on its derivative domain of degree m with centre a, evaluated at x, is the sum over all count vectors of total order at most m of the sorted Taylor coefficient times the matching monomial in the coordinates of x − a.
Definition (Lean source)
parameters
def
multiindexTaylor S u m a x :
ℝ
given by
∑ κ : MultiIndex d m, taylorCoefficient S u a κ * centeredMonomial a x κ.1
theorem diagonal_taylor_eq_multiindex_taylor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a function on its derivative domain, a degree m, and a centre a and an evaluation point x, if for every order up to m the derivative within the domain at a is unchanged by reordering its directions, then the diagonal Taylor polynomial equals the multi-index Taylor polynomial.
Formal statement
hypotheses
d :
ℕ
S :
u :
EuclideanSpace ℝ (Fin d) → ℝ
m :
ℕ
a x :
EuclideanSpace ℝ (Fin d)
hsym :
∀ k ≤ m,
iteratedFDerivWithin ℝ k u S a (v ∘ σ) = iteratedFDerivWithin ℝ k u S a v
conclusion
diagonalTaylor S u m a x = multiindexTaylor S u m a x
Proof (Lean source)
theorem diagonal_taylor_eq_multiindex_taylor {d : ℕ}
(S : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ)
(m : ℕ) (a x : EuclideanSpace ℝ (Fin d))
(hsym : ∀ k ≤ m, ∀ (σ : Perm (Fin k))
(v : Fin k → EuclideanSpace ℝ (Fin d)),
iteratedFDerivWithin ℝ k u S a (v ∘ σ) = iteratedFDerivWithin ℝ k u S a v) :
diagonalTaylor S u m a x = multiindexTaylor S u m a x := by
-- At each order use the coordinate expansion, word_product_eq_count_product,
-- and group_word_sum_by_count. word_fiber_card_mul_factorial cancels k!;
-- combine the exact-order sums into the bounded-degree subtype sum.
-- For factorial cancellation, cast the multiplicative fiber identity to ℝ
-- and use positivity of both factorials. Do not cast natural division as
-- unrestricted real division. For sortedWordOfOrder, eliminate κ.2 before
-- comparing the cast-reindexed multilinear evaluation with coordinatePartial.
-- Group MultiIndex d m by its order in Fin (m+1) using sum_fiberwise;
-- each fiber is equivalent to ExactIndex d k.val. Fintype.sum_equiv
-- transports the fiber sum, and Fin.sum_univ_eq_sum_range restores range notation.
classical
have horder (k : ℕ) (hk : k ≤ m) :
(k.factorial : ℝ)⁻¹ * iteratedFDerivWithin ℝ k u S a (fun _ => x - a) =
∑ κ : ExactIndex d k,
coordinatePartial S u κ.1 a / (multiFactorial κ.1 : ℝ) *
centeredMonomial a x κ.1 := by
rw [within_diagonal_derivative_coordinate_expansion]
rw [group_word_sum_by_count (hF := by
intro v w hc
rw [word_product_eq_count_product v, word_product_eq_count_product w, hc,
wordPartialWithin_eq_of_count S u a (hsym k hk) v w hc])]
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro κ _
have hsorted : wordPartialWithin S u (sortedWordOfOrder κ) a =
coordinatePartial S u κ.1 a := by
rcases κ with ⟨κ, hκ⟩
subst k
rfl
have hcount : coordCount (sortedWordOfOrder κ) = κ.1 := by
rcases κ with ⟨κ, hκ⟩
subst k
exact sortedWord_count κ
rw [word_product_eq_count_product, hcount, hsorted]
have hf : ((wordFiber k κ.1).card : ℝ) * (multiFactorial κ.1 : ℝ) =
(k.factorial : ℝ) := by
exact_mod_cast word_fiber_card_mul_factorial κ.1 κ.2
have hkfac : (k.factorial : ℝ) ≠ 0 := by
exact_mod_cast Nat.factorial_ne_zero k
have hκfac : (multiFactorial κ.1 : ℝ) ≠ 0 := by
exact_mod_cast (multiFactorial_pos κ.1).ne'
have hcancel : (k.factorial : ℝ)⁻¹ *
((k.factorial / multiFactorial κ.1 : ℕ) : ℝ) =
(multiFactorial κ.1 : ℝ)⁻¹ := by
rw [← word_fiber_card_eq_multinomial κ.1 κ.2]
apply (mul_right_cancel₀ hκfac)
rw [mul_assoc, hf, inv_mul_cancel₀ hkfac, inv_mul_cancel₀ hκfac]
change (k.factorial : ℝ)⁻¹ *
(((k.factorial / multiFactorial κ.1 : ℕ) : ℝ) *
(centeredMonomial a x κ.1 * coordinatePartial S u κ.1 a)) = _
rw [← mul_assoc, hcancel]
simp only [div_eq_mul_inv]
ring
let order : MultiIndex d m → Fin (m + 1) :=
fun κ => ⟨multiOrder κ.1, Nat.lt_succ_of_le κ.2⟩
unfold diagonalTaylor multiindexTaylor
rw [← Fin.sum_univ_eq_sum_range]
rw [← Finset.sum_fiberwise univ order]
apply Finset.sum_congr rfl
intro k _
rw [horder k.val (le_of_lt_succ k.isLt)]
rw [Finset.sum_subtype (p := fun κ : MultiIndex d m => order κ = k)
(F := inferInstance)
(Finset.univ.filter fun κ => order κ = k) (by intro κ; simp)
(fun κ => taylorCoefficient S u a κ * centeredMonomial a x κ.1)]
let e : {κ : MultiIndex d m // order κ = k} ≃ ExactIndex d k.val :=
{ toFun := fun κ => ⟨κ.1.1, congrArg val κ.2⟩
invFun := fun κ =>
⟨⟨κ.1, κ.2.le.trans (le_of_lt_succ k.isLt)⟩,
by apply Fin.ext; exact κ.2⟩
left_inv := fun κ => by apply Subtype.ext; rfl
right_inv := fun κ => by rfl }
exact (Fintype.sum_equiv e _ _ (fun κ => by rfl)).symm
3 supporting declarations (lemmas, instances)
-
wordPartialWithin_eq_of_counttheorem — For a function on its derivative domain and a point at which the order-k derivative within the domain is unchanged by reordering its directions, two coordinate words of length k in which every coordinate occurs equally often give the same ordered coordinate partial at that point.hypothesesd k :ℕS :u :EuclideanSpace ℝ (Fin d) → ℝa :EuclideanSpace ℝ (Fin d)hsym :iteratedFDerivWithin ℝ k u S a (v ∘ σ) = iteratedFDerivWithin ℝ k u S a vhc :coordCount w = coordCount vconclusionwordPartialWithin S u w a = wordPartialWithin S u v aProof (Lean source)
theorem wordPartialWithin_eq_of_count {d k : ℕ} (S : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ) (a : EuclideanSpace ℝ (Fin d)) (hsym : ∀ (σ : Perm (Fin k)) (v : Fin k → EuclideanSpace ℝ (Fin d)), iteratedFDerivWithin ℝ k u S a (v ∘ σ) = iteratedFDerivWithin ℝ k u S a v) (w v : Fin k → Fin d) (hc : coordCount w = coordCount v) : wordPartialWithin S u w a = wordPartialWithin S u v a := by -- Use coordCount_eq_iff_perm, then evaluate hsym on coordinate directions. obtain ⟨σ, rfl⟩ := (coordCount_eq_iff_perm w v).mp hc simpa only [wordPartialWithin, Function.comp_def] using hsym σ (fun r => single (v r) 1) -
cube_diagonal_taylor_eq_multiindextheorem — For a cube with centre b and side length H that is positive, a function u that is m times continuously differentiable on the cube, and a centre a in the cube, the degree-m diagonal Taylor polynomial of u within the cube equals its degree-m multi-index Taylor polynomial at every evaluation point.hypothesesd m :ℕb a x :EuclideanSpace ℝ (Fin d)H :ℝhH :0 < Hu :EuclideanSpace ℝ (Fin d) → ℝhu :ContDiffOn ℝ m u (centeredCube b H)ha :a ∈ centeredCube b HconclusionProof (Lean source)
theorem cube_diagonal_taylor_eq_multiindex {d m : ℕ} (b a x : EuclideanSpace ℝ (Fin d)) (H : ℝ) (hH : 0 < H) (u : EuclideanSpace ℝ (Fin d) → ℝ) (hu : ContDiffOn ℝ m u (centeredCube b H)) (ha : a ∈ centeredCube b H) : diagonalTaylor (centeredCube b H) u m a x = multiindexTaylor (centeredCube b H) u m a x := by -- Apply the algebraic conversion using euclidean_within_jet_perm, -- uniqueDiffOn_centeredCube, and centeredCube_subset_closure_interior. apply diagonal_taylor_eq_multiindex_taylor intro k hk σ v exact euclidean_within_jet_perm (uniqueDiffOn_centeredCube b H hH) (hu.of_le (by exact_mod_cast hk)) ha (centeredCube_subset_closure_interior b H hH ha) σ v -
multiindexTaylor_centertheorem — For a function on its derivative domain, any degree, and any centre, the multi-index Taylor polynomial evaluated at its own centre equals the function's value there.hypothesesconclusionmultiindexTaylor S u m a a = u aProof (Lean source)
theorem multiindexTaylor_center {d : ℕ} (S : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ) (m : ℕ) (a : EuclideanSpace ℝ (Fin d)) : multiindexTaylor S u m a a = u a := by -- Every nonzero count vector gives a zero centered monomial; the zero -- vector contributes the order-zero within derivative, which is u a. classical let zeroIndex : MultiIndex d m := ⟨fun _ => 0, by simp [multiOrder]⟩ unfold multiindexTaylor rw [Finset.sum_eq_single zeroIndex] · have heval (k : ℕ) (hk : k = 0) (v : Fin k → EuclideanSpace ℝ (Fin d)) : iteratedFDerivWithin ℝ k u S a v = u a := by subst k exact iteratedFDerivWithin_zero_apply v have hp : coordinatePartial S u (fun _ => 0) a = u a := heval _ (by simp [multiOrder]) _ simp [taylorCoefficient, zeroIndex, hp, multiFactorial, centeredMonomial] · intro κ _ hκ have hpos : ∃ i, κ.1 i ≠ 0 := by by_contra h apply hκ apply Subtype.ext funext i simpa using not_exists.mp h i obtain ⟨i, hi⟩ := hpos have hz : centeredMonomial a a κ.1 = 0 := by apply Finset.prod_eq_zero (Finset.mem_univ i) simp [hi] rw [hz, mul_zero] · simp
TensorLegendre 5 core · 4 supporting The finite triangular inverse matrix realizes centered coordinate monomials and arbitrary polynomials of total degree at most two. ★ degree_two_monomial_scaledLegendre
Tensorized inverse Legendre realization
The finite triangular inverse matrix realizes centered coordinate monomials and arbitrary polynomials of total degree at most two. All coefficients are explicit finite sums. Natural powers of the cube side control every matrix entry; no coefficient bound or representation is a hypothesis.
def scaledTensorLegendre reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The scaled tensor Legendre entry for a centre a, a side length h, a multi-index, and a point x is the product over coordinates of the normalized Legendre entry whose degree is that coordinate's count, evaluated at the coordinate of x − a divided by h.
Definition (Lean source)
parameters
def
scaledTensorLegendre a h κ x :
ℝ
given by
∏ i, legendreEntry (κ.1 i) ((x i - a i) / h)
def inverseTensorCoeff reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The tensor inverse coefficient at scale h for an input and an output vector of coordinate degrees is the product over coordinates of the one-dimensional inverse Legendre entries for the matching pair of degrees.
Definition (Lean source)
theorem degree_two_monomial_scaledLegendre reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a degree bound m at most two, a centre a and a point x, a side length h that is positive, and a multi-index of total order at most m, the centred monomial with those exponents equals the sum, over all multi-indices of total order at most m, of the tensor inverse coefficient times the scaled tensor Legendre entry.
Formal statement
hypotheses
conclusion
centeredMonomial a x α.1
Proof (Lean source)
theorem degree_two_monomial_scaledLegendre {d m : ℕ} (hm : m ≤ 2)
(a x : EuclideanSpace ℝ (Fin d)) (h : ℝ) (hh : 0 < h)
(α : MultiIndex d m) :
centeredMonomial a x α.1 = ∑ β : MultiIndex d m,
inverseTensorCoeff h α.1 β.1 * scaledTensorLegendre a h β x := by
-- Substitute t=(x_i-a_i)/h into monomial_inverse_legendre, expand the
-- finite product of sums, and discard indices above α coordinatewise.
-- Triangularity proves total-degree preservation without any tensor box
-- relaxation of the index set. The identity holds for all x, not just a cube.
-- Mathlib Fintype.prod_sum expands the coordinate Fin 3 sums. Compare
-- the resulting Fin d → Fin 3 box with MultiIndex d m by zero-extension:
-- nonzero terms satisfy β≤α coordinatewise, hence multiOrder β≤m.
-- Preserve this total-degree restriction; the full box is not the API index.
classical
-- Embed the total-degree simplex into the coordinate box without enlarging the API.
let encode : MultiIndex d m → (Fin d → Fin 3) := fun β i =>
⟨β.1 i, by
have := (coordinate_le_order β.1 i).trans (β.2.trans hm)
omega⟩
have encode_inj : Injective encode := by
intro β γ he
apply Subtype.ext
funext i
exact congrArg val (congrFun he i)
let term : (Fin d → Fin 3) → ℝ := fun b =>
inverseTensorCoeff h α.1 (fun i => (b i).val) *
∏ i, legendreEntry (b i).val ((x i - a i) / h)
have outside (b : Fin d → Fin 3)
(hb : b ∉ Finset.univ.image encode) : term b = 0 := by
have hnot : ¬ ∀ i, (b i).val ≤ α.1 i := by
intro hle
have horder : multiOrder (fun i => (b i).val) ≤ m :=
(Finset.sum_le_sum (fun i _ => hle i)).trans α.2
let β : MultiIndex d m := ⟨fun i => (b i).val, horder⟩
apply hb
refine Finset.mem_image.mpr ⟨β, Finset.mem_univ _, ?_⟩
funext i
apply Fin.ext
rfl
simp only [term, inverseTensorCoeff_zero h α _ hnot, zero_mul]
calc
centeredMonomial a x α.1 =
∏ i, ∑ j : Fin 3, inverseEntry h (α.1 i) j.val *
legendreEntry j.val ((x i - a i) / h) := by
apply Finset.prod_congr rfl
intro i _
have hi := monomial_inverse_legendre (α.1 i)
((coordinate_le_order α.1 i).trans (α.2.trans hm)) h ((x i - a i) / h)
simpa only [mul_div_cancel₀ _ hh.ne'] using hi
_ = ∑ b : Fin d → Fin 3, ∏ i, inverseEntry h (α.1 i) (b i).val *
legendreEntry (b i).val ((x i - a i) / h) := Fintype.prod_sum _
_ = ∑ b : Fin d → Fin 3, term b := by
apply Finset.sum_congr rfl
intro b _
simp only [term, inverseTensorCoeff, Finset.prod_mul_distrib]
_ = ∑ b ∈ Finset.univ.image encode, term b := by
symm
exact Finset.sum_subset (Finset.subset_univ _)
(fun b _ hb => outside b hb)
_ = ∑ β : MultiIndex d m,
inverseTensorCoeff h α.1 β.1 * scaledTensorLegendre a h β x := by
rw [Finset.sum_image (fun β _ γ _ he => encode_inj he)]
rfl
def legendreCoefficients reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The Legendre coefficients at scale h of a vector of centred-monomial coefficients are given for each output multi-index by the sum over input multi-indices of the monomial coefficient times the tensor inverse coefficient.
Definition (Lean source)
def legendrePolynomial reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The scaled Legendre polynomial with centre a, side length h, and coefficient vector, evaluated at a point x, is the sum over multi-indices of the scaled tensor Legendre entry times its coefficient.
Definition (Lean source)
4 supporting declarations (lemmas, instances)
-
inverseTensorCoeff_zerotheorem — For any scale, an input multi-index of total order at most m, and an output vector of degrees, if some output degree exceeds the input degree in the same coordinate, then the tensor inverse coefficient is zero.hypothesesconclusioninverseTensorCoeff h α.1 β = 0Proof (Lean source)
theorem inverseTensorCoeff_zero {d m : ℕ} (h : ℝ) (α : MultiIndex d m) (β : Fin d → ℕ) (hβ : ¬ ∀ i, β i ≤ α.1 i) : inverseTensorCoeff h α.1 β = 0 := by -- Find an offending coordinate and use inverseEntry_above in prod_eq_zero. classical push Not at hβ obtain ⟨i, hi⟩ := hβ unfold inverseTensorCoeff exact Finset.prod_eq_zero (Finset.mem_univ i) (inverseEntry_above h _ _ hi) -
inverseTensorCoeff_abs_letheorem — For a degree bound m at most two, a scale h that is positive, an input multi-index of total order at most m, and any output vector of degrees, the tensor inverse coefficient is at most h raised to the total order of the input multi-index, in absolute value.hypothesesconclusion|inverseTensorCoeff h α.1 β| ≤ h ^ multiOrder α.1Proof (Lean source)
theorem inverseTensorCoeff_abs_le {d m : ℕ} (hm : m ≤ 2) (h : ℝ) (hh : 0 < h) (α : MultiIndex d m) (β : Fin d → ℕ) : |inverseTensorCoeff h α.1 β| ≤ h ^ multiOrder α.1 := by -- Apply inverseEntry_abs_le coordinatewise and prod_pow_eq_pow_sum. unfold inverseTensorCoeff rw [Finset.abs_prod] calc _ ≤ ∏ i, h ^ α.1 i := Finset.prod_le_prod (fun i _ => abs_nonneg _) (fun i _ => inverseEntry_abs_le h hh _ _ ((coordinate_le_order α.1 i).trans (α.2.trans hm))) _ = h ^ multiOrder α.1 := Finset.prod_pow_eq_pow_sum _ _ _ -
legendreCoefficients_realizetheorem — For a degree bound m at most two, a centre a and a point x, a side length h that is positive, and a vector of monomial coefficients, the scaled Legendre polynomial with the transformed coefficients equals the centred polynomial with the original coefficients, evaluated at x.hypothesesconclusionlegendrePolynomial a h (legendreCoefficients h c) x = ∑ α, c α * centeredMonomial a x α.1Proof (Lean source)
theorem legendreCoefficients_realize {d m : ℕ} (hm : m ≤ 2) (a x : EuclideanSpace ℝ (Fin d)) (h : ℝ) (hh : 0 < h) (c : MultiIndex d m → ℝ) : legendrePolynomial a h (legendreCoefficients h c) x = ∑ α, c α * centeredMonomial a x α.1 := by -- Exchange the two finite sums and use the monomial realization. classical unfold legendrePolynomial legendreCoefficients simp_rw [Finset.mul_sum] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro α _ rw [degree_two_monomial_scaledLegendre hm a x h hh α, Finset.mul_sum] apply Finset.sum_congr rfl intro β _ ring -
legendreCoefficients_l2_boundtheorem — In a dimension and for a degree bound m at most two, there is a positive constant C such that, for every side length h that is positive and at most one half and every coefficient vector whose entries are bounded in absolute value by a nonnegative L, the Euclidean norm of the Legendre coefficients is at most C times L.hypothesesd m :ℕhm :m ≤ 2Proof (Lean source)
theorem legendreCoefficients_l2_bound (d m : ℕ) (hm : m ≤ 2) : ∃ C : ℝ, 0 < C ∧ ∀ (h L : ℝ) (c : MultiIndex d m → ℝ), 0 < h → h ≤ 1 / 2 → 0 ≤ L → (∀ α, |c α| ≤ L) → sqrt (∑ β, legendreCoefficients h c β ^ 2) ≤ C * L := by -- Let N be card (MultiIndex d m). Every matrix entry is ≤1 because -- |entry|≤h^|α| and h≤1; thus |θβ|≤N L and the norm ≤sqrt(N) N L. -- Adding one to sqrt(N) N makes the bound positive without a dimension side condition. classical let N : ℝ := card (MultiIndex d m) have hN : 0 ≤ N := Nat.cast_nonneg _ refine ⟨Real.sqrt N * N + 1, by positivity, ?_⟩ intro h L c hh hhhalf hL hc have hentry (α β : MultiIndex d m) : |inverseTensorCoeff h α.1 β.1| ≤ 1 := (inverseTensorCoeff_abs_le hm h hh α β.1).trans (pow_le_one₀ hh.le (by linarith)) have hθ (β : MultiIndex d m) : |legendreCoefficients h c β| ≤ N * L := by unfold legendreCoefficients calc _ ≤ ∑ α, |c α * inverseTensorCoeff h α.1 β.1| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ _α : MultiIndex d m, L := Finset.sum_le_sum (fun α _ => by rw [abs_mul] simpa using mul_le_mul (hc α) (hentry α β) (abs_nonneg _) hL) _ = N * L := by simp [N] have hsum : (∑ β, legendreCoefficients h c β ^ 2) ≤ N * (N * L) ^ 2 := by calc _ ≤ ∑ _β : MultiIndex d m, (N * L) ^ 2 := Finset.sum_le_sum (fun β _ => by simpa only [sq_abs] using pow_le_pow_left₀ (abs_nonneg _) (hθ β) 2) _ = N * (N * L) ^ 2 := by simp [N] calc _ ≤ sqrt (N * (N * L) ^ 2) := Real.sqrt_le_sqrt hsum _ = sqrt N * N * L := by rw [Real.sqrt_mul hN, Real.sqrt_sq (mul_nonneg hN hL)] ring _ ≤ (sqrt N * N + 1) * L := by nlinarith
Affine 1 core · 2 supporting The map x ↦ 2x-1 sends [0,1]^d to [-1,1]^d. ★ affine_holderBall
Affine transport between fixed cubes
The map x ↦ 2x-1 sends [0,1]^d to [-1,1]^d. Coordinate derivatives of order
j gain 2^j, and the top Hölder seminorm gains 2^(m+s).
theorem affine_holderBall reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
If a function u of d variables lies in the fixed-cube Hölder ball of derivative order m, exponent s, and radius R on the normalized cube, then its pullback z ↦ u(2z − 1) to the unit cube satisfies three things: it is m times continuously differentiable on the unit cube; each of its coordinate partial derivatives of order j at most m is at most 2^j times R in absolute value on the unit cube; and each of its order-m coordinate partials changes between any two points of the unit cube by at most 2^(m + s) times R times their distance to the power s.
Formal statement
hypotheses
conclusion
conclusion 1
ContDiffOn ℝ m (fun z => u (cubeAffine z)) (unitCube d)
conclusion 2
|coordPartial j (fun z => u (cubeAffine z)) f x| ≤ (2 : ℝ) ^ j * R
conclusion 3
|coordPartial m (fun z => u (cubeAffine z)) f x
- coordPartial m (fun z => u (cubeAffine z)) f y|
≤ ((2 : ℝ) ^ ((m : ℝ) + s) * R) * ‖x - y‖ ^ s
Proof (Lean source)
theorem affine_holderBall {d m : ℕ} {s R : ℝ} (u : (Fin d → ℝ) → ℝ)
(hu : HolderBall d m s R u) :
ContDiffOn ℝ m (fun z => u (cubeAffine z)) (unitCube d) ∧
(∀ j ≤ m, ∀ f : Fin j → Fin d, ∀ x ∈ unitCube d,
|coordPartial j (fun z => u (cubeAffine z)) f x| ≤ (2 : ℝ) ^ j * R) ∧
(∀ f : Fin m → Fin d, ∀ x ∈ unitCube d, ∀ y ∈ unitCube d,
|coordPartial m (fun z => u (cubeAffine z)) f x -
coordPartial m (fun z => u (cubeAffine z)) f y| ≤
((2 : ℝ) ^ ((m : ℝ) + s) * R) * ‖x - y‖ ^ s) := by
refine ⟨?_, ?_, affine_topHolder u hu.modulus⟩
· have hmap : Set.MapsTo (cubeAffine : (Fin d → ℝ) → (Fin d → ℝ))
(unitCube d) (cube d) := fun _ hx => cubeAffine_mem_cube hx
simpa only [Function.comp_def] using
hu.regularity.comp cubeAffine_contDiff.contDiffOn hmap
· intro j hj f x hx
rw [affine_coordPartial, abs_mul, abs_of_nonneg (by positivity : 0 ≤ (2 : ℝ) ^ j)]
exact mul_le_mul_of_nonneg_left
(hu.derivBound j hj f (cubeAffine x) (cubeAffine_mem_cube hx))
(by positivity)
2 supporting declarations (lemmas, instances)
-
affine_coordPartialtheorem — A finite dimension, derivative order, response, coordinate-direction sequence, and evaluation point imply that affine transport from the unit cube multiplies the coordinate partial by two to that order.hypothesesconclusioncoordPartial j (fun z => u (cubeAffine z)) f x= (2 : ℝ) ^ j * coordPartial j u f (cubeAffine x)Proof (Lean source)
theorem affine_coordPartial {d j : ℕ} (u : (Fin d → ℝ) → ℝ) (f : Fin j → Fin d) (x : Fin d → ℝ) : coordPartial j (fun z => u (cubeAffine z)) f x = (2 : ℝ) ^ j * coordPartial j u f (cubeAffine x) := by let a : Fin d → ℝ := fun _ => 1 let v : (Fin d → ℝ) → ℝ := fun y => u (y - a) let e : (Fin d → ℝ) ≃L[ℝ] (Fin d → ℝ) := ContinuousLinearEquiv.smulLeft (R₁ := ℝ) (M₁ := Fin d → ℝ) (Units.mk0 (2 : ℝ) (by norm_num)) have he (z : Fin d → ℝ) : e z = (2 : ℝ) • z := by ext i simp [e] have he_map : (e : (Fin d → ℝ) →L[ℝ] (Fin d → ℝ)) = (2 : ℝ) • id ℝ (Fin d → ℝ) := by apply ContinuousLinearMap.ext intro z simpa using he z have hscale := e.iteratedFDerivWithin_comp_right v uniqueDiffOn_univ (Set.mem_univ (e x)) j simp only [Set.preimage_univ, iteratedFDerivWithin_univ] at hscale have hscale' : iteratedFDeriv ℝ j (fun z => v ((2 : ℝ) • z)) x = (iteratedFDeriv ℝ j v ((2 : ℝ) • x)).compContinuousLinearMap (fun _ => (2 : ℝ) • id ℝ (Fin d → ℝ)) := by simpa only [he_map, he, Function.comp_def] using hscale have hc (z : Fin d → ℝ) : cubeAffine z = (2 : ℝ) • z - a := by ext i simp [cubeAffine, a, Pi.smul_apply, Pi.sub_apply, smul_eq_mul] have htrans : iteratedFDeriv ℝ j v ((2 : ℝ) • x) = iteratedFDeriv ℝ j u ((2 : ℝ) • x - a) := by exact iteratedFDeriv_comp_sub j a ((2 : ℝ) • x) unfold coordPartial rw [show (fun z => u (cubeAffine z)) = (fun z => v ((2 : ℝ) • z)) by funext z; simp [v, hc]] rw [hscale', htrans] simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply, smul_apply, ContinuousLinearMap.id_apply] rw [ContinuousMultilinearMap.map_smul_univ] simp [hc, a] -
affine_topHoldertheorem — A finite dimension, derivative order, Hölder exponent, seminorm bound, response, and top-order modulus imply the affine-scaled top-order Hölder modulus on the unit cube.hypothesesconclusion|coordPartial m (fun z => u (cubeAffine z)) f x- coordPartial m (fun z => u (cubeAffine z)) f y|≤ ((2 : ℝ) ^ ((m : ℝ) + s) * L) * ‖x - y‖ ^ sProof (Lean source)
theorem affine_topHolder {d m : ℕ} {s L : ℝ} (u : (Fin d → ℝ) → ℝ) (hL : TopHolder d m s L u) : ∀ f : Fin m → Fin d, ∀ x ∈ unitCube d, ∀ y ∈ unitCube d, |coordPartial m (fun z => u (cubeAffine z)) f x - coordPartial m (fun z => u (cubeAffine z)) f y| ≤ ((2 : ℝ) ^ ((m : ℝ) + s) * L) * ‖x - y‖ ^ s := by intro f x hx y hy rw [affine_coordPartial, affine_coordPartial] have h := hL f (cubeAffine x) (cubeAffine_mem_cube hx) (cubeAffine y) (cubeAffine_mem_cube hy) have hpow : (2 : ℝ) ^ m * (2 * ‖x - y‖) ^ s = (2 : ℝ) ^ ((m : ℝ) + s) * ‖x - y‖ ^ s := by rw [Real.mul_rpow (by norm_num : (0 : ℝ) ≤ 2) (norm_nonneg _), ← Real.rpow_natCast, ← mul_assoc, ← Real.rpow_add (by norm_num : (0 : ℝ) < 2)] calc |(2 : ℝ) ^ m * coordPartial m u f (cubeAffine x) - (2 : ℝ) ^ m * coordPartial m u f (cubeAffine y)| = (2 : ℝ) ^ m * |coordPartial m u f (cubeAffine x) - coordPartial m u f (cubeAffine y)| := by rw [← mul_sub, abs_mul, abs_of_nonneg (by positivity)] _ ≤ (2 : ℝ) ^ m * (L * ‖cubeAffine x - cubeAffine y‖ ^ s) := by exact mul_le_mul_of_nonneg_left h (by positivity) _ = ((2 : ℝ) ^ ((m : ℝ) + s) * L) * ‖x - y‖ ^ s := by rw [cubeAffine_norm_sub] calc (2 : ℝ) ^ m * (L * (2 * ‖x - y‖) ^ s) = ((2 : ℝ) ^ m * (2 * ‖x - y‖) ^ s) * L := by ring _ = _ := by rw [hpow]; ring
Boundary 1 core · 0 supporting Interior estimates for ambient coordinate partials extend to the closed cube under C^m regularity on the cube. ★ interior_coordPartial_bound_extends
Extending coordinate derivative bounds to cube faces
Interior estimates for ambient coordinate partials extend to the closed cube
under C^m regularity on the cube. The ambient derivative convention is kept:
if a boundary derivative does not exist, Lean's derivative has its default zero
value, which also satisfies a nonnegative bound.
theorem interior_coordPartial_bound_extends reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a function that is m times continuously differentiable on the closed normalized cube and a nonnegative bound B, if every coordinate partial of order at most m is at most B in absolute value throughout the open cube, then the same bound holds at every point of the closed cube.
Formal statement
hypotheses
conclusion
DerivBound d m B u
Proof (Lean source)
theorem interior_coordPartial_bound_extends {d m : ℕ}
{u : (Fin d → ℝ) → ℝ} {B : ℝ} (hB : 0 ≤ B)
(hu : ContDiffOn ℝ m u (cube d))
(hinterior : ∀ j ≤ m, ∀ f : Fin j → Fin d,
∀ x ∈ openCube d, |coordPartial j u f x| ≤ B) :
DerivBound d m B u := by
intro j hj f x hx
rcases ambient_jet_zero_or_within hu hj x hx with hzero | hwithin
· simpa [coordPartial, hzero] using hB
· simpa only [coordPartial, hwithin] using
within_coordPartial_bound_extends hu hj f (hinterior j hj f) x hx
BoundaryFacts 1 core · 2 supporting The open cube is dense in the closed cube. ★ ambient_jet_zero_or_within
Cube closure and boundary jets
The open cube is dense in the closed cube. Within derivatives therefore inherit interior bounds. An ambient iterated derivative at a face either agrees with the corresponding within derivative or has Lean's fallback value zero.
theorem ambient_jet_zero_or_within reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a function that is m times continuously differentiable on the closed normalized cube, an order j at most m, and a point of that cube, the order-j iterated derivative taken in the whole space is either zero or equal to the order-j iterated derivative taken within the cube.
Formal statement
hypotheses
conclusion
iteratedFDeriv ℝ j u x
= 0 ∨ iteratedFDeriv ℝ j u x = iteratedFDerivWithin ℝ j u (cube d) x
Proof (Lean source)
theorem ambient_jet_zero_or_within {d m j : ℕ}
{u : (Fin d → ℝ) → ℝ}
(hu : ContDiffOn ℝ m u (cube d)) (hj : j ≤ m)
(x : Fin d → ℝ) (hx : x ∈ cube d) :
iteratedFDeriv ℝ j u x = 0 ∨
iteratedFDeriv ℝ j u x = iteratedFDerivWithin ℝ j u (cube d) x := by
cases j with
| zero =>
exact inr rfl
| succ n =>
let g := iteratedFDeriv ℝ n u
let w := iteratedFDerivWithin ℝ n u (cube d)
by_cases hd : DifferentiableAt ℝ g x
· right
have hnm : (n : WithTop ℕ∞) < m := by exact_mod_cast (Nat.lt_of_succ_le hj)
have hwcont : ContinuousOn w (cube d) :=
hu.continuousOn_iteratedFDerivWithin (by exact_mod_cast (le_of_lt (Nat.lt_of_succ_le hj)))
(cube_uniqueDiffOn d)
have heq : EqOn g w (openCube d) := by
intro y hy
have hreg : ContDiffAt ℝ n u y :=
(hu.mono (openCube_subset_cube d)).contDiffAt
((isOpen_openCube d).mem_nhds hy) |>.of_le
(by exact_mod_cast (le_of_lt (Nat.lt_of_succ_le hj)))
exact (iteratedFDerivWithin_eq_iteratedFDeriv
(cube_uniqueDiffOn d) hreg (openCube_subset_cube d hy)).symm
have hxeq : g x = w x := by
haveI : (nhdsWithin x (openCube d)).NeBot :=
mem_closure_iff_clusterPt.mp (by simpa [closure_openCube_eq_cube] using hx)
exact tendsto_nhds_unique_of_eventuallyEq
(hd.continuousAt.mono_left nhdsWithin_le_nhds)
((hwcont x hx).mono_left (nhdsWithin_mono _ (openCube_subset_cube d)))
(heq.eventuallyEq_of_mem self_mem_nhdsWithin)
have hwdiff := hu.differentiableOn_iteratedFDerivWithin hnm
(cube_uniqueDiffOn d) x hx
have hgderiv : HasFDerivWithinAt g (fderiv ℝ g x) (openCube d) x :=
hd.hasFDerivAt.hasFDerivWithinAt
have hwderiv : HasFDerivWithinAt w
(fderivWithin ℝ w (cube d) x) (openCube d) x :=
hwdiff.hasFDerivWithinAt.mono (openCube_subset_cube d)
have huniq : UniqueDiffWithinAt ℝ (openCube d) x := by
have hc : UniqueDiffWithinAt ℝ (closure (openCube d)) x := by
simpa [closure_openCube_eq_cube] using cube_uniqueDiffOn d x hx
exact hc.of_closure
have hderiv : fderiv ℝ g x = fderivWithin ℝ w (cube d) x :=
huniq.eq hgderiv (hwderiv.congr heq hxeq)
simpa only [iteratedFDeriv_succ_eq_comp_left,
iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, g, w] using
congrArg (continuousMultilinearCurryLeftEquiv ℝ
(fun _ : Fin (n + 1) => Fin d → ℝ) ℝ).symm hderiv
· left
simp [iteratedFDeriv_succ_eq_comp_left,
fderiv_zero_of_not_differentiableAt hd, g]
2 supporting declarations (lemmas, instances)
-
cube_subset_closure_openCubetheorem — Every point of the closed coordinate cube is a limit of points in the open coordinate cube.Proof (Lean source)
theorem cube_subset_closure_openCube (d : ℕ) : cube d ⊆ closure (openCube d) := by intro x hx rw [openCube, mem_closure_pi] intro i _ rw [closure_Ioo (by norm_num : (-1 : ℝ) ≠ 1)] exact hx i -
within_coordPartial_bound_extendstheorem — An interior bound on a coordinate partial extends to the corresponding within derivative throughout the closed cube.hypothesesd m j :ℕ(Fin d → ℝ) → ℝB :ℝhu :ContDiffOn ℝ m u (cube d)hj :j ≤ mhinterior :∀ x ∈ openCube d, |coordPartial j u f x| ≤ Bx ∈ cube d :conclusion|iteratedFDerivWithin ℝ j u (cube d) x (fun a => single (f a) (1 : ℝ))| ≤ BProof (Lean source)
theorem within_coordPartial_bound_extends {d m j : ℕ} {u : (Fin d → ℝ) → ℝ} {B : ℝ} (hu : ContDiffOn ℝ m u (cube d)) (hj : j ≤ m) (f : Fin j → Fin d) (hinterior : ∀ x ∈ openCube d, |coordPartial j u f x| ≤ B) : ∀ x ∈ cube d, |iteratedFDerivWithin ℝ j u (cube d) x (fun a => single (f a) (1 : ℝ))| ≤ B := by let v : Fin j → Fin d → ℝ := fun a => single (f a) (1 : ℝ) have hcont : ContinuousOn (fun x => |iteratedFDerivWithin ℝ j u (cube d) x v|) (cube d) := by have heval : Continuous (fun L : ContinuousMultilinearMap ℝ (fun _ : Fin j => Fin d → ℝ) ℝ => |L v|) := by fun_prop exact heval.comp_continuousOn (hu.continuousOn_iteratedFDerivWithin (by exact_mod_cast hj) (cube_uniqueDiffOn d)) have hbound : ∀ x ∈ openCube d, |iteratedFDerivWithin ℝ j u (cube d) x v| ≤ B := by intro x hx have hreg : ContDiffAt ℝ j u x := (hu.mono (openCube_subset_cube d)).contDiffAt ((isOpen_openCube d).mem_nhds hx) |>.of_le (by exact_mod_cast hj) rw [iteratedFDerivWithin_eq_iteratedFDeriv (cube_uniqueDiffOn d) hreg (openCube_subset_cube d hx)] exact hinterior x hx intro x hx change |iteratedFDerivWithin ℝ j u (cube d) x v| ≤ B exact le_on_closure hbound (by simpa [closure_openCube_eq_cube] using hcont) continuousOn_const (by simpa [closure_openCube_eq_cube] using hx)
Directional 1 core · 1 supporting Finite multilinearity expands a diagonal Fréchet derivative in coordinate directions. ★ topHolder_diagonal_derivative
Coordinate expansion of diagonal derivatives
Finite multilinearity expands a diagonal Fréchet derivative in coordinate directions. The expansion turns the top coordinate Hölder condition into a bound along any line.
theorem topHolder_diagonal_derivative reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a real function that satisfies the top-order Hölder condition on the normalized cube with exponent s and constant L, where L is nonnegative, and for two points x and y and a direction h with both points in the cube, the order-m derivative taken m times in the direction h changes between x and y by at most (d + 1)^m times L times the distance between the points to the power s times the length of h to the power m.
Formal statement
hypotheses
d m :
ℕ
s L :
ℝ
u :
(Fin d → ℝ) → ℝ
hL :
0 ≤ L
hu :
TopHolder d m s L u
x y h :
Fin d → ℝ
hx :
x ∈ cube d
hy :
y ∈ cube d
conclusion
|iteratedFDeriv ℝ m u x (fun _ => h) - iteratedFDeriv ℝ m u y (fun _ => h)|
≤ ((d : ℝ) + 1) ^ m * L * ‖x - y‖ ^ s * ‖h‖ ^ m
Proof (Lean source)
theorem topHolder_diagonal_derivative {d m : ℕ} {s L : ℝ}
(u : (Fin d → ℝ) → ℝ) (hL : 0 ≤ L)
(hu : TopHolder d m s L u) (x y h : Fin d → ℝ)
(hx : x ∈ cube d) (hy : y ∈ cube d) :
|iteratedFDeriv ℝ m u x (fun _ => h) -
iteratedFDeriv ℝ m u y (fun _ => h)| ≤
((d : ℝ) + 1) ^ m * L * ‖x - y‖ ^ s * ‖h‖ ^ m := by
classical
let A : ℝ := L * ‖x - y‖ ^ s
let B : ℝ := ‖h‖ ^ m
have hA : 0 ≤ A := mul_nonneg hL (Real.rpow_nonneg (norm_nonneg _) _)
have hB : 0 ≤ B := pow_nonneg (norm_nonneg _) _
have hterm (f : Fin m → Fin d) :
|(∏ k : Fin m, h (f k)) *
(coordPartial m u f x - coordPartial m u f y)| ≤ B * A := by
have hc : |∏ k : Fin m, h (f k)| ≤ B := by
rw [Finset.abs_prod]
calc
(∏ k : Fin m, |h (f k)|) ≤ ∏ _k : Fin m, ‖h‖ := by
apply Finset.prod_le_prod
· intro k _; exact abs_nonneg _
· intro k _; exact norm_le_pi_norm h (f k)
_ = B := by simp [B]
rw [abs_mul]
exact mul_le_mul hc (hu f x hx y hy) (abs_nonneg _) hB
rw [diagonal_derivative_coordinate_expansion u x h,
diagonal_derivative_coordinate_expansion u y h, ← Finset.sum_sub_distrib]
simp_rw [← mul_sub]
have hsum :
|∑ f : Fin m → Fin d,
(∏ k : Fin m, h (f k)) *
(coordPartial m u f x - coordPartial m u f y)| ≤
(card (Fin m → Fin d) : ℝ) * (B * A) := by
calc
_ ≤ ∑ f : Fin m → Fin d,
|(∏ k : Fin m, h (f k)) *
(coordPartial m u f x - coordPartial m u f y)| := Finset.abs_sum_le_sum_abs _ _
_ ≤ ∑ _f : Fin m → Fin d, B * A := Finset.sum_le_sum (by
intro f _; exact hterm f)
_ = (card (Fin m → Fin d) : ℝ) * (B * A) := by simp
have hcard : (card (Fin m → Fin d) : ℝ) ≤ ((d : ℝ) + 1) ^ m := by
simp only [Fintype.card_fun, Fintype.card_fin, Nat.cast_pow]
gcongr
exact le_add_of_nonneg_right (by norm_num : (0 : ℝ) ≤ 1)
calc
_ ≤ (card (Fin m → Fin d) : ℝ) * (B * A) := hsum
_ ≤ ((d : ℝ) + 1) ^ m * (B * A) := mul_le_mul_of_nonneg_right hcard (mul_nonneg hB hA)
_ = ((d : ℝ) + 1) ^ m * L * ‖x - y‖ ^ s * ‖h‖ ^ m := by
simp only [A, B]
ring
1 supporting declaration (lemmas, instances)
-
diagonal_derivative_coordinate_expansiontheorem — The order-m derivative evaluated repeatedly on one vector is the sum of its coordinate partials weighted by products of that vector's coordinates.hypothesesconclusioniteratedFDeriv ℝ m u x (fun _ => h)Proof (Lean source)
theorem diagonal_derivative_coordinate_expansion {d m : ℕ} (u : (Fin d → ℝ) → ℝ) (x h : Fin d → ℝ) : iteratedFDeriv ℝ m u x (fun _ => h) = ∑ f : Fin m → Fin d, (∏ k : Fin m, h (f k)) * coordPartial m u f x := by classical let F := iteratedFDeriv ℝ m u x have hh : (∑ i : Fin d, single i (h i)) = h := Finset.univ_sum_single h calc F (fun _ => h) = F (fun _ => ∑ i : Fin d, single i (h i)) := by rw [hh] _ = ∑ f : Fin m → Fin d, F (fun k => single (f k) (h (f k))) := F.map_sum (fun _ i => single i (h i)) _ = ∑ f : Fin m → Fin d, (∏ k : Fin m, h (f k)) * coordPartial m u f x := by apply Finset.sum_congr rfl intro f _ have heq : (fun k => single (f k) (h (f k))) = (fun k => h (f k) • single (f k) (1 : ℝ)) := by funext k rw [← Pi.single_smul] simp rw [heq, F.map_smul_univ] simp [F, coordPartial]
Euclidean 2 core · 0 supporting The paper convention uses the square root of the coordinate square sum, while the neutral fixed-cube API uses the ambient norm on Fin d → ℝ. ★ euclidean_to_topHolder
Euclidean seminorm conversion on a finite cube
The paper convention uses the square root of the coordinate square sum, while the
neutral fixed-cube API uses the ambient norm on Fin d → ℝ.
def euclideanDistance reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The Euclidean distance between two d-dimensional coordinate vectors.
theorem euclidean_to_topHolder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension that is at least one, a derivative order, and an exponent s that is positive, there is a positive constant C, depending only on the dimension, the order, and the exponent, such that for every function and every nonnegative L: if every order-m coordinate partial changes between any two points of the normalized cube by at most L times their Euclidean distance to the power s, then the function satisfies the top-order Hölder condition with constant C times L in the coordinatewise-maximum norm.
Formal statement
hypotheses
d m :
ℕ
hd :
1 ≤ d
s :
ℝ
hs :
0 < s
conclusion
∃ C : ℝ,
0 < C
conclusion 1
u :
(Fin d → ℝ) → ℝ
L :
ℝ
0 ≤ L
(∀ f : Fin m → Fin d, ∀ x ∈ cube d, ∀ y ∈ cube d, |coordPartial m u f x - coordPartial m u f y| ≤ L * euclideanDistance x y ^ s)
TopHolder d m s (C * L) u
Proof (Lean source)
theorem euclidean_to_topHolder (d m : ℕ) (hd : 1 ≤ d) (s : ℝ) (hs : 0 < s) :
∃ C : ℝ, 0 < C ∧
∀ (u : (Fin d → ℝ) → ℝ) (L : ℝ),
0 ≤ L →
(∀ f : Fin m → Fin d, ∀ x ∈ cube d, ∀ y ∈ cube d,
|coordPartial m u f x - coordPartial m u f y| ≤
L * euclideanDistance x y ^ s) →
TopHolder d m s (C * L) u := by
refine ⟨(sqrt d) ^ s, Real.rpow_pos_of_pos (Real.sqrt_pos.2 (by exact_mod_cast hd)) _, ?_⟩
intro u L hL hmod f x hx y hy
have hsq : (∑ i : Fin d, (x i - y i) ^ 2) ≤ (d : ℝ) * ‖x - y‖ ^ 2 := by
calc
_ ≤ ∑ _i : Fin d, ‖x - y‖ ^ 2 := by
apply Finset.sum_le_sum
intro i _
have hi := norm_le_pi_norm (x - y) i
simpa only [Pi.sub_apply, Real.norm_eq_abs, sq_abs] using
((sq_le_sq₀ (abs_nonneg _) (norm_nonneg _)).2 hi)
_ = (d : ℝ) * ‖x - y‖ ^ 2 := by simp
have hdist : euclideanDistance x y ≤ sqrt d * ‖x - y‖ := by
calc
euclideanDistance x y ≤ sqrt ((d : ℝ) * ‖x - y‖ ^ 2) :=
Real.sqrt_le_sqrt hsq
_ = sqrt d * ‖x - y‖ := by
rw [Real.sqrt_mul (by positivity : (0 : ℝ) ≤ d), Real.sqrt_sq_eq_abs]
simp
have hpow : euclideanDistance x y ^ s ≤
(sqrt d) ^ s * ‖x - y‖ ^ s := by
calc
_ ≤ (sqrt d * ‖x - y‖) ^ s :=
Real.rpow_le_rpow (Real.sqrt_nonneg _) hdist (le_of_lt hs)
_ = _ := Real.mul_rpow (Real.sqrt_nonneg _) (norm_nonneg _)
exact (hmod f x hx y hy).trans (by
calc
L * euclideanDistance x y ^ s ≤ L * ((sqrt d) ^ s * ‖x - y‖ ^ s) :=
mul_le_mul_of_nonneg_left hpow hL
_ = ((sqrt d) ^ s * L) * ‖x - y‖ ^ s := by ring)
EuclideanRemainder 1 core · 2 supporting Sorted within-cube coordinate Hölder data controls the Taylor remainder from any interior point, including evaluation at a boundary point. ★ local_cube_multiindex_remainder
Euclidean top-Hölder Taylor remainders on arbitrary cubes
Sorted within-cube coordinate Hölder data controls the Taylor remainder from any interior point, including evaluation at a boundary point. The constants are uniform in the exponent 0 < s ≤ 1 as well as center and side length.
The existing top_holder_taylor_remainder and euclidean_to_topHolder live on the normalized Pi cube and ambient jets. Here their segment argument is transported to Euclidean within jets; no ambient differentiability at the boundary is required. Segment.lean isolates the line-jet transport and Holder.lean isolates the sorted-to-diagonal modulus before the final remainder argument.
theorem local_cube_multiindex_remainder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
In a finite Euclidean dimension at a derivative order, there is a positive constant C such that the following holds for every cube of positive side length, every nonnegative L, and every positive exponent s at most one: if a function is m times continuously differentiable on the cube and each of its sorted coordinate partials of total order m changes between any two cube points by at most L times their distance to the power s, then on every smaller cube of positive side length h contained in the big cube and centred at one of its interior points, the function differs from its order-m multi-index Taylor polynomial at that centre by at most C times L times h to the power m + s.
Formal statement
hypotheses
d m :
ℕ
conclusion
∃ C : ℝ,
0 < C
conclusion 1
b a :
EuclideanSpace ℝ (Fin d)
H h L s :
ℝ
u :
EuclideanSpace ℝ (Fin d) → ℝ
0 < H
0 < h
0 ≤ L
0 < s
s ≤ 1
ContDiffOn ℝ m u (centeredCube b H)
(∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H, ∀ z ∈ centeredCube b H, |coordinatePartial (centeredCube b H) u κ.1 x - coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s)
a ∈ interior (centeredCube b H)
centeredCube a h ⊆ centeredCube b H
x ∈ centeredCube a h :
|u x - multiindexTaylor (centeredCube b H) u m a x| ≤ C * L * h ^ ((m : ℝ) + s)
Proof (Lean source)
theorem local_cube_multiindex_remainder (d m : ℕ) :
∃ C : ℝ, 0 < C ∧ ∀ (b a : EuclideanSpace ℝ (Fin d))
(H h L s : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ),
0 < H → 0 < h → 0 ≤ L → 0 < s → s ≤ 1 →
ContDiffOn ℝ m u (centeredCube b H) →
(∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H, ∀ z ∈ centeredCube b H,
|coordinatePartial (centeredCube b H) u κ.1 x -
coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s) →
a ∈ interior (centeredCube b H) → centeredCube a h ⊆ centeredCube b H →
∀ x ∈ centeredCube a h,
|u x - multiindexTaylor (centeredCube b H) u m a x| ≤
C * L * h ^ ((m : ℝ) + s) := by
obtain ⟨Cr, hCr, hr⟩ := cube_euclidean_taylor_remainder d m
let D : ℝ := (d : ℝ) + 1
have hD : 1 ≤ D := by
dsimp [D]
linarith [Nat.cast_nonneg (α := ℝ) d]
have hDpos : 0 < D := lt_of_lt_of_le zero_lt_one hD
refine ⟨Cr * D ^ (m + 1), mul_pos hCr (pow_pos hDpos _), ?_⟩
intro b a H h L s u hH hh hL hs hs1 hu hmod ha hsub x hx
have he : 0 ≤ (m : ℝ) + s := by positivity
have hsqrt : sqrt d ≤ D := by
apply (Real.sqrt_le_iff).mpr
constructor
· exact hDpos.le
· dsimp [D]
nlinarith [Nat.cast_nonneg (α := ℝ) d, sq_nonneg (d : ℝ)]
have hdist : ‖x - a‖ ≤ D * h := by
calc
_ ≤ sqrt d * (h / 2) := centeredCube_norm_sub_le a h hh.le hx
_ ≤ D * (h / 2) := mul_le_mul_of_nonneg_right hsqrt (by positivity)
_ ≤ D * h := mul_le_mul_of_nonneg_left (by linarith) hDpos.le
have hpow : ‖x - a‖ ^ ((m : ℝ) + s) ≤
D ^ (m + 1) * h ^ ((m : ℝ) + s) := by
calc
_ ≤ (D * h) ^ ((m : ℝ) + s) :=
Real.rpow_le_rpow (norm_nonneg _) hdist he
_ = D ^ ((m : ℝ) + s) * h ^ ((m : ℝ) + s) :=
Real.mul_rpow hDpos.le hh.le
_ ≤ D ^ ((m : ℝ) + 1) * h ^ ((m : ℝ) + s) :=
mul_le_mul_of_nonneg_right
(Real.rpow_le_rpow_of_exponent_le hD (by linarith))
(Real.rpow_nonneg hh.le _)
_ = D ^ (m + 1) * h ^ ((m : ℝ) + s) := by
rw [show (m : ℝ) + 1 = ((m + 1 : ℕ) : ℝ) by norm_cast,
Real.rpow_natCast]
rw [← cube_diagonal_taylor_eq_multiindex b a x H hH u hu (interior_subset ha)]
calc
_ ≤ Cr * L * ‖x - a‖ ^ ((m : ℝ) + s) :=
hr b a x H L s u hH hL hs hs1 hu hmod ha (hsub hx)
_ ≤ Cr * L * (D ^ (m + 1) * h ^ ((m : ℝ) + s)) :=
mul_le_mul_of_nonneg_left hpow (mul_nonneg hCr.le hL)
_ = Cr * D ^ (m + 1) * L * h ^ ((m : ℝ) + s) := by ring
2 supporting declarations (lemmas, instances)
-
segment_topHolder_from_sortedtheorem — Take a cube centre b and two points a and y, a side length H that is positive, a real function u, and constants L and s with L nonnegative and s positive. Suppose u is m times continuously differentiable on the cube, every sorted coordinate partial of total order m, taken within the cube, changes between any two cube points by at most L times their distance to the power s, a is interior to the cube, and y lies in the cube. Then for any two times r and q in the half-open unit interval, the m-th derivative of the function restricted to the segment from a to y changes between those times by at most (d + 1)^m times L times the segment length to the power m + s times the time difference to the power s.hypothesesd m :ℕb a y :EuclideanSpace ℝ (Fin d)H :ℝhH :0 < Hu :EuclideanSpace ℝ (Fin d) → ℝL s :ℝhL :0 ≤ Lhs :0 < shu :ContDiffOn ℝ m u (centeredCube b H)hmod :∀ κ : ExactIndex d m,∀ x ∈ centeredCube b H,∀ z ∈ centeredCube b H,|coordinatePartial (centeredCube b H) u κ.1 x- coordinatePartial (centeredCube b H) u κ.1 z|≤ L * ‖x - z‖ ^ sha :a ∈ interior (centeredCube b H)hy :y ∈ centeredCube b Hr q :ℝhr :r ∈ Ico (0 : ℝ) 1hq :q ∈ Ico (0 : ℝ) 1conclusion|iteratedDeriv m (fun t : ℝ => u (a + t • (y - a))) r- iteratedDeriv m (fun t : ℝ => u (a + t • (y - a))) q|≤ ((d : ℝ) + 1) ^ m * L * ‖y - a‖ ^ ((m : ℝ) + s) * |r - q| ^ sProof (Lean source)
theorem segment_topHolder_from_sorted {d m : ℕ} (b a y : EuclideanSpace ℝ (Fin d)) (H : ℝ) (hH : 0 < H) (u : EuclideanSpace ℝ (Fin d) → ℝ) (L s : ℝ) (hL : 0 ≤ L) (hs : 0 < s) (hu : ContDiffOn ℝ m u (centeredCube b H)) (hmod : ∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H, ∀ z ∈ centeredCube b H, |coordinatePartial (centeredCube b H) u κ.1 x - coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s) (ha : a ∈ interior (centeredCube b H)) (hy : y ∈ centeredCube b H) (r q : ℝ) (hr : r ∈ Ico (0 : ℝ) 1) (hq : q ∈ Ico (0 : ℝ) 1) : |iteratedDeriv m (fun t : ℝ => u (a + t • (y - a))) r - iteratedDeriv m (fun t : ℝ => u (a + t • (y - a))) q| ≤ ((d : ℝ) + 1) ^ m * L * ‖y - a‖ ^ ((m : ℝ) + s) * |r - q| ^ s := by rw [segment_iteratedDeriv_eq_within_diagonal b a y H hH u hu ha hy r hr m le_rfl, segment_iteratedDeriv_eq_within_diagonal b a y H hH u hu ha hy q hq m le_rfl] have hrc := interior_subset (segment_mem_interior_centeredCube b a y H ha hy r hr) have hqc := interior_subset (segment_mem_interior_centeredCube b a y H ha hy q hq) have hbound := within_diagonal_topHolder_from_sorted b H hH u L s hL hu hmod (a + r • (y - a)) (a + q • (y - a)) (y - a) hrc hqc have hdiff : (a + r • (y - a)) - (a + q • (y - a)) = (r - q) • (y - a) := by rw [sub_smul] abel rw [hdiff, norm_smul, Real.norm_eq_abs] at hbound calc _ ≤ ((d : ℝ) + 1) ^ m * L * (|r - q| * ‖y - a‖) ^ s * ‖y - a‖ ^ m := hbound _ = _ := by rw [Real.mul_rpow (abs_nonneg _) (norm_nonneg _), Real.rpow_add_of_nonneg (norm_nonneg _) (Nat.cast_nonneg _) hs.le, Real.rpow_natCast] ring -
cube_euclidean_taylor_remaindertheorem — In a finite Euclidean dimension at a derivative order, there is a positive constant C such that the following holds for every cube of positive side length, every nonnegative L, and every positive exponent s at most one: if a function is m times continuously differentiable on the cube and each of its sorted coordinate partials of total order m changes between any two cube points by at most L times their distance to the power s, then at every cube point y the function differs from its order-m diagonal Taylor polynomial centred at an interior point a by at most C times L times the distance from a to y raised to the power m + s.hypothesesd m :ℕconclusion∃ C : ℝ,0 < Cconclusion 1b a y :EuclideanSpace ℝ (Fin d)H L s :ℝu :EuclideanSpace ℝ (Fin d) → ℝ0 < H0 ≤ L0 < ss ≤ 1ContDiffOn ℝ m u (centeredCube b H)(∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H, ∀ z ∈ centeredCube b H, |coordinatePartial (centeredCube b H) u κ.1 x - coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s)a ∈ interior (centeredCube b H)y ∈ centeredCube b H|u y - diagonalTaylor (centeredCube b H) u m a y| ≤ C * L * ‖y - a‖ ^ ((m : ℝ) + s)Proof (Lean source)
theorem cube_euclidean_taylor_remainder (d m : ℕ) : ∃ C : ℝ, 0 < C ∧ ∀ (b a y : EuclideanSpace ℝ (Fin d)) (H L s : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ), 0 < H → 0 ≤ L → 0 < s → s ≤ 1 → ContDiffOn ℝ m u (centeredCube b H) → (∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H, ∀ z ∈ centeredCube b H, |coordinatePartial (centeredCube b H) u κ.1 x - coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s) → a ∈ interior (centeredCube b H) → y ∈ centeredCube b H → |u y - diagonalTaylor (centeredCube b H) u m a y| ≤ C * L * ‖y - a‖ ^ ((m : ℝ) + s) := by refine ⟨((d : ℝ) + 1) ^ m, by positivity, ?_⟩ intro b a y H L s u hH hL hs _hs1 hu hmod ha hy let v : ℝ → ℝ := fun r => u (a + r • (y - a)) have hline : ContDiff ℝ m (fun r : ℝ => a + r • (y - a)) := contDiff_const.add (contDiff_id.smul contDiff_const) have hmaps : Set.MapsTo (fun r : ℝ => a + r • (y - a)) (Icc (0 : ℝ) 1) (centeredCube b H) := by intro r hr by_cases hr1 : r < 1 · exact interior_subset (segment_mem_interior_centeredCube b a y H ha hy r ⟨hr.1, hr1⟩) · have hr' : r = 1 := by linarith [hr.2] subst r simpa using hy have hv : ContDiffOn ℝ m v (Icc (0 : ℝ) 1) := hu.comp hline.contDiffOn hmaps have hzero : (0 : ℝ) ∈ Ico (0 : ℝ) 1 := by norm_num have hderiv (k : ℕ) (hk : k ≤ m) : iteratedDeriv k v 0 = iteratedFDerivWithin ℝ k u (centeredCube b H) a (fun _ => y - a) := by simpa [v] using segment_iteratedDeriv_eq_within_diagonal b a y H hH u hu ha hy 0 hzero k hk have hpoly : (∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedFDerivWithin ℝ k u (centeredCube b H) a (fun _ => y - a)) = ∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k := by apply Finset.sum_congr rfl intro k hk rw [hderiv k (Nat.lt_succ_iff.mp (Finset.mem_range.mp hk))] norm_num have hvone : v 1 = u y := by simp [v] have hbase : ∀ k ≤ m, iteratedDerivWithin k v (uIcc (0 : ℝ) 1) 0 = iteratedDeriv k v 0 := by intro k hk have hcont : ContDiffAt ℝ k v 0 := by have hua : ContDiffAt ℝ k u a := ((hu.mono interior_subset).contDiffAt (isOpen_interior.mem_nhds ha)).of_le (by exact_mod_cast hk) have hlinek : ContDiffAt ℝ k (fun r : ℝ => a + r • (y - a)) 0 := (hline.of_le (by exact_mod_cast hk)).contDiffAt have hua' : ContDiffAt ℝ k u (a + (0 : ℝ) • (y - a)) := by simpa using hua change ContDiffAt ℝ k (u ∘ fun r : ℝ => a + r • (y - a)) 0 exact hua'.comp 0 hlinek exact iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_uIcc (by norm_num : (0 : ℝ) ≠ 1)) hcont Set.left_mem_uIcc by_cases hm0 : m = 0 · subst m have htop := within_diagonal_topHolder_from_sorted b H hH u L s hL hu hmod y a (y - a) hy (interior_subset ha) simpa [diagonalTaylor, iteratedFDerivWithin_zero_apply] using htop · have hmpos : 0 < m := Nat.pos_of_ne_zero hm0 let n := m - 1 have hn : n + 1 = m := Nat.succ_pred_eq_of_pos hmpos have hcont : ContDiffOn ℝ (n + 1) v (uIcc (0 : ℝ) 1) := by change ContDiffOn ℝ (↑(n + 1 : ℕ)) v (uIcc (0 : ℝ) 1) rw [hn, Set.uIcc_of_le (by norm_num : (0 : ℝ) ≤ 1)] exact hv obtain ⟨ξ, hξ, hrem⟩ := taylor_mean_remainder_lagrange_iteratedDeriv (f := v) (x := (1 : ℝ)) (x₀ := (0 : ℝ)) (n := n) (by norm_num) hcont have hξ' : ξ ∈ Ioo (0 : ℝ) 1 := by simpa [Set.uIoo_of_le (by norm_num : (0 : ℝ) ≤ 1)] using hξ have htop : |iteratedDeriv m v ξ - iteratedDeriv m v 0| ≤ ((d : ℝ) + 1) ^ m * L * ‖y - a‖ ^ ((m : ℝ) + s) := by have h := segment_topHolder_from_sorted b a y H hH u L s hL hs hu hmod ha hy ξ 0 ⟨hξ'.1.le, hξ'.2⟩ hzero change |iteratedDeriv m v ξ - iteratedDeriv m v 0| ≤ _ at h have hp : |ξ - 0| ^ s ≤ (1 : ℝ) := by rw [sub_zero, abs_of_pos hξ'.1] simpa using Real.rpow_le_rpow (le_of_lt hξ'.1) hξ'.2.le hs.le calc _ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - a‖ ^ ((m : ℝ) + s) * |ξ - 0| ^ s := h _ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - a‖ ^ ((m : ℝ) + s) * 1 := mul_le_mul_of_nonneg_left hp (by positivity) _ = _ := by ring have hpolyM : (∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k) = (∑ k ∈ range (n + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k) + (Nat.factorial m : ℝ)⁻¹ * iteratedDeriv m v 0 * (1 - 0) ^ m := by rw [hn, Finset.sum_range_succ] have hpolyN : taylorWithinEval v n (uIcc (0 : ℝ) 1) 0 1 = ∑ k ∈ range (n + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k := by rw [taylor_within_apply] apply Finset.sum_congr rfl intro k hk have hk' : k ≤ m := by have hk'' : k ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) omega rw [hbase k hk'] simp only [smul_eq_mul] ring have hdiff : v 1 - (∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k) = (iteratedDeriv m v ξ - iteratedDeriv m v 0) / (Nat.factorial m : ℝ) := by rw [hpolyM, ← hpolyN, sub_add_eq_sub_sub, hrem] simp only [hn] norm_num ring change |u y - (∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedFDerivWithin ℝ k u (centeredCube b H) a (fun _ => y - a))| ≤ _ rw [← hvone, hpoly, hdiff] have hfac : 1 ≤ (Nat.factorial m : ℝ) := by exact_mod_cast Nat.factorial_pos m calc |(iteratedDeriv m v ξ - iteratedDeriv m v 0) / (Nat.factorial m : ℝ)| = |iteratedDeriv m v ξ - iteratedDeriv m v 0| / (Nat.factorial m : ℝ) := by rw [abs_div, abs_of_nonneg (by linarith : (0 : ℝ) ≤ m.factorial)] _ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - a‖ ^ ((m : ℝ) + s) / (Nat.factorial m : ℝ) := div_le_div_of_nonneg_right htop (by linarith) _ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - a‖ ^ ((m : ℝ) + s) := div_le_self (by positivity) hfac
EuclideanSegment 1 core · 1 supporting The segment from an interior point to a closed cube point remains interior before its endpoint. ★ segment_iteratedDeriv_eq_within_diagonal
Segment derivatives of Euclidean within-cube jets
The segment from an interior point to a closed cube point remains interior before its endpoint. Its ordinary iterated derivatives agree with diagonal within-cube jets. This analytic transport imports no Taylor or Hölder layer.
theorem segment_iteratedDeriv_eq_within_diagonal reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a cube with centre b and side length H that is positive, a function u that is m times continuously differentiable on the cube, a point a in the cube's interior, a point y in the cube, a time r in the half-open unit interval, and an order k at most m, the k-th derivative at time r of the function restricted to the segment from a to y equals the order-k derivative within the cube at the point a + r (y − a), taken k times in the direction y − a.
Formal statement
hypotheses
d m :
ℕ
b a y :
EuclideanSpace ℝ (Fin d)
H :
ℝ
hH :
0 < H
u :
EuclideanSpace ℝ (Fin d) → ℝ
hu :
ContDiffOn ℝ m u (centeredCube b H)
ha :
a ∈ interior (centeredCube b H)
hy :
y ∈ centeredCube b H
r :
ℝ
hr :
r ∈ Ico (0 : ℝ) 1
k :
ℕ
hk :
k ≤ m
conclusion
iteratedDeriv k (fun t : ℝ => u (a + t • (y - a))) r
= iteratedFDerivWithin ℝ k u (centeredCube b H) (a + r • (y - a)) (fun _ => y - a)
Proof (Lean source)
theorem segment_iteratedDeriv_eq_within_diagonal {d m : ℕ}
(b a y : EuclideanSpace ℝ (Fin d)) (H : ℝ) (hH : 0 < H)
(u : EuclideanSpace ℝ (Fin d) → ℝ)
(hu : ContDiffOn ℝ m u (centeredCube b H))
(ha : a ∈ interior (centeredCube b H)) (hy : y ∈ centeredCube b H)
(r : ℝ) (hr : r ∈ Ico (0 : ℝ) 1) (k : ℕ) (hk : k ≤ m) :
iteratedDeriv k (fun t : ℝ => u (a + t • (y - a))) r =
iteratedFDerivWithin ℝ k u (centeredCube b H)
(a + r • (y - a)) (fun _ => y - a) := by
-- Reuse CubeInterpolation/Segment.lean's generic chain-rule argument:
-- V=(id ℝ ℝ).smulRight (y-a),
-- U={z | a+z ∈ interior (centeredCube b H)}. U and V⁻¹'U are open.
-- Apply V.iteratedFDerivWithin_comp_right to u ∘ (a+·) on U,
-- then iteratedFDerivWithin_of_isOpen, iteratedFDeriv_comp_add_left,
-- and iteratedDeriv_eq_iteratedFDeriv. Finally convert the ambient jet
-- to the cube jet by iteratedFDerivWithin_eq_iteratedFDeriv using
-- uniqueDiffOn_centeredCube and hu.contDiffAt at the interior point.
-- segment_mem_interior_centeredCube supplies all interior memberships.
-- Keep arbitrary k≤m, boundary y, r=0, and d=0; no extension assumption.
let v : ℝ →L[ℝ] EuclideanSpace ℝ (Fin d) :=
(id ℝ ℝ).smulRight (y - a)
let S : Set (EuclideanSpace ℝ (Fin d)) :=
{z | a + z ∈ interior (centeredCube b H)}
have hS : IsOpen S :=
isOpen_interior.preimage (continuous_const.add continuous_id)
have hf : ContDiffOn ℝ m (fun z : EuclideanSpace ℝ (Fin d) => u (a + z)) S := by
apply hS.contDiffOn_iff.mpr
intro z hz
exact ((hu.mono interior_subset).contDiffAt (isOpen_interior.mem_nhds hz)).comp z
((contDiff_const.add contDiff_id).contDiffAt)
have hinterior := segment_mem_interior_centeredCube b a y H ha hy r hr
have hvr : v r ∈ S := by
simpa [S, v, ContinuousLinearMap.smulRight_apply] using hinterior
have hpre : IsOpen (v ⁻¹' S) := hS.preimage v.continuous
have hcomp := v.iteratedFDerivWithin_comp_right hf hS.uniqueDiffOn
hpre.uniqueDiffOn hvr (show (k : WithTop ℕ∞) ≤ m from mod_cast hk)
have hfun : (fun t : ℝ => u (a + t • (y - a))) =
(fun z : EuclideanSpace ℝ (Fin d) => u (a + z)) ∘ v := by
funext t
simp [v, ContinuousLinearMap.smulRight_apply]
have huAt : ContDiffAt ℝ k u (a + r • (y - a)) :=
((hu.mono interior_subset).contDiffAt
(isOpen_interior.mem_nhds hinterior)).of_le (by exact_mod_cast hk)
rw [iteratedFDerivWithin_eq_iteratedFDeriv
(uniqueDiffOn_centeredCube b H hH) huAt (interior_subset hinterior)]
rw [hfun, iteratedDeriv_eq_iteratedFDeriv]
rw [← iteratedFDerivWithin_of_isOpen k hpre hvr,
hcomp, iteratedFDerivWithin_of_isOpen k hS hvr]
rw [iteratedFDeriv_comp_add_left]
simp [v, ContinuousMultilinearMap.compContinuousLinearMap_apply]
1 supporting declaration (lemmas, instances)
-
segment_mem_interior_centeredCubetheorem — For a cube with centre b and side length H, a point a in the cube's interior, a point y in the cube, and a time r in the half-open unit interval, the point a + r (y − a) of the segment from a to y lies in the cube's interior.hypothesesd :ℕb a y :EuclideanSpace ℝ (Fin d)H :ℝha :a ∈ interior (centeredCube b H)hy :y ∈ centeredCube b Hr :ℝhr :r ∈ Ico (0 : ℝ) 1conclusiona + r • (y - a) ∈ interior (centeredCube b H)Proof (Lean source)
theorem segment_mem_interior_centeredCube {d : ℕ} (b a y : EuclideanSpace ℝ (Fin d)) (H : ℝ) (ha : a ∈ interior (centeredCube b H)) (hy : y ∈ centeredCube b H) (r : ℝ) (hr : r ∈ Ico (0 : ℝ) 1) : a + r • (y - a) ∈ interior (centeredCube b H) := by have h := (centeredCube_convex b H).combo_interior_self_mem_interior ha hy (show 0 < 1 - r by linarith [hr.2]) hr.1 (by ring : (1 - r) + r = 1) convert h using 1 module
Grid 1 core · 0 supporting The existing Causalean tensor interpolation formula supplies a uniform coefficient norm bound for polynomials of arbitrary finite coordinate degree. ★ tensor_coefficient_bound
Fixed tensor grid coefficient bounds
The existing Causalean tensor interpolation formula supplies a uniform coefficient norm bound for polynomials of arbitrary finite coordinate degree.
theorem tensor_coefficient_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension and a degree m, there is a positive constant C such that every multivariate polynomial of degree at most m in each variable that is bounded in absolute value by a nonnegative B at every point of the fixed tensor grid has every tensor monomial coefficient bounded in absolute value by C times B.
Formal statement
hypotheses
d m :
ℕ
conclusion
∃ C : ℝ,
0 < C
conclusion 1
|tensorCoeffs (D := m) p a| ≤ C * B
Proof (Lean source)
theorem tensor_coefficient_bound (d m : ℕ) :
∃ C : ℝ, 0 < C ∧
∀ (p : MvPolynomial (Fin d) ℝ) (B : ℝ),
0 ≤ B → (∀ i, p.degreeOf i ≤ m) →
(∀ b : Fin d → Fin (m + 1),
|eval (tensorGridPoint b) p| ≤ B) →
∀ a : Fin d → Fin (m + 1), |tensorCoeffs (D := m) p a| ≤ C * B := by
classical
refine ⟨((2 : ℝ) ^ (4 * m + 4)) ^ d, by positivity, ?_⟩
intro p B hB hdeg hgrid a
have hw : (∑ b : Fin d → Fin (m + 1), |tensorGridWeight a b|) ≤
((2 : ℝ) ^ (4 * m + 4)) ^ d := by
calc
_ ≤ ∑ a : Fin d → Fin (m + 1),
∑ b : Fin d → Fin (m + 1), |tensorGridWeight a b| :=
Finset.single_le_sum (fun _ _ => Finset.sum_nonneg (fun _ _ => abs_nonneg _))
(Finset.mem_univ a)
_ ≤ _ := tensorGrid_weight_oneNorm_le d m
rw [tensorGrid_coeff_recovery p hdeg a]
calc
|∑ b : Fin d → Fin (m + 1),
tensorGridWeight a b * eval (tensorGridPoint b) p| ≤
∑ b : Fin d → Fin (m + 1),
|tensorGridWeight a b * eval (tensorGridPoint b) p| :=
Finset.abs_sum_le_sum_abs _ _
_ = ∑ b : Fin d → Fin (m + 1),
|tensorGridWeight a b| * |eval (tensorGridPoint b) p| := by
simp only [abs_mul]
_ ≤ ∑ b : Fin d → Fin (m + 1), |tensorGridWeight a b| * B := by
apply Finset.sum_le_sum
intro b _
exact mul_le_mul_of_nonneg_left (hgrid b) (abs_nonneg _)
_ = (∑ b : Fin d → Fin (m + 1), |tensorGridWeight a b|) * B := by
rw [Finset.sum_mul]
_ ≤ ((2 : ℝ) ^ (4 * m + 4)) ^ d * B :=
mul_le_mul_of_nonneg_right hw hB
GridResponse 1 core · 0 supporting The top derivative seminorm controls the Taylor remainder at every fixed grid node. ★ taylor_polynomial_grid_bound
Taylor polynomial values on the fixed tensor grid
The top derivative seminorm controls the Taylor remainder at every fixed grid node. Together with the response supremum this bounds the Taylor polynomial on that grid, with a constant independent of the function and its bounds.
theorem taylor_polynomial_grid_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension, a derivative order m, and an exponent s with s positive, there is a positive constant C such that the following holds for all nonnegative M and L: if a function is m times continuously differentiable on the closed normalized cube, bounded there by M in absolute value, and satisfies the top-order Hölder condition with exponent s and constant L, then any polynomial that equals its order-m Taylor polynomial at a centre in the open cube is at most C times (M + L) in absolute value at every node of the fixed tensor grid.
Formal statement
hypotheses
d m :
ℕ
s :
ℝ
hs :
0 < s
conclusion
∃ C : ℝ,
0 < C
conclusion 1
u :
(Fin d → ℝ) → ℝ
M L :
ℝ
0 ≤ M
0 ≤ L
ContDiffOn ℝ m u (cube d)
(∀ y ∈ cube d, |u y| ≤ M)
TopHolder d m s L u
x ∈ openCube d :
p :
MvPolynomial (Fin d) ℝ
(∀ y : Fin d → ℝ, eval y p = ∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => y - x))
|eval (tensorGridPoint b) p| ≤ C * (M + L)
Proof (Lean source)
theorem taylor_polynomial_grid_bound (d m : ℕ) (s : ℝ)
(hs : 0 < s) :
∃ C : ℝ, 0 < C ∧
∀ (u : (Fin d → ℝ) → ℝ) (M L : ℝ),
0 ≤ M → 0 ≤ L → ContDiffOn ℝ m u (cube d) →
(∀ y ∈ cube d, |u y| ≤ M) → TopHolder d m s L u →
∀ x ∈ openCube d, ∀ p : MvPolynomial (Fin d) ℝ,
(∀ y : Fin d → ℝ,
eval y p =
∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ *
iteratedFDeriv ℝ k u x (fun _ => y - x)) →
∀ b : Fin d → Fin (m + 1),
|eval (tensorGridPoint b) p| ≤ C * (M + L) := by
obtain ⟨A, hApos, hA⟩ := top_holder_taylor_remainder d m s hs
have hcompact : IsCompact (cube d) := by
have h := isCompact_univ_pi (fun _ : Fin d => isCompact_Icc (a := (-1 : ℝ)) (b := 1))
convert h using 1
ext z
simp only [cube, normalizedCube,
Set.mem_ofPred_eq, Set.mem_univ_pi, Set.mem_Icc]
obtain ⟨D, hD⟩ := Metric.isBounded_iff.mp hcompact.isBounded
let K : ℝ := max 1 D
have hKpos : 0 < K := lt_of_lt_of_le (by norm_num) (le_max_left _ _)
have hKdist : ∀ x ∈ cube d, ∀ y ∈ cube d, ‖y - x‖ ≤ K := by
intro x hx y hy
rw [← dist_eq_norm]
exact (hD hy hx).trans (le_max_right _ _)
refine ⟨1 + A * K ^ ((m : ℝ) + s), by positivity, ?_⟩
intro u M L hM hL hu hbound hholder x hx p hp b
let y := tensorGridPoint b
have hy : y ∈ cube d := tensorGridPoint_mem_cube b
have hx' : x ∈ cube d := by
intro i
exact ⟨le_of_lt (hx i (Set.mem_univ i)).1,
le_of_lt (hx i (Set.mem_univ i)).2⟩
have hpow : ‖y - x‖ ^ ((m : ℝ) + s) ≤ K ^ ((m : ℝ) + s) :=
Real.rpow_le_rpow (norm_nonneg _) (hKdist x hx' y hy) (by positivity)
have hrem := hA u L hL hu hholder x hx y hy
rw [← hp y] at hrem
have hpoly : |eval y p| ≤ M + A * L * K ^ ((m : ℝ) + s) := by
calc
|eval y p| = |u y - (u y - eval y p)| := by ring
_ ≤ |u y| + |u y - eval y p| := by
simpa [abs_sub_comm] using abs_sub_le (u y) 0 (u y - eval y p)
_ ≤ M + A * L * ‖y - x‖ ^ ((m : ℝ) + s) :=
add_le_add (hbound y hy) hrem
_ ≤ M + A * L * K ^ ((m : ℝ) + s) := by
have h := mul_le_mul_of_nonneg_left hpow (mul_nonneg hApos.le hL)
nlinarith [h]
change |eval y p| ≤ (1 + A * K ^ ((m : ℝ) + s)) * (M + L)
nlinarith [mul_nonneg (le_of_lt hApos) (Real.rpow_nonneg hKpos.le ((m : ℝ) + s))]
Holder 1 core · 0 supporting Permutation invariance converts a modulus on sorted top-order coordinate partials into a modulus on every word jet. ★ within_diagonal_topHolder_from_sorted
Sorted Euclidean Hölder data controls diagonal within jets
Permutation invariance converts a modulus on sorted top-order coordinate partials into a modulus on every word jet. Multilinearity then gives a uniform diagonal estimate at arbitrary cube points, including the boundary. This finite-sum estimate is independent of segment differentiation.
theorem within_diagonal_topHolder_from_sorted reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
Take a cube with centre b and side length H that is positive, a real function u, and constants L and s with L nonnegative. Suppose u is m times continuously differentiable on the cube and every sorted coordinate partial of total order m, taken within the cube, changes between any two cube points by at most L times their distance to the power s. Then for two points x and z and a direction v with both points in the cube, the order-m derivative within the cube, taken m times in the direction v, changes between x and z by at most (d + 1)^m times L times the distance between the points to the power s times the length of v to the power m.
Formal statement
hypotheses
d m :
ℕ
b :
EuclideanSpace ℝ (Fin d)
H :
ℝ
hH :
0 < H
u :
EuclideanSpace ℝ (Fin d) → ℝ
L s :
ℝ
hL :
0 ≤ L
hu :
ContDiffOn ℝ m u (centeredCube b H)
hmod :
∀ κ : ExactIndex d m,
∀ x ∈ centeredCube b H,
∀ z ∈ centeredCube b H,
|coordinatePartial (centeredCube b H) u κ.1 x
- coordinatePartial (centeredCube b H) u κ.1 z|
≤ L * ‖x - z‖ ^ s
x z v :
EuclideanSpace ℝ (Fin d)
hx :
x ∈ centeredCube b H
hz :
z ∈ centeredCube b H
conclusion
|iteratedFDerivWithin ℝ m u (centeredCube b H) x (fun _ => v)
- iteratedFDerivWithin ℝ m u (centeredCube b H) z (fun _ => v)|
≤ ((d : ℝ) + 1) ^ m * L * ‖x - z‖ ^ s * ‖v‖ ^ m
Proof (Lean source)
theorem within_diagonal_topHolder_from_sorted {d m : ℕ}
(b : EuclideanSpace ℝ (Fin d)) (H : ℝ) (hH : 0 < H)
(u : EuclideanSpace ℝ (Fin d) → ℝ) (L s : ℝ) (hL : 0 ≤ L)
(hu : ContDiffOn ℝ m u (centeredCube b H))
(hmod : ∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H,
∀ z ∈ centeredCube b H,
|coordinatePartial (centeredCube b H) u κ.1 x -
coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s)
(x z v : EuclideanSpace ℝ (Fin d))
(hx : x ∈ centeredCube b H) (hz : z ∈ centeredCube b H) :
|iteratedFDerivWithin ℝ m u (centeredCube b H) x (fun _ => v) -
iteratedFDerivWithin ℝ m u (centeredCube b H) z (fun _ => v)| ≤
((d : ℝ) + 1) ^ m * L * ‖x - z‖ ^ s * ‖v‖ ^ m := by
classical
have hsorted (κ : ExactIndex d m) (a : EuclideanSpace ℝ (Fin d)) :
wordPartialWithin (centeredCube b H) u (sortedWordOfOrder κ) a =
coordinatePartial (centeredCube b H) u κ.1 a := by
rcases κ with ⟨κ, hκ⟩
subst m
rfl
have hcount (κ : ExactIndex d m) : coordCount (sortedWordOfOrder κ) = κ.1 := by
rcases κ with ⟨κ, hκ⟩
subst m
exact sortedWord_count κ
have hword (w : Fin m → Fin d) (a : EuclideanSpace ℝ (Fin d))
(ha : a ∈ centeredCube b H) :
wordPartialWithin (centeredCube b H) u w a =
coordinatePartial (centeredCube b H) u (coordCount w) a := by
let κ : ExactIndex d m := ⟨coordCount w, coordCount_order w⟩
calc
_ = wordPartialWithin (centeredCube b H) u (sortedWordOfOrder κ) a := by
apply wordPartialWithin_eq_of_count
(centeredCube b H) u a
(euclidean_within_jet_perm (uniqueDiffOn_centeredCube b H hH) hu ha
(centeredCube_subset_closure_interior b H hH ha))
exact (hcount κ).symm
_ = _ := hsorted κ a
-- The finite-sum estimate of CubeInterpolation.topHolder_diagonal_derivative,
-- using Euclidean coordinate bounds in place of its Pi sup-norm bounds.
let A : ℝ := L * ‖x - z‖ ^ s
let B : ℝ := ‖v‖ ^ m
have hA : 0 ≤ A := mul_nonneg hL (Real.rpow_nonneg (norm_nonneg _) _)
have hB : 0 ≤ B := pow_nonneg (norm_nonneg _) _
have hterm (w : Fin m → Fin d) :
|(∏ r : Fin m, v (w r)) *
(wordPartialWithin (centeredCube b H) u w x -
wordPartialWithin (centeredCube b H) u w z)| ≤ B * A := by
have hc : |∏ r : Fin m, v (w r)| ≤ B := by
rw [Finset.abs_prod]
calc
(∏ r : Fin m, |v (w r)|) ≤ ∏ _r : Fin m, ‖v‖ := by
apply Finset.prod_le_prod
· intro r _; exact abs_nonneg _
· intro r _; exact (Real.norm_eq_abs _).symm ▸ PiLp.norm_apply_le v (w r)
_ = B := by simp [B]
have hm : |wordPartialWithin (centeredCube b H) u w x -
wordPartialWithin (centeredCube b H) u w z| ≤ A := by
rw [hword w x hx, hword w z hz]
exact hmod ⟨coordCount w, coordCount_order w⟩ x hx z hz
rw [abs_mul]
exact mul_le_mul hc hm (abs_nonneg _) hB
rw [within_diagonal_derivative_coordinate_expansion,
within_diagonal_derivative_coordinate_expansion, ← Finset.sum_sub_distrib]
simp_rw [← mul_sub]
have hsum :
|∑ w : Fin m → Fin d, (∏ r : Fin m, v (w r)) *
(wordPartialWithin (centeredCube b H) u w x -
wordPartialWithin (centeredCube b H) u w z)| ≤
(card (Fin m → Fin d) : ℝ) * (B * A) := by
calc
_ ≤ ∑ w : Fin m → Fin d, |(∏ r : Fin m, v (w r)) *
(wordPartialWithin (centeredCube b H) u w x -
wordPartialWithin (centeredCube b H) u w z)| :=
Finset.abs_sum_le_sum_abs _ _
_ ≤ ∑ _w : Fin m → Fin d, B * A := Finset.sum_le_sum (by
intro w _; exact hterm w)
_ = (card (Fin m → Fin d) : ℝ) * (B * A) := by simp
have hcard : (card (Fin m → Fin d) : ℝ) ≤ ((d : ℝ) + 1) ^ m := by
simp only [Fintype.card_fun, Fintype.card_fin, Nat.cast_pow]
gcongr
exact le_add_of_nonneg_right (by norm_num : (0 : ℝ) ≤ 1)
calc
_ ≤ (card (Fin m → Fin d) : ℝ) * (B * A) := hsum
_ ≤ ((d : ℝ) + 1) ^ m * (B * A) :=
mul_le_mul_of_nonneg_right hcard (mul_nonneg hB hA)
_ = ((d : ℝ) + 1) ^ m * L * ‖x - z‖ ^ s * ‖v‖ ^ m := by
simp only [A, B]
ring
Interpolation 1 core · 2 supporting The main estimate bounds all lower coordinate partials from a response supremum and the seminorm of the highest coordinate partials, uniformly over the response. ★ fixed_cube_holder_completion
Fixed-cube Hölder interpolation
The main estimate bounds all lower coordinate partials from a response supremum and the seminorm of the highest coordinate partials, uniformly over the response.
theorem fixed_cube_holder_completion reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
In dimension d, for a smoothness index β greater than one, write m for the largest integer strictly below β and s = β − m. Then there is a positive constant K, depending only on d and β, such that for all nonnegative M and L: every function that is m times continuously differentiable on the closed normalized cube, is bounded there by M in absolute value, and satisfies the top-order Hölder condition of order m with exponent s and constant L, lies in the fixed-cube Hölder ball of order m, exponent s, and radius K times (M + L); in particular all its coordinate partials of order at most m are bounded by K times (M + L) on the cube.
Formal statement
hypotheses
d :
ℕ
β :
ℝ
hβ :
1 < β
conclusion
∃ K : ℝ,
0 < K
conclusion 1
u :
(Fin d → ℝ) → ℝ
M L :
ℝ
0 ≤ M
0 ≤ L
ContDiffOn ℝ (⌈β⌉₊ - 1) u (cube d)
(∀ x ∈ cube d, |u x| ≤ M)
TopHolder d (⌈β⌉₊ - 1) (β - ((⌈β⌉₊ - 1 : ℕ) : ℝ)) L u
HolderBall d (⌈β⌉₊ - 1) (β - ((⌈β⌉₊ - 1 : ℕ) : ℝ)) (K * (M + L)) u
Proof (Lean source)
theorem fixed_cube_holder_completion (d : ℕ)
(β : ℝ) (hβ : 1 < β) :
∃ K : ℝ, 0 < K ∧
∀ (u : (Fin d → ℝ) → ℝ) (M L : ℝ),
0 ≤ M → 0 ≤ L →
ContDiffOn ℝ (⌈β⌉₊ - 1) u (cube d) →
(∀ x ∈ cube d, |u x| ≤ M) →
TopHolder d (⌈β⌉₊ - 1) (β - ((⌈β⌉₊ - 1 : ℕ) : ℝ)) L u →
HolderBall d (⌈β⌉₊ - 1)
(β - ((⌈β⌉₊ - 1 : ℕ) : ℝ)) (K * (M + L)) u := by
have hceil_one : 1 ≤ ⌈β⌉₊ := Nat.one_le_ceil_iff.mpr (by linarith)
have hcast : ((⌈β⌉₊ - 1 : ℕ) : ℝ) = (⌈β⌉₊ : ℝ) - 1 := by
rw [Nat.cast_sub hceil_one, Nat.cast_one]
have hs : 0 < β - ((⌈β⌉₊ - 1 : ℕ) : ℝ) := by
rw [hcast]
linarith [Nat.ceil_lt_add_one (by linarith : 0 ≤ β)]
have hs1 : β - ((⌈β⌉₊ - 1 : ℕ) : ℝ) ≤ 1 := by
rw [hcast]
linarith [Nat.le_ceil β]
obtain ⟨K, hK, hinterp⟩ :=
fixed_cube_interpolation d (⌈β⌉₊ - 1)
(β - ((⌈β⌉₊ - 1 : ℕ) : ℝ)) hs
refine ⟨K + 1, by linarith, ?_⟩
intro u M L hM hL hu hbound hholder
have hsum : 0 ≤ M + L := add_nonneg hM hL
have hKle : K ≤ K + 1 := by linarith
have hLradius : L ≤ (K + 1) * (M + L) := by
calc
L ≤ M + L := by linarith
_ = 1 * (M + L) := by ring
_ ≤ (K + 1) * (M + L) :=
mul_le_mul_of_nonneg_right (by linarith : 1 ≤ K + 1) hsum
refine ⟨hu, ?_, ?_⟩
· intro j hj f x hx
exact (hinterp u M L hM hL hu hbound hholder j hj f x hx).trans
(mul_le_mul_of_nonneg_right hKle hsum)
· intro f x hx y hy
exact (hholder f x hx y hy).trans
(mul_le_mul_of_nonneg_right hLradius (by positivity))
2 supporting declarations (lemmas, instances)
-
interior_fixed_cube_interpolationtheorem — A finite dimension, derivative order, and positive Hölder exponent guarantee a positive uniform constant controlling every coordinate partial in the open normalized cube from the response supremum and top-order Hölder seminorm.hypothesesd m :ℕs :ℝhs :0 < sconclusion∃ K : ℝ,0 < Kconclusion 1u :(Fin d → ℝ) → ℝM L :ℝ0 ≤ M0 ≤ LContDiffOn ℝ m u (cube d)(∀ x ∈ cube d, |u x| ≤ M)TopHolder d m s L uj ≤ m :x ∈ openCube d :|coordPartial j u f x| ≤ K * (M + L)Proof (Lean source)
theorem interior_fixed_cube_interpolation (d m : ℕ) (s : ℝ) (hs : 0 < s) : ∃ K : ℝ, 0 < K ∧ ∀ (u : (Fin d → ℝ) → ℝ) (M L : ℝ), 0 ≤ M → 0 ≤ L → ContDiffOn ℝ m u (cube d) → (∀ x ∈ cube d, |u x| ≤ M) → TopHolder d m s L u → ∀ j ≤ m, ∀ f : Fin j → Fin d, ∀ x ∈ openCube d, |coordPartial j u f x| ≤ K * (M + L) := by obtain ⟨C₁, hC₁, hgrid⟩ := taylor_polynomial_grid_bound d m s hs obtain ⟨C₂, hC₂, hpoly⟩ := tensor_polynomial_deriv_bound d m refine ⟨C₂ * C₁, mul_pos hC₂ hC₁, ?_⟩ intro u M L hM hL hu hbound hholder j hj f x hx obtain ⟨p, hdegree, hp⟩ := taylor_expression_polynomial d m u x have ho : IsOpen (openCube d) := isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo) have hsub : openCube d ⊆ cube d := by intro z hz i exact ⟨le_of_lt (hz i (Set.mem_univ i)).1, le_of_lt (hz i (Set.mem_univ i)).2⟩ have hux : ContDiffAt ℝ m u x := (hu.mono hsub).contDiffAt (ho.mem_nhds hx) have hB : 0 ≤ C₁ * (M + L) := mul_nonneg (le_of_lt hC₁) (add_nonneg hM hL) have hpbound := hpoly p (C₁ * (M + L)) hB hdegree (hgrid u M L hM hL hu hbound hholder x hx p hp) j hj f x (hsub hx) rw [← taylor_polynomial_jet_match hux hp j hj f] calc |coordPartial j (fun z => eval z p) f x| ≤ C₂ * (C₁ * (M + L)) := hpbound _ = (C₂ * C₁) * (M + L) := by ring -
fixed_cube_interpolationtheorem — A finite dimension, derivative order, and positive Hölder exponent guarantee a positive uniform constant controlling every coordinate partial on the closed normalized cube from the response supremum and top-order Hölder seminorm.hypothesesd m :ℕs :ℝhs :0 < sconclusion∃ K : ℝ,0 < Kconclusion 1u :(Fin d → ℝ) → ℝM L :ℝ0 ≤ M0 ≤ LContDiffOn ℝ m u (cube d)(∀ x ∈ cube d, |u x| ≤ M)TopHolder d m s L uDerivBound d m (K * (M + L)) uProof (Lean source)
theorem fixed_cube_interpolation (d m : ℕ) (s : ℝ) (hs : 0 < s) : ∃ K : ℝ, 0 < K ∧ ∀ (u : (Fin d → ℝ) → ℝ) (M L : ℝ), 0 ≤ M → 0 ≤ L → ContDiffOn ℝ m u (cube d) → (∀ x ∈ cube d, |u x| ≤ M) → TopHolder d m s L u → DerivBound d m (K * (M + L)) u := by obtain ⟨K, hK, hinterior⟩ := interior_fixed_cube_interpolation d m s hs refine ⟨K, hK, ?_⟩ intro u M L hM hL hu hbound hholder apply interior_coordPartial_bound_extends (mul_nonneg (le_of_lt hK) (add_nonneg hM hL)) hu exact hinterior u M L hM hL hu hbound hholder
JetHomogeneous 1 core · 2 supporting The homogeneous terms of a finite Fréchet Taylor expression have zero jets away from their own degree. ★ homogeneous_taylor_jet_at_degree
Jets of homogeneous Taylor terms
The homogeneous terms of a finite Fréchet Taylor expression have zero jets away from their own degree. At the matching degree, symmetry of the iterated derivative recovers the original ordered coordinate partial.
theorem homogeneous_taylor_jet_at_degree reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
If a function is k times continuously differentiable at a point, then for any sequence of k coordinate directions, the order-k coordinate partial along that sequence of the degree-k Taylor term centred at the point, evaluated at the point, equals the same coordinate partial of the function there.
Formal statement
hypotheses
conclusion
coordPartial k (fun z => (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => z - x)) f x
= coordPartial k u f x
Proof (Lean source)
theorem homogeneous_taylor_jet_at_degree {d k : ℕ}
{u : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ}
(hu : ContDiffAt ℝ k u x) (f : Fin k → Fin d) :
coordPartial k
(fun z => (Nat.factorial k : ℝ)⁻¹ *
iteratedFDeriv ℝ k u x (fun _ => z - x)) f x =
coordPartial k u f x := by
-- Differentiation produces a permutation sum. The iterated derivative is
-- symmetric at a C^k point, so division by k! leaves one ordered value.
classical
let A := (Nat.factorial k : ℝ)⁻¹ • iteratedFDeriv ℝ k u x
let g' : (Fin d → ℝ) → ℝ := fun y => A (fun _ => y)
have hfun : (fun z => (Nat.factorial k : ℝ)⁻¹ *
iteratedFDeriv ℝ k u x (fun _ => z - x)) =
(fun z => g' (z - x)) := by
funext z
simp [g', A, smul_eq_mul]
unfold coordPartial
rw [hfun, iteratedFDeriv_comp_sub]
simp only [sub_self]
change (iteratedFDeriv ℝ k (fun z => A (fun _ => z)) 0)
(fun i => single (f i) (1 : ℝ)) = _
rw [A.iteratedFDeriv_comp_diagonal]
simp only [A, smul_apply, smul_eq_mul]
have hperm (σ : Perm (Fin k)) :
iteratedFDeriv ℝ k u x (fun i => single (f (σ i)) (1 : ℝ)) =
iteratedFDeriv ℝ k u x (fun i => single (f i) (1 : ℝ)) := by
simpa only [Function.comp_def] using
finite_order_iteratedFDeriv_perm hu
(fun i => single (f i) (1 : ℝ)) σ
simp_rw [hperm]
have hn : (Nat.factorial k : ℝ) ≠ 0 := by exact_mod_cast Nat.factorial_ne_zero k
simp [Fintype.card_perm, hn]
2 supporting declarations (lemmas, instances)
-
homogeneous_taylor_jet_below_degreetheorem — A homogeneous Taylor term of degree k has zero coordinate partial of every smaller order j at its center.hypothesesconclusioncoordPartial j (fun z => (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => z - x)) f x= 0Proof (Lean source)
theorem homogeneous_taylor_jet_below_degree {d j k : ℕ} (hjk : j < k) (u : (Fin d → ℝ) → ℝ) (x : Fin d → ℝ) (f : Fin j → Fin d) : coordPartial j (fun z => (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => z - x)) f x = 0 := by let A := (Nat.factorial k : ℝ)⁻¹ • iteratedFDeriv ℝ k u x let D : (Fin d → ℝ) →L[ℝ] (Fin k → (Fin d → ℝ)) := ContinuousLinearMap.pi (fun _ => id ℝ (Fin d → ℝ)) have hfun : (fun z => (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => z - x)) = (fun z => A (D (z - x))) := by funext z simp [A, D, smul_eq_mul] unfold coordPartial rw [hfun] change (iteratedFDeriv ℝ j (fun z => (A ∘ D) (z - x)) x) (fun i => single (f i) (1 : ℝ)) = 0 rw [iteratedFDeriv_comp_sub] simp only [sub_self] rw [D.iteratedFDeriv_comp_right A.contDiff 0 le_rfl, A.iteratedFDeriv_eq] have hzero : A.iteratedFDeriv j (0 : Fin k → (Fin d → ℝ)) = 0 := by apply norm_eq_zero.mp have h := A.norm_iteratedFDeriv_le' j (fun _ => (0 : Fin d → ℝ)) simp only [Fintype.card_fin] at h have hz : (fun _ : Fin k => (0 : Fin d → ℝ)) = 0 := rfl rw [hz, norm_zero, zero_pow (by omega : k - j ≠ 0), mul_zero] at h exact le_antisymm (by simpa using h) (norm_nonneg _) simp only [map_zero] rw [hzero] simp -
homogeneous_taylor_jet_above_degreetheorem — A homogeneous Taylor term of degree k has zero coordinate partial of every larger order j at its center.hypothesesconclusioncoordPartial j (fun z => (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => z - x)) f x= 0Proof (Lean source)
theorem homogeneous_taylor_jet_above_degree {d j k : ℕ} (hkj : k < j) (u : (Fin d → ℝ) → ℝ) (x : Fin d → ℝ) (f : Fin j → Fin d) : coordPartial j (fun z => (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => z - x)) f x = 0 := by let A := (Nat.factorial k : ℝ)⁻¹ • iteratedFDeriv ℝ k u x let D : (Fin d → ℝ) →L[ℝ] (Fin k → (Fin d → ℝ)) := ContinuousLinearMap.pi (fun _ => id ℝ (Fin d → ℝ)) have hfun : (fun z => (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => z - x)) = (fun z => A (D (z - x))) := by funext z simp [A, D, smul_eq_mul] unfold coordPartial rw [hfun] change (iteratedFDeriv ℝ j (fun z => (A ∘ D) (z - x)) x) (fun i => single (f i) (1 : ℝ)) = 0 rw [iteratedFDeriv_comp_sub] simp only [sub_self] rw [D.iteratedFDeriv_comp_right A.contDiff 0 le_rfl, A.iteratedFDeriv_eq] have hzero : A.iteratedFDeriv j (0 : Fin k → (Fin d → ℝ)) = 0 := by classical simp only [ContinuousMultilinearMap.iteratedFDeriv] apply Finset.sum_eq_zero intro e _ have he : j ≤ k := by simpa using Fintype.card_le_of_injective e e.injective omega simp only [map_zero] rw [hzero] simp
JetPolynomial 1 core · 1 supporting The diagonal evaluations of finitely many multilinear derivatives form a multivariate polynomial. ★ taylor_polynomial_jet_match
Polynomial realization of a finite Taylor jet
The diagonal evaluations of finitely many multilinear derivatives form a multivariate polynomial. At a smooth point its coordinate derivatives recover the corresponding coordinate derivatives of the original function.
theorem taylor_polynomial_jet_match reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
If a function is m times continuously differentiable at a point and a polynomial agrees everywhere with the function's order-m Taylor polynomial at that point, then every coordinate partial derivative of the polynomial of order at most m, evaluated at the expansion point, equals the corresponding coordinate partial of the function there.
Formal statement
hypotheses
hu :
ContDiffAt ℝ m u x
p :
MvPolynomial (Fin d) ℝ
hp :
∀ y : Fin d → ℝ,
eval y p
= ∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => y - x)
j ≤ m :
conclusion
Proof (Lean source)
theorem taylor_polynomial_jet_match {d m : ℕ}
{u : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ}
(hu : ContDiffAt ℝ m u x) {p : MvPolynomial (Fin d) ℝ}
(hp : ∀ y : Fin d → ℝ,
eval y p =
∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ *
iteratedFDeriv ℝ k u x (fun _ => y - x)) :
∀ j ≤ m, ∀ f : Fin j → Fin d,
coordPartial j (fun z => eval z p) f x =
coordPartial j u f x := by
-- Differentiate the finite Taylor polynomial at its center. Higher
-- homogeneous terms vanish there; symmetry of derivatives at `hu` gives
-- the original ordered coordinate partial for the degree-`j` term.
classical
intro j hj f
let H (k : ℕ) (z : Fin d → ℝ) : ℝ :=
(Nat.factorial k : ℝ)⁻¹ *
iteratedFDeriv ℝ k u x (fun _ => z - x)
have hterm (k : ℕ) : ContDiff ℝ (j : WithTop ℕ∞) (H k) := by
let A := (Nat.factorial k : ℝ)⁻¹ • iteratedFDeriv ℝ k u x
let D : (Fin d → ℝ) →L[ℝ] (Fin k → (Fin d → ℝ)) :=
ContinuousLinearMap.pi (fun _ => id ℝ (Fin d → ℝ))
have h : ContDiff ℝ ⊤ (fun z => A (D (z - x))) :=
A.contDiff.comp (D.contDiff.comp (contDiff_id.sub contDiff_const))
have heq : H k = (fun z => A (D (z - x))) := by
funext z
simp [H, A, D, smul_eq_mul]
rw [heq]
exact h.of_le le_top
have hsum :
coordPartial j (fun z => eval z p) f x =
∑ k ∈ range (m + 1), coordPartial j (H k) f x := by
unfold coordPartial
have heq : (fun z => eval z p) =
(fun z => ∑ k ∈ range (m + 1), H k z) := by
funext z
exact hp z
rw [heq, iteratedFDeriv_fun_sum_apply]
· change (ContinuousMultilinearMap.applyAddHom
(fun i => single (f i) (1 : ℝ)))
(∑ k ∈ range (m + 1), iteratedFDeriv ℝ j (H k) x) = _
simp only [map_sum]
rfl
· intro k hk
exact (hterm k).contDiffAt
rw [hsum]
have hjmem : j ∈ range (m + 1) := Finset.mem_range.mpr (Nat.lt_succ_of_le hj)
have hsingle :
(∑ k ∈ range (m + 1), coordPartial j (H k) f x) =
coordPartial j (H j) f x := by
apply Finset.sum_eq_single j
· intro k hk hkj
rcases lt_or_gt_of_ne hkj with hlt | hgt
· exact homogeneous_taylor_jet_above_degree hlt u x f
· exact homogeneous_taylor_jet_below_degree hgt u x f
· intro hnot
exact (hnot hjmem).elim
rw [hsingle]
have hjm : (j : WithTop ℕ∞) ≤ (m : WithTop ℕ∞) := by exact_mod_cast hj
exact homogeneous_taylor_jet_at_degree (hu.of_le hjm) f
1 supporting declaration (lemmas, instances)
-
taylor_expression_polynomialtheorem — The order-m Taylor expression at a point is the evaluation of a multivariate polynomial with degree at most m in each coordinate.hypothesesconclusion∃ p : MvPolynomial (Fin d) ℝ,conclusion 1i :p.degreeOf i ≤ mconclusion 2y :Fin d → ℝeval y p= ∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => y - x)Proof (Lean source)
theorem taylor_expression_polynomial (d m : ℕ) (u : (Fin d → ℝ) → ℝ) (x : Fin d → ℝ) : ∃ p : MvPolynomial (Fin d) ℝ, (∀ i, p.degreeOf i ≤ m) ∧ ∀ y : Fin d → ℝ, eval y p = ∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => y - x) := by classical let q : ℕ → MvPolynomial (Fin d) ℝ := fun k => ∑ f : Fin k → Fin d, C ((Nat.factorial k : ℝ)⁻¹ * coordPartial k u f x) * ∏ a : Fin k, (MvPolynomial.X (f a) - C (x (f a))) have hfactor : ∀ a : Fin d, (MvPolynomial.X a - C (x a)).totalDegree ≤ 1 := by intro a have h := MvPolynomial.totalDegree_add (MvPolynomial.X a : MvPolynomial (Fin d) ℝ) (-C (x a)) simpa only [sub_eq_add_neg] using le_trans h (by simp : max (MvPolynomial.X a : MvPolynomial (Fin d) ℝ).totalDegree (-C (x a)).totalDegree ≤ 1) have hq (k : ℕ) : (q k).totalDegree ≤ k := by unfold q apply le_trans (MvPolynomial.totalDegree_finsetSum _ _) (Finset.sup_le fun f _ => ?_) apply le_trans (MvPolynomial.totalDegree_mul _ _) have hc : (C ((Nat.factorial k : ℝ)⁻¹ * coordPartial k u f x) : MvPolynomial (Fin d) ℝ).totalDegree = 0 := MvPolynomial.totalDegree_C _ rw [hc, zero_add] apply le_trans (MvPolynomial.totalDegree_finsetProd _ _) simpa using (Finset.sum_le_sum (s := univ) (fun a _ => hfactor (f a))) refine ⟨∑ k ∈ range (m + 1), q k, ?_, ?_⟩ · intro i apply le_trans (MvPolynomial.degreeOf_le_totalDegree _ _) apply le_trans (MvPolynomial.totalDegree_finsetSum _ _) apply Finset.sup_le intro k hk exact (hq k).trans (Nat.lt_succ_iff.mp (Finset.mem_range.mp hk)) · intro y simp only [MvPolynomial.eval_sum] apply Finset.sum_congr rfl intro k hk simp only [q, MvPolynomial.eval_sum, MvPolynomial.eval_mul, MvPolynomial.eval_C, MvPolynomial.eval_prod, MvPolynomial.eval_sub, MvPolynomial.eval_X] rw [diagonal_derivative_coordinate_expansion u x (y - x)] simp_rw [Pi.sub_apply] simp only [Finset.mul_sum] apply Finset.sum_congr rfl intro f hf ring
JetSymmetry 1 core · 0 supporting At a point of finite C^k regularity over the reals, the order-k iterated Fréchet derivative is invariant under permutations of its directions. ★ finite_order_iteratedFDeriv_perm
Finite-order symmetry of coordinate jets
At a point of finite C^k regularity over the reals, the order-k iterated
Fréchet derivative is invariant under permutations of its directions. This is
the symmetry needed to recover ordered coordinate partials from homogeneous
Taylor terms without assuming analyticity.
theorem finite_order_iteratedFDeriv_perm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
If a function is k times continuously differentiable at a point, then for any k directions and any permutation of them, the order-k derivative at that point takes the same value on the reordered directions as on the original ones.
Formal statement
hypotheses
conclusion
iteratedFDeriv ℝ k u x (v ∘ σ) = iteratedFDeriv ℝ k u x v
Proof (Lean source)
theorem finite_order_iteratedFDeriv_perm {d k : ℕ}
{u : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ}
(hu : ContDiffAt ℝ k u x) (v : Fin k → (Fin d → ℝ))
(σ : Perm (Fin k)) :
iteratedFDeriv ℝ k u x (v ∘ σ) = iteratedFDeriv ℝ k u x v := by
cases k with
| zero =>
have hσ : σ = 1 := Subsingleton.elim σ 1
simp [hσ]
| succ n =>
let S : Submonoid (Perm (Fin (n + 1))) :=
{ carrier := {τ | ∀ w : Fin (n + 1) → (Fin d → ℝ),
iteratedFDeriv ℝ (n + 1) u x (w ∘ τ) =
iteratedFDeriv ℝ (n + 1) u x w}
one_mem' := by simp
mul_mem' := by
intro τ ρ hτ hρ w
calc
iteratedFDeriv ℝ (n + 1) u x
(w ∘ (τ * ρ : Perm (Fin (n + 1)))) =
iteratedFDeriv ℝ (n + 1) u x ((w ∘ τ) ∘ ρ) := by
congr 1
_ = iteratedFDeriv ℝ (n + 1) u x (w ∘ τ) := hρ (w ∘ τ)
_ = iteratedFDeriv ℝ (n + 1) u x w := hτ w }
have hgen : (Set.range fun i : Fin n => swap i.castSucc i.succ) ⊆ S := by
rintro τ ⟨i, rfl⟩
exact fun w => finite_order_iteratedFDeriv_adjacent_swap hu w i
have htop : S = ⊤ := by
apply top_unique
rw [← Equiv.Perm.mclosure_swap_castSucc_succ n]
exact Submonoid.closure_le.mpr hgen
have hσ : σ ∈ S := by rw [htop]; trivial
exact hσ v
JetSymmetryAdjacent 1 core · 0 supporting The leading-pair swap extends to any pair of consecutive derivative slots. ★ finite_order_iteratedFDeriv_adjacent_swap
Adjacent swaps in finite-order jets
The leading-pair swap extends to any pair of consecutive derivative slots. This is the analytic step needed before using finite permutation generators.
theorem finite_order_iteratedFDeriv_adjacent_swap reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
If a function is n + 1 times continuously differentiable at a point, then for any n + 1 directions and any position i among the first n, exchanging the directions at positions i and i + 1 leaves the order-(n + 1) derivative at that point unchanged.
Formal statement
hypotheses
hu :
ContDiffAt ℝ (n + 1) u x
i :
Fin n
conclusion
iteratedFDeriv ℝ (n + 1) u x (v ∘ swap i.castSucc i.succ)
= iteratedFDeriv ℝ (n + 1) u x v
Proof (Lean source)
theorem finite_order_iteratedFDeriv_adjacent_swap {d n : ℕ}
{u : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ}
(hu : ContDiffAt ℝ (n + 1) u x)
(v : Fin (n + 1) → (Fin d → ℝ)) (i : Fin n) :
iteratedFDeriv ℝ (n + 1) u x
(v ∘ swap i.castSucc i.succ) =
iteratedFDeriv ℝ (n + 1) u x v := by
-- The first two positions are `finite_order_iteratedFDeriv_front_swap`.
-- For later positions, peel off the first direction with
-- `iteratedFDeriv_succ_apply_left'`. The induction hypothesis identifies
-- the two scalar evaluations of the lower jet near `x`, so their derivatives
-- at `x` agree.
induction n generalizing x with
| zero => exact i.elim0
| succ n ih =>
cases i using Fin.cases with
| zero =>
rcases Fin.exists_cons v with ⟨a, w, rfl⟩
rcases Fin.exists_cons w with ⟨b, r, rfl⟩
change (iteratedFDeriv ℝ (n + 2) u x)
(vecCons a (vecCons b r) ∘ swap 0 1) = _
rw [Matrix.cons_cons_comp_swap_zero_one]
simpa [cons, vecCons] using
finite_order_iteratedFDeriv_front_swap hu b a r
| succ j =>
rcases Fin.exists_cons v with ⟨a, w, rfl⟩
have hlow : ContDiffAt ℝ (n + 1) u x := hu.of_le (by norm_cast; omega)
have hnear :
(fun y => (iteratedFDeriv ℝ (n + 1) u y)
(w ∘ swap j.castSucc j.succ)) =ᶠ[nhds x]
(fun y => (iteratedFDeriv ℝ (n + 1) u y) w) := by
filter_upwards [hlow.eventually (by simp)] with y hy
exact ih hy w j
have hd : DifferentiableAt ℝ (iteratedFDeriv ℝ (n + 1) u) x :=
hu.differentiableAt_iteratedFDeriv (by norm_cast; omega)
have hidx : (succ j).castSucc = succ j.castSucc := Fin.ext rfl
rw [hidx]
change (iteratedFDeriv ℝ (n + 2) u x)
(vecCons a w ∘ swap (succ j.castSucc) (succ j.succ)) = _
rw [← Matrix.cons_swap]
rw [hd.iteratedFDeriv_succ_apply_left', hd.iteratedFDeriv_succ_apply_left']
exact congrArg (fun L : (Fin d → ℝ) →L[ℝ] ℝ => L a) (hnear.fderiv_eq)
JetSymmetryTwo 1 core · 3 supporting Finite C^(n+2) regularity makes the order-n derivative a C² map. ★ finite_order_iteratedFDeriv_front_swap
Second derivatives of finite jets
Finite C^(n+2) regularity makes the order-n derivative a C² map.
The library's second-derivative symmetry then applies to that lower jet.
An evaluation bridge identifies its second derivative with the first two
slots of the order-n+2 derivative of the original map.
theorem finite_order_iteratedFDeriv_front_swap reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
If a function is n + 2 times continuously differentiable at a point, then for any two leading directions and any n further directions, exchanging the two leading directions leaves the order-(n + 2) derivative at that point unchanged.
Formal statement
Proof (Lean source)
theorem finite_order_iteratedFDeriv_front_swap {d n : ℕ}
{u : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ}
(hu : ContDiffAt ℝ (n + 2) u x)
(a b : Fin d → ℝ) (r : Fin n → (Fin d → ℝ)) :
iteratedFDeriv ℝ (n + 2) u x (cons a (cons b r)) =
iteratedFDeriv ℝ (n + 2) u x (cons b (cons a r)) := by
calc
_ = (iteratedFDeriv ℝ 2 (iteratedFDeriv ℝ n u) x ![a, b]) r :=
(iteratedFDeriv_two_front_as_second_jet u x a b r).symm
_ = (iteratedFDeriv ℝ 2 (iteratedFDeriv ℝ n u) x ![b, a]) r := by
simpa [iteratedFDeriv_two_apply] using
congrArg (fun L => L r) (finite_order_lower_jet_second_symmetric hu a b)
_ = _ := iteratedFDeriv_two_front_as_second_jet u x b a r
3 supporting declarations (lemmas, instances)
-
finite_order_lower_jet_contDiffAt_twotheorem — The order-n iterated derivative of a C^(n+2) real function is C² at the same point.Proof (Lean source)
theorem finite_order_lower_jet_contDiffAt_two {d n : ℕ} {u : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ} (hu : ContDiffAt ℝ (n + 2) u x) : ContDiffAt ℝ 2 (iteratedFDeriv ℝ n u) x := by exact hu.iteratedFDeriv_right (m := 2) (i := n) (by exact le_of_eq (add_comm (2 : WithTop ℕ∞) (n : WithTop ℕ∞))) -
finite_order_lower_jet_second_symmetrictheorem — At a C^(n+2) point, the second derivative of the order-n jet is symmetric in its two input directions.hypothesesconclusionProof (Lean source)
theorem finite_order_lower_jet_second_symmetric {d n : ℕ} {u : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ} (hu : ContDiffAt ℝ (n + 2) u x) (a b : Fin d → ℝ) : fderiv ℝ (fderiv ℝ (iteratedFDeriv ℝ n u)) x a b = fderiv ℝ (fderiv ℝ (iteratedFDeriv ℝ n u)) x b a := by exact (finite_order_lower_jet_contDiffAt_two hu).isSymmSndFDerivAt (by norm_num) a b -
iteratedFDeriv_two_front_as_second_jettheorem — Evaluating the second derivative of the order-n jet on two directions and then on n more directions equals the order-n+2 derivative evaluated on that concatenated list.hypothesesconclusion(iteratedFDeriv ℝ 2 (iteratedFDeriv ℝ n u) x ![a, b]) rProof (Lean source)
theorem iteratedFDeriv_two_front_as_second_jet {d n : ℕ} (u : (Fin d → ℝ) → ℝ) (x a b : Fin d → ℝ) (r : Fin n → (Fin d → ℝ)) : (iteratedFDeriv ℝ 2 (iteratedFDeriv ℝ n u) x ![a, b]) r = iteratedFDeriv ℝ (n + 2) u x (cons a (cons b r)) := by -- Both sides are obtained by twice applying -- `iteratedFDeriv_succ_apply_left`; unfold the curry equivalences and -- commute evaluation at the fixed trailing directions with `fderiv`. let L : ((Fin d → ℝ) [×(n + 1)]→L[ℝ] ℝ) ≃ₗᵢ[ℝ] ((Fin d → ℝ) [×1]→L[ℝ] ((Fin d → ℝ) [×n]→L[ℝ] ℝ)) := (continuousMultilinearCurryLeftEquiv ℝ (fun _ : Fin (n + 1) => Fin d → ℝ) ℝ).trans (continuousMultilinearCurryFin1 ℝ (Fin d → ℝ) ((Fin d → ℝ) [×n]→L[ℝ] ℝ)).symm have h : iteratedFDeriv ℝ 1 (iteratedFDeriv ℝ n u) = L ∘ iteratedFDeriv ℝ (n + 1) u := by funext y ext v r rw [iteratedFDeriv_one_apply] simp [L, iteratedFDeriv_succ_apply_left] change ((fderiv ℝ (iteratedFDeriv ℝ 1 (iteratedFDeriv ℝ n u)) x) a) ![b] r = ((fderiv ℝ (iteratedFDeriv ℝ (n + 1) u) x) a) (cons b r) rw [h, L.comp_fderiv] rfl
Legendre 3 core · 3 supporting The orthonormal entries on the interval [-1/2,1/2] are 1, sqrt(12)t, and sqrt(5)(6t²-1/2). ★ monomial_inverse_legendre
Degree-two Legendre entries and explicit inverse coefficients
The orthonormal entries on the interval [-1/2,1/2] are 1, sqrt(12)t, and sqrt(5)(6t²-1/2). These are the degree-zero through degree-two standard Legendre polynomials at 2t multiplied by sqrt(2k+1). See the primary source https://dlmf.nist.gov/18.3 and its Rodrigues representation https://dlmf.nist.gov/18.5#ii. Only these three entries are needed; the default value outside this degree range is never used by the API.
The inverse formulas are 1 = ell₀(t), h t = h ell₁(t)/sqrt(12), and (h t)² = h² ell₀(t)/12 + h² ell₂(t)/(6 sqrt(5)). They are derived here independently, without importing any research module or its forward affine change-of-basis theorem.
def legendreEntry reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The normalized Legendre entry of degree k at a point t is 1 for degree zero, the square root of 12 times t for degree one, the square root of 5 times (6 t² − 1/2) for degree two, and zero for every higher degree.
def inverseEntry reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The inverse Legendre entry at scale h for a monomial degree k and a Legendre degree j is 1 when both degrees are zero, h over the square root of 12 when both are one, h² / 12 for degrees two and zero, h² over 6 times the square root of 5 when both are two, and zero otherwise.
theorem monomial_inverse_legendre reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a degree k at most two and any real scale h and point t, the monomial (h t)^k equals the sum over the first three Legendre degrees of the inverse entry times the normalized Legendre entry at t.
Formal statement
hypotheses
k :
ℕ
hk :
k ≤ 2
h t :
ℝ
conclusion
Proof (Lean source)
theorem monomial_inverse_legendre (k : ℕ) (hk : k ≤ 2) (h t : ℝ) :
(h * t) ^ k = ∑ j : Fin 3, inverseEntry h k j.val * legendreEntry j.val t := by
have hs12 : sqrt 12 ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (by norm_num))
have hs5 : sqrt 5 ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (by norm_num))
interval_cases k <;>
simp [Fin.sum_univ_succ, inverseEntry, legendreEntry]
· field_simp
· field_simp
ring
3 supporting declarations (lemmas, instances)
-
inverseEntry_abovetheorem — For any scale and a monomial degree k and a Legendre degree j with j strictly larger than k, the inverse Legendre entry is zero.Proof (Lean source)
theorem inverseEntry_above (h : ℝ) (k j : ℕ) (hj : k < j) : inverseEntry h k j = 0 := by unfold inverseEntry split_ifs <;> first | omega | rfl -
inverseEntry_abs_letheorem — For a scale h that is positive and a monomial degree k and a Legendre degree j with k at most two, the inverse Legendre entry is at most h to the power k in absolute value.Proof (Lean source)
theorem inverseEntry_abs_le (h : ℝ) (hh : 0 < h) (k j : ℕ) (hk : k ≤ 2) : |inverseEntry h k j| ≤ h ^ k := by have hs12 : 1 ≤ sqrt 12 := Real.one_le_sqrt.mpr (by norm_num) have hs5 : 1 ≤ sqrt 5 := Real.one_le_sqrt.mpr (by norm_num) have hs6 : 1 ≤ 6 * sqrt 5 := by linarith unfold inverseEntry split_ifs with h0 h1 h2 h3 · rcases h0 with ⟨rfl, rfl⟩ simp · rcases h1 with ⟨rfl, rfl⟩ simp only [pow_one, abs_div, abs_of_pos hh, abs_of_nonneg (Real.sqrt_nonneg _)] exact div_le_self hh.le hs12 · rcases h2 with ⟨rfl, rfl⟩ rw [abs_of_nonneg (div_nonneg (sq_nonneg h) (by norm_num))] exact div_le_self (sq_nonneg h) (by norm_num) · rcases h3 with ⟨rfl, rfl⟩ rw [abs_of_nonneg (div_nonneg (sq_nonneg h) (by positivity))] exact div_le_self (sq_nonneg h) hs6 · simpa using pow_nonneg hh.le k -
legendreEntry_abs_letheorem — For a degree k at most two and a point t at most one half in absolute value, the normalized Legendre entry is at most the square root of 5 in absolute value.Proof (Lean source)
theorem legendreEntry_abs_le (k : ℕ) (hk : k ≤ 2) (t : ℝ) (ht : |t| ≤ 1 / 2) : |legendreEntry k t| ≤ sqrt 5 := by have hs5 : 1 ≤ sqrt 5 := Real.one_le_sqrt.mpr (by norm_num) have hs12_nonneg := Real.sqrt_nonneg 12 have hs5_nonneg := Real.sqrt_nonneg 5 have hs12_sq : sqrt 12 ^ 2 = 12 := Real.sq_sqrt (by norm_num) have hs5_sq : sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num) interval_cases k · simp [legendreEntry, Real.one_le_sqrt] · simp only [legendreEntry, show ¬ (1 : ℕ) = 0 by omega, ↓reduceIte, abs_mul, abs_of_nonneg hs12_nonneg] calc sqrt 12 * |t| ≤ sqrt 12 * (1 / 2) := mul_le_mul_of_nonneg_left ht hs12_nonneg _ ≤ sqrt 5 := by nlinarith · have ht2 : t ^ 2 ≤ 1 / 4 := by rcases abs_le.mp ht with ⟨htlo, hthi⟩ nlinarith [mul_nonneg (by linarith : 0 ≤ 1 / 2 - t) (by linarith : 0 ≤ 1 / 2 + t)] have hp : |6 * t ^ 2 - 1 / 2| ≤ 1 := by apply abs_le.mpr constructor <;> nlinarith [sq_nonneg t] simp only [legendreEntry, show ¬ (2 : ℕ) = 0 by omega, show ¬ (2 : ℕ) = 1 by omega, ↓reduceIte, abs_mul, abs_of_nonneg hs5_nonneg] simpa using mul_le_mul_of_nonneg_left hp hs5_nonneg
LineInterior 1 core · 1 supporting On every compact initial subsegment, the restriction of a C^m function is C^m and its top line derivative inherits the coordinate Hölder modulus. ★ segment_line_topHolder_before_endpoint
Line calculus before a cube segment reaches its boundary
On every compact initial subsegment, the restriction of a C^m function is
C^m and its top line derivative inherits the coordinate Hölder modulus.
theorem segment_line_topHolder_before_endpoint reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a function that is m times continuously differentiable on the closed normalized cube and satisfies the top-order Hölder condition with exponent s and constant L, where s is positive and L is nonnegative, take a starting point x in the open cube, an end point y in the closed cube, and a time t that is strictly less than one. Then for any two times r and w between 0 and t, the m-th derivative of the function restricted to the segment from x to y changes between those times by at most (d + 1)^m times L times the segment length to the power m + s times the time difference to the power s.
Formal statement
hypotheses
d m :
ℕ
s L :
ℝ
u :
(Fin d → ℝ) → ℝ
hu :
ContDiffOn ℝ m u (cube d)
hs :
0 < s
hL :
0 ≤ L
hholder :
TopHolder d m s L u
x y :
Fin d → ℝ
hx :
x ∈ openCube d
hy :
y ∈ cube d
t :
ℝ
ht1 :
t < 1
r w :
ℝ
hr :
r ∈ Icc 0 t
hw :
w ∈ Icc 0 t
conclusion
|iteratedDeriv m (fun q : ℝ => u (x + q • (y - x))) r
- iteratedDeriv m (fun q : ℝ => u (x + q • (y - x))) w|
≤ ((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) * |r - w| ^ s
Proof (Lean source)
theorem segment_line_topHolder_before_endpoint {d m : ℕ} {s L : ℝ}
{u : (Fin d → ℝ) → ℝ} (hu : ContDiffOn ℝ m u (cube d))
(hs : 0 < s) (hL : 0 ≤ L) (hholder : TopHolder d m s L u)
{x y : Fin d → ℝ} (hx : x ∈ openCube d) (hy : y ∈ cube d)
{t : ℝ} (ht1 : t < 1)
{r w : ℝ} (hr : r ∈ Icc 0 t) (hw : w ∈ Icc 0 t) :
|iteratedDeriv m (fun q : ℝ => u (x + q • (y - x))) r -
iteratedDeriv m (fun q : ℝ => u (x + q • (y - x))) w| ≤
((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) * |r - w| ^ s := by
-- Apply `segment_iteratedDeriv_eq_diagonal` at `r,w`, then
-- `topHolder_diagonal_derivative`; use
-- `‖r • (y-x) - w • (y-x)‖ = |r-w| * ‖y-x‖`.
have hrr : r ∈ Ico (0 : ℝ) 1 := ⟨hr.1, lt_of_le_of_lt hr.2 ht1⟩
have hww : w ∈ Ico (0 : ℝ) 1 := ⟨hw.1, lt_of_le_of_lt hw.2 ht1⟩
rw [segment_iteratedDeriv_eq_diagonal hu hx hy hrr m le_rfl,
segment_iteratedDeriv_eq_diagonal hu hx hy hww m le_rfl]
have hrc : x + r • (y - x) ∈ cube d := by
have h := segment_mem_openCube hx hy hrr
intro i
exact ⟨le_of_lt (h i (Set.mem_univ i)).1, le_of_lt (h i (Set.mem_univ i)).2⟩
have hwc : x + w • (y - x) ∈ cube d := by
have h := segment_mem_openCube hx hy hww
intro i
exact ⟨le_of_lt (h i (Set.mem_univ i)).1, le_of_lt (h i (Set.mem_univ i)).2⟩
have hbound := topHolder_diagonal_derivative u hL hholder
(x + r • (y - x)) (x + w • (y - x)) (y - x) hrc hwc
have hdiff : (x + r • (y - x)) - (x + w • (y - x)) =
(r - w) • (y - x) := by
rw [sub_smul]
abel
rw [hdiff, norm_smul, Real.norm_eq_abs] at hbound
calc
_ ≤ ((d : ℝ) + 1) ^ m * L *
(|r - w| * ‖y - x‖) ^ s * ‖y - x‖ ^ m := hbound
_ = ((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) *
|r - w| ^ s := by
rw [Real.mul_rpow (abs_nonneg _) (norm_nonneg _),
Real.rpow_add_of_nonneg (norm_nonneg _) (Nat.cast_nonneg _) (le_of_lt hs),
Real.rpow_natCast]
ring
1 supporting declaration (lemmas, instances)
-
segment_line_contDiffOn_before_endpointtheorem — A line from an interior cube point toward a closed-cube point is C^m on each closed initial subsegment ending strictly before the final endpoint.hypothesesd m :ℕ(Fin d → ℝ) → ℝhu :ContDiffOn ℝ m u (cube d)x y :Fin d → ℝhx :x ∈ openCube dhy :y ∈ cube dt :ℝht1 :t < 1conclusionContDiffOn ℝ m (fun r : ℝ => u (x + r • (y - x))) (Icc 0 t)Proof (Lean source)
theorem segment_line_contDiffOn_before_endpoint {d m : ℕ} {u : (Fin d → ℝ) → ℝ} (hu : ContDiffOn ℝ m u (cube d)) {x y : Fin d → ℝ} (hx : x ∈ openCube d) (hy : y ∈ cube d) {t : ℝ} (ht1 : t < 1) : ContDiffOn ℝ m (fun r : ℝ => u (x + r • (y - x))) (Icc 0 t) := by -- Compose `hu` with the affine line and use `segment_mem_openCube` on -- `Icc 0 t`; the line is smooth in an open neighborhood of every point. have hline : ContDiff ℝ m (fun r : ℝ => x + r • (y - x)) := contDiff_const.add (contDiff_id.smul contDiff_const) have hmaps : Set.MapsTo (fun r : ℝ => x + r • (y - x)) (Icc 0 t) (cube d) := by intro r hr have hro : r ∈ Ico (0 : ℝ) 1 := ⟨hr.1, lt_of_le_of_lt hr.2 ht1⟩ have hri := segment_mem_openCube hx hy hro intro i exact ⟨le_of_lt (hri i (Set.mem_univ i)).1, le_of_lt (hri i (Set.mem_univ i)).2⟩ exact hu.comp hline.contDiffOn hmaps
LineTaylor 1 core · 0 supporting If a function of one real variable is m times continuously differentiable on [a, b] and its m-th derivative is Hölder with exponent s ∈ (0, 1] and constant L, then at every y in [a, b] it differs from its degree-m Taylor ★ line_holder_taylor
One-dimensional Taylor remainder under a Hölder condition on the top derivative
If a function of one real variable is m times continuously differentiable on [a, b] and its m-th derivative is Hölder with exponent s ∈ (0, 1] and constant L, then at every y in [a, b] it differs from its degree-m Taylor polynomial centred at an interior point x by at most C·L·|y − x|^(m + s), with C depending only on m and s. Applied along line segments, this is the calculus step behind the multivariate Hölder–Taylor remainder on the cube.
Main results
* line_holder_taylor — the Taylor remainder bound of order m + s with a constant uniform over
functions, intervals and expansion points.
theorem line_holder_taylor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a derivative order m and an exponent s with s positive, there is a positive constant C such that, for every function of one real variable that is m times continuously differentiable on a nondegenerate closed interval and whose m-th derivative changes between any two points of the interval by at most a nonnegative L times their distance to the power s, the function at any point y of the interval differs from its order-m Taylor polynomial centred at any interior point x by at most C times L times the distance from x to y raised to the power m + s.
Formal statement
hypotheses
m :
ℕ
s :
ℝ
hs :
0 < s
conclusion
∃ C : ℝ,
0 < C
conclusion 1
v :
ℝ → ℝ
a b L :
ℝ
a < b
0 ≤ L
ContDiffOn ℝ m v (Set.Icc a b)
(∀ z ∈ Set.Icc a b, ∀ w ∈ Set.Icc a b, |iteratedDeriv m v z - iteratedDeriv m v w| ≤ L * |z - w| ^ s)
x ∈ Set.Ioo a b :
y ∈ Set.Icc a b :
|v y
- ∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v x * (y - x) ^ k|
≤ C * L * |y - x| ^ ((m : ℝ) + s)
Proof (Lean source)
theorem line_holder_taylor (m : ℕ) (s : ℝ) (hs : 0 < s) :
∃ C : ℝ, 0 < C ∧
∀ (v : ℝ → ℝ) (a b L : ℝ),
a < b → 0 ≤ L → ContDiffOn ℝ m v (Icc a b) →
(∀ z ∈ Icc a b, ∀ w ∈ Icc a b,
|iteratedDeriv m v z - iteratedDeriv m v w| ≤ L * |z - w| ^ s) →
∀ x ∈ Ioo a b, ∀ y ∈ Icc a b,
|v y - ∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v x * (y - x) ^ k| ≤
C * L * |y - x| ^ ((m : ℝ) + s) := by
refine ⟨1, by norm_num, ?_⟩
intro v a b L hab hL hv hholder x hx y hy
have hxmem : x ∈ Icc a b := ⟨hx.1.le, hx.2.le⟩
have hbase : ∀ n ≤ m, ∀ z, x ∈ uIcc x z → x ≠ z →
iteratedDerivWithin n v (uIcc x z) x = iteratedDeriv n v x := by
intro n hn z hxz hne
exact iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_uIcc hne)
((hv.contDiffAt (Icc_mem_nhds hx.1 hx.2)).of_le (by exact_mod_cast hn)) hxz
by_cases hxy : x = y
· subst y
have he : 0 < (m : ℝ) + s := by positivity
have hsum : (∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v x * (x - x) ^ k) = v x := by
calc
_ = (Nat.factorial 0 : ℝ)⁻¹ * iteratedDeriv 0 v x * (x - x) ^ 0 := by
apply Finset.sum_eq_single 0
· intro k hk hk0
simp [hk0]
· simp
_ = v x := by simp [iteratedDeriv_zero]
rw [hsum]
simp [Real.zero_rpow (ne_of_gt he)]
have hpos : 0 < |y - x| := abs_pos.mpr (sub_ne_zero.mpr (Ne.symm hxy))
have hseg : uIcc x y ⊆ Icc a b := by
intro z hz
rcases le_total x y with h | h
· rw [Set.uIcc_of_le h] at hz
exact ⟨hxmem.1.trans hz.1, hz.2.trans hy.2⟩
· rw [Set.uIcc_of_ge h] at hz
exact ⟨hy.1.trans hz.1, hz.2.trans hxmem.2⟩
rcases Nat.eq_zero_or_pos m with hm0 | hmpos
· subst m
simpa [iteratedDeriv_zero] using hholder y hy x hxmem
let n := m - 1
have hm : n + 1 = m := Nat.succ_pred_eq_of_pos hmpos
have hcont : ContDiffOn ℝ (n + 1) v (uIcc x y) := by
change ContDiffOn ℝ (↑(n + 1 : ℕ)) v (uIcc x y)
rw [hm]
exact hv.mono hseg
obtain ⟨ξ, hξ, hrem⟩ :=
taylor_mean_remainder_lagrange_iteratedDeriv (f := v) (x := y) (x₀ := x)
(n := n) hxy hcont
have hξmem : ξ ∈ Icc a b := hseg (Set.uIoo_subset_uIcc_self hξ)
have hξdist : |ξ - x| ≤ |y - x| := by
rcases le_total x y with h | h
· rw [Set.uIoo_of_le h] at hξ
rw [abs_of_nonneg (sub_nonneg.mpr hξ.1.le),
abs_of_nonneg (sub_nonneg.mpr h)]
linarith [hξ.2]
· rw [Set.uIoo_of_ge h] at hξ
rw [abs_of_nonpos (sub_nonpos.mpr hξ.2.le),
abs_of_nonpos (sub_nonpos.mpr h)]
linarith [hξ.1]
have hpow : |ξ - x| ^ s ≤ |y - x| ^ s :=
Real.rpow_le_rpow (abs_nonneg _) hξdist hs.le
have htop : |iteratedDeriv m v ξ - iteratedDeriv m v x| ≤
L * |y - x| ^ s :=
(hholder ξ hξmem x hxmem).trans (mul_le_mul_of_nonneg_left hpow hL)
have hpolyM :
(∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v x * (y - x) ^ k) =
(∑ k ∈ range (n + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v x * (y - x) ^ k) +
(Nat.factorial m : ℝ)⁻¹ * iteratedDeriv m v x * (y - x) ^ m := by
rw [hm, Finset.sum_range_succ]
have hpolyN' : taylorWithinEval v n (uIcc x y) x y =
∑ k ∈ range (n + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v x * (y - x) ^ k := by
rw [taylor_within_apply]
apply Finset.sum_congr rfl
intro k hk
have hk' : k ≤ m := by
have hk'' : k ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk)
omega
rw [hbase k hk' y Set.left_mem_uIcc hxy]
simp only [smul_eq_mul]
ring
have hdiff :
v y - (∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v x * (y - x) ^ k) =
(iteratedDeriv m v ξ - iteratedDeriv m v x) /
(Nat.factorial m : ℝ) * (y - x) ^ m := by
rw [hpolyM, ← hpolyN', sub_add_eq_sub_sub, hrem]
simp only [hm]
ring
rw [hdiff]
have hfac : 1 ≤ (Nat.factorial m : ℝ) := by exact_mod_cast Nat.factorial_pos m
calc
|(iteratedDeriv m v ξ - iteratedDeriv m v x) / (Nat.factorial m : ℝ) *
(y - x) ^ m| =
|iteratedDeriv m v ξ - iteratedDeriv m v x| /
(Nat.factorial m : ℝ) * |y - x| ^ m := by
rw [abs_mul, abs_div, abs_pow, abs_of_nonneg (by linarith : (0 : ℝ) ≤ m.factorial)]
_ ≤ L * |y - x| ^ s / (Nat.factorial m : ℝ) * |y - x| ^ m := by
gcongr
_ ≤ L * |y - x| ^ s * |y - x| ^ m := by
gcongr
exact div_le_self (mul_nonneg hL (Real.rpow_nonneg (abs_nonneg _) _)) hfac
_ = 1 * L * |y - x| ^ ((m : ℝ) + s) := by
have hp : |y - x| ^ s * |y - x| ^ m =
|y - x| ^ ((m : ℝ) + s) := by
rw [← Real.rpow_natCast, ← Real.rpow_add hpos]
congr 1
ring
calc
_ = L * (|y - x| ^ s * |y - x| ^ m) := by ring
_ = L * |y - x| ^ ((m : ℝ) + s) := by rw [hp]
_ = _ := by ring
PolynomialControl 1 core · 0 supporting A fixed tensor grid controls every coordinate derivative of a polynomial of bounded coordinate degree throughout the normalized cube. ★ tensor_polynomial_deriv_bound
Derivatives of bounded tensor-grid polynomials
A fixed tensor grid controls every coordinate derivative of a polynomial of bounded coordinate degree throughout the normalized cube. This is the finite-dimensional polynomial step in fixed-cube interpolation.
theorem tensor_polynomial_deriv_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension and a degree m, there is a positive constant C such that every multivariate polynomial of degree at most m in each variable that is bounded in absolute value by a nonnegative B at every point of the fixed tensor grid has all its coordinate partial derivatives of order at most m bounded in absolute value by C times B throughout the closed normalized cube.
Formal statement
hypotheses
d m :
ℕ
conclusion
∃ C : ℝ,
0 < C
conclusion 1
|coordPartial j (fun z => eval z p) f x| ≤ C * B
Proof (Lean source)
theorem tensor_polynomial_deriv_bound (d m : ℕ) :
∃ C : ℝ, 0 < C ∧
∀ (p : MvPolynomial (Fin d) ℝ) (B : ℝ),
0 ≤ B → (∀ i, p.degreeOf i ≤ m) →
(∀ b : Fin d → Fin (m + 1),
|eval
(tensorGridPoint b) p| ≤ B) →
∀ j ≤ m, ∀ f : Fin j → Fin d, ∀ x ∈ cube d,
|coordPartial j (fun z => eval z p) f x| ≤ C * B := by
classical
obtain ⟨C₀, hC₀, hcoeff⟩ := tensor_coefficient_bound d m
obtain ⟨M, hM₀, hM⟩ := tensor_monomial_deriv_uniform d m
let A := Fin d → Fin (m + 1)
have hcard : 0 < Fintype.card A := Fintype.card_pos_iff.mpr inferInstance
refine ⟨(Fintype.card A : ℝ) * C₀ * (M + 1), by positivity, ?_⟩
intro p B hB hdeg hgrid j hj f x hx
let v : Fin j → (Fin d → ℝ) := fun k => single (f k) (1 : ℝ)
have hv : ‖v‖ ≤ (1 : ℝ) := by
apply (pi_norm_le_iff_of_nonneg (by positivity)).2
intro k
change ‖(single (f k) (1 : ℝ) : Fin d → ℝ)‖ ≤ 1
rw [Pi.norm_single]
norm_num
have hmono (a : A) :
|(iteratedFDeriv ℝ j (fun z : Fin d → ℝ =>
eval z (monomial (tensorExponent a) (1 : ℝ))) x) v| ≤
M := by
rw [← Real.norm_eq_abs]
calc
_ ≤ ‖iteratedFDeriv ℝ j (fun z : Fin d → ℝ =>
eval z (monomial (tensorExponent a) (1 : ℝ))) x‖ *
(1 : ℝ) ^ j :=
(iteratedFDeriv ℝ j (fun z : Fin d → ℝ =>
eval z
(monomial (tensorExponent a) (1 : ℝ))) x).le_opNorm_mul_pow_of_le hv
_ ≤ M := by simpa using hM a j hj x hx
have hc : ∀ a : A, |tensorCoeffs (D := m) p a| ≤ C₀ * B :=
hcoeff p B hB hdeg hgrid
calc
|coordPartial j (fun z => eval z p) f x| =
|∑ a : A, tensorCoeffs (D := m) p a *
(iteratedFDeriv ℝ j (fun z : Fin d → ℝ =>
eval z (monomial (tensorExponent a) (1 : ℝ))) x) v| := by
rw [coordPartial, tensor_eval_sum d m p hdeg, tensor_eval_sum_deriv p x]
simp [v, smul_eq_mul]
rfl
_ ≤ ∑ a : A, |tensorCoeffs (D := m) p a| *
|(iteratedFDeriv ℝ j (fun z : Fin d → ℝ =>
eval z (monomial (tensorExponent a) (1 : ℝ))) x) v| := by
calc
_ ≤ ∑ a : A, |tensorCoeffs (D := m) p a *
(iteratedFDeriv ℝ j (fun z : Fin d → ℝ =>
eval z (monomial (tensorExponent a) (1 : ℝ))) x) v| :=
Finset.abs_sum_le_sum_abs _ _
_ = _ := by simp only [abs_mul]
_ ≤ ∑ _a : A, (C₀ * B) * M := by
apply Finset.sum_le_sum
intro a ha
exact (mul_le_mul_of_nonneg_right (hc a) (abs_nonneg _)).trans
(mul_le_mul_of_nonneg_left (hmono a) (mul_nonneg (le_of_lt hC₀) hB))
_ ≤ ((Fintype.card A : ℝ) * C₀ * (M + 1)) * B := by
simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
calc
(Fintype.card A : ℝ) * ((C₀ * B) * M) =
((Fintype.card A : ℝ) * C₀ * B) * M := by ring
_ ≤ ((Fintype.card A : ℝ) * C₀ * B) * (M + 1) :=
mul_le_mul_of_nonneg_left (by linarith)
(mul_nonneg (mul_nonneg (by positivity) (le_of_lt hC₀)) hB)
_ = _ := by ring
Prefix 1 core · 1 supporting The sorted list of repeated coordinates identifies each word position with the half-open interval between consecutive cumulative coordinate counts. ★ sortedWord_eq_iff_prefix
Sorted coordinate words and prefix intervals
The sorted list of repeated coordinates identifies each word position with the half-open interval between consecutive cumulative coordinate counts. This purely combinatorial bridge permits identification with prefix-based coordinate partial definitions, independently of the Taylor conversion.
theorem sortedWord_eq_iff_prefix reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a vector of coordinate counts, a position r in its sorted word, and a coordinate i, the sorted word has coordinate i at position r exactly when r is at least the sum of the counts of the coordinates before i and strictly less than that sum plus the count of i.
Formal statement
hypotheses
conclusion
sortedWord κ r = i ↔ (∑ j ∈ Finset.univ.filter (fun j => j < i), κ j) ≤ r.val ∧
r.val < (∑ j ∈ Finset.univ.filter (fun j => j < i), κ j) + κ i
Proof (Lean source)
theorem sortedWord_eq_iff_prefix {d : ℕ} (κ : Fin d → ℕ)
(r : Fin (multiOrder κ)) (i : Fin d) :
sortedWord κ r = i ↔
(∑ j ∈ Finset.univ.filter (fun j => j < i), κ j) ≤ r.val ∧
r.val < (∑ j ∈ Finset.univ.filter (fun j => j < i), κ j) + κ i := by
classical
induction d with
| zero => exact elim0 i
| succ d ih =>
let κ' : Fin d → ℕ := fun j => κ j.succ
have horder : multiOrder κ = κ 0 + multiOrder κ' := by
exact Fin.sum_univ_succ κ
have hlist : countList κ =
List.replicate (κ 0) 0 ++ (countList κ').map succ := by
simp only [countList, List.ofFn_succ, List.flatten_cons,
List.map_flatten, List.map_ofFn]
simp [κ', Function.comp_def]
have hprefix (j : Fin d) :
(∑ k ∈ Finset.univ.filter (fun k => k < j.succ), κ k) =
κ 0 + ∑ k ∈ Finset.univ.filter (fun k => k < j), κ' k := by
simp only [Finset.sum_filter]
rw [Fin.sum_univ_succ]
simp [κ', Fin.succ_lt_succ_iff]
by_cases hr : r.val < κ 0
· have hword : sortedWord κ r = 0 := by
simp only [sortedWord, List.get_eq_getElem]
simp only [hlist]
rw [List.getElem_append_left (by simpa using hr)]
exact List.getElem_replicate _
rw [hword]
refine Fin.cases ?_ (fun j => ?_) i
· simp [hr]
· rw [hprefix]
have hne : (0 : Fin (d + 1)) ≠ j.succ := by
intro h
have := congrArg val h
simp only [Fin.val_zero, Fin.val_succ] at this
omega
simp only [hne, false_iff]
omega
· have htail : r.val - κ 0 < multiOrder κ' := by
have := r.isLt
simp only [horder] at this
omega
let r' : Fin (multiOrder κ') := ⟨r.val - κ 0, htail⟩
have hword : sortedWord κ r = (sortedWord κ' r').succ := by
simp only [sortedWord, List.get_eq_getElem]
simp only [hlist]
rw [List.getElem_append_right (by simpa using Nat.le_of_not_gt hr)]
simp only [List.length_replicate, List.getElem_map]
rfl
rw [hword]
refine Fin.cases ?_ (fun j => ?_) i
· simp [hr]
· rw [Fin.succ_inj, ih κ' r' j, hprefix]
change
((∑ k ∈ Finset.univ.filter (fun k => k < j), κ' k) ≤ r.val - κ 0 ∧
r.val - κ 0 < (∑ k ∈ Finset.univ.filter (fun k => k < j), κ' k) + κ' j) ↔
(κ 0 + (∑ k ∈ Finset.univ.filter (fun k => k < j), κ' k) ≤ r.val ∧
r.val < κ 0 + (∑ k ∈ Finset.univ.filter (fun k => k < j), κ' k) + κ' j)
omega
1 supporting declaration (lemmas, instances)
-
sorted_coordinate_directions_eq_prefixtheorem — For a vector of coordinate counts and a position r in its sorted word, the unit vector of the coordinate at position r equals the sum over coordinates i of the unit vector of i whenever r is at least the sum of the counts before i and strictly less than that sum plus the count of i, and zero otherwise.hypothesesconclusionconclusion 1single (sortedWord κ r) (1 : ℝ)= ∑ i, if (∑ j ∈ Finset.univ.filter (fun j => j < i), κ j) ≤ r.valconclusion 2r.val < (∑ j ∈ Finset.univ.filter (fun j => j < i), κ j)+ κ i then single i (1 : ℝ) else 0Proof (Lean source)
theorem sorted_coordinate_directions_eq_prefix {d : ℕ} (κ : Fin d → ℕ) (r : Fin (multiOrder κ)) : single (sortedWord κ r) (1 : ℝ) = ∑ i, if (∑ j ∈ Finset.univ.filter (fun j => j < i), κ j) ≤ r.val ∧ r.val < (∑ j ∈ Finset.univ.filter (fun j => j < i), κ j) + κ i then single i (1 : ℝ) else 0 := by classical symm rw [Finset.sum_eq_single (sortedWord κ r)] · rw [if_pos ((sortedWord_eq_iff_prefix κ r _).mp rfl)] · intro i _ hi rw [if_neg (fun h => hi ((sortedWord_eq_iff_prefix κ r i).mpr h).symm)] · intro h exact (h (Finset.mem_univ _)).elim
Segment 1 core · 1 supporting The segment from an interior cube point to a closed cube point remains interior before its final endpoint. ★ segment_iteratedDeriv_eq_diagonal
Interior line segments in a fixed cube
The segment from an interior cube point to a closed cube point remains interior before its final endpoint. Along that open part, ordinary line derivatives agree with diagonal Fréchet derivatives of the original function.
theorem segment_iteratedDeriv_eq_diagonal reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a function that is m times continuously differentiable on the closed normalized cube, a starting point x in the open cube, an end point y in the closed cube, a time t in the half-open unit interval, and an order k at most m, the k-th derivative at time t of the function restricted to the segment from x to y equals the order-k derivative of the function at the point x + t (y − x), taken k times in the direction y − x.
Formal statement
hypotheses
d m :
ℕ
(Fin d → ℝ) → ℝ
hu :
ContDiffOn ℝ m u (cube d)
x y :
Fin d → ℝ
hx :
x ∈ openCube d
hy :
y ∈ cube d
t :
ℝ
ht :
t ∈ Ico (0 : ℝ) 1
k :
ℕ
hk :
k ≤ m
conclusion
iteratedDeriv k (fun r : ℝ => u (x + r • (y - x))) t
= iteratedFDeriv ℝ k u (x + t • (y - x)) (fun _ => y - x)
Proof (Lean source)
theorem segment_iteratedDeriv_eq_diagonal {d m : ℕ}
{u : (Fin d → ℝ) → ℝ} (hu : ContDiffOn ℝ m u (cube d))
{x y : Fin d → ℝ} (hx : x ∈ openCube d) (hy : y ∈ cube d)
{t : ℝ} (ht : t ∈ Ico (0 : ℝ) 1)
(k : ℕ) (hk : k ≤ m) :
iteratedDeriv k (fun r : ℝ => u (x + r • (y - x))) t =
iteratedFDeriv ℝ k u (x + t • (y - x)) (fun _ => y - x) := by
let v : ℝ →L[ℝ] (Fin d → ℝ) :=
(1 : ℝ →L[ℝ] ℝ).smulRight (y - x)
let S : Set (Fin d → ℝ) := {z | x + z ∈ openCube d}
have ho : IsOpen (openCube d) :=
isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo)
have hsub : openCube d ⊆ cube d := by
intro z hz i
exact ⟨le_of_lt (hz i (Set.mem_univ i)).1,
le_of_lt (hz i (Set.mem_univ i)).2⟩
have hS : IsOpen S := ho.preimage (continuous_const.add continuous_id)
have hf : ContDiffOn ℝ m (fun z : Fin d → ℝ => u (x + z)) S := by
apply hS.contDiffOn_iff.mpr
intro z hz
exact ((hu.mono hsub).contDiffAt (ho.mem_nhds hz)).comp z
((contDiff_const.add contDiff_id).contDiffAt)
have hvt : v t ∈ S := by
simpa [S, v, ContinuousLinearMap.smulRight_apply] using
(segment_mem_openCube hx hy ht)
have hpre : IsOpen (v ⁻¹' S) := hS.preimage v.continuous
have hcomp := v.iteratedFDerivWithin_comp_right hf hS.uniqueDiffOn
hpre.uniqueDiffOn hvt (show (k : WithTop ℕ∞) ≤ m from mod_cast hk)
have hfun : (fun r : ℝ => u (x + r • (y - x))) =
(fun z : Fin d → ℝ => u (x + z)) ∘ v := by
funext r
simp [v, ContinuousLinearMap.smulRight_apply]
rw [hfun]
rw [iteratedDeriv_eq_iteratedFDeriv]
rw [← iteratedFDerivWithin_of_isOpen k hpre hvt,
hcomp, iteratedFDerivWithin_of_isOpen k hS hvt]
rw [iteratedFDeriv_comp_add_left]
simp [v, ContinuousMultilinearMap.compContinuousLinearMap_apply]
1 supporting declaration (lemmas, instances)
-
segment_mem_openCubetheorem — Every point before the final endpoint of a segment from an interior cube point to a closed cube point remains in the open cube.hypothesesconclusionx + t • (y - x) ∈ openCube dProof (Lean source)
theorem segment_mem_openCube {d : ℕ} {x y : Fin d → ℝ} (hx : x ∈ openCube d) (hy : y ∈ cube d) {t : ℝ} (ht : t ∈ Ico (0 : ℝ) 1) : x + t • (y - x) ∈ openCube d := by rcases ht with ⟨ht0, ht1⟩ intro i hi have hxi := hx i (Set.mem_univ i) have hyi := hy i dsimp [openCube] at hxi dsimp at hxi hyi ⊢ constructor · have h₁ : 0 < (1 - t) * (x i + 1) := mul_pos (by linarith) (by linarith [hxi.1]) have h₂ : 0 ≤ t * (y i + 1) := mul_nonneg ht0 (by linarith [hyi.1]) nlinarith · have h₁ : 0 < (1 - t) * (1 - x i) := mul_pos (by linarith) (by linarith [hxi.2]) have h₂ : 0 ≤ t * (1 - y i) := mul_nonneg ht0 (by linarith [hyi.2]) nlinarith
Taylor 1 core · 0 supporting The Taylor remainder uses only the Hölder differences of order-m coordinate partials. ★ top_holder_taylor_remainder
Taylor remainder from the top coordinate seminorm
The Taylor remainder uses only the Hölder differences of order-m coordinate partials.
The expansion point is interior, where ContDiffOn agrees with ambient derivatives.
theorem top_holder_taylor_remainder reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a dimension, a derivative order m, and an exponent s with s positive, there is a positive constant C such that, for every function that is m times continuously differentiable on the closed normalized cube and satisfies the top-order Hölder condition with exponent s and a nonnegative constant L, the function at any point y of the closed cube differs from its order-m Taylor polynomial centred at any point x of the open cube by at most C times L times the distance from x to y raised to the power m + s.
Formal statement
hypotheses
d m :
ℕ
s :
ℝ
hs :
0 < s
conclusion
∃ C : ℝ,
0 < C
conclusion 1
u :
(Fin d → ℝ) → ℝ
L :
ℝ
0 ≤ L
ContDiffOn ℝ m u (cube d)
TopHolder d m s L u
x ∈ openCube d :
y ∈ cube d :
|u y
- ∑ k ∈ range (m + 1), (Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => y - x)|
≤ C * L * ‖y - x‖ ^ ((m : ℝ) + s)
Proof (Lean source)
theorem top_holder_taylor_remainder (d m : ℕ) (s : ℝ)
(hs : 0 < s) :
∃ C : ℝ, 0 < C ∧
∀ (u : (Fin d → ℝ) → ℝ) (L : ℝ),
0 ≤ L → ContDiffOn ℝ m u (cube d) → TopHolder d m s L u →
∀ x ∈ openCube d, ∀ y ∈ cube d,
|u y - ∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ *
iteratedFDeriv ℝ k u x (fun _ => y - x)| ≤
C * L * ‖y - x‖ ^ ((m : ℝ) + s) := by
refine ⟨((d : ℝ) + 1) ^ m, by positivity, ?_⟩
intro u L hL hu hholder x hx y hy
let v : ℝ → ℝ := fun r => u (x + r • (y - x))
have hline : ContDiff ℝ m (fun r : ℝ => x + r • (y - x)) :=
contDiff_const.add (contDiff_id.smul contDiff_const)
have hmaps : Set.MapsTo (fun r : ℝ => x + r • (y - x))
(Icc (0 : ℝ) 1) (cube d) := by
intro r hr
by_cases hr1 : r < 1
· have h := segment_mem_openCube hx hy (show r ∈ Ico (0 : ℝ) 1 from ⟨hr.1, hr1⟩)
intro i
exact ⟨le_of_lt (h i (Set.mem_univ i)).1,
le_of_lt (h i (Set.mem_univ i)).2⟩
· have hr' : r = 1 := by linarith [hr.2]
subst r
simpa using hy
have hv : ContDiffOn ℝ m v (Icc (0 : ℝ) 1) :=
hu.comp hline.contDiffOn hmaps
have hzero : (0 : ℝ) ∈ Ico (0 : ℝ) 1 := by norm_num
have hderiv (k : ℕ) (hk : k ≤ m) :
iteratedDeriv k v 0 = iteratedFDeriv ℝ k u x (fun _ => y - x) := by
simpa [v] using segment_iteratedDeriv_eq_diagonal hu hx hy hzero k hk
have hpoly :
(∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedFDeriv ℝ k u x (fun _ => y - x)) =
∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k := by
apply Finset.sum_congr rfl
intro k hk
rw [hderiv k (Nat.lt_succ_iff.mp (Finset.mem_range.mp hk))]
norm_num
have hvone : v 1 = u y := by simp [v]
have hbase : ∀ k ≤ m,
iteratedDerivWithin k v (uIcc (0 : ℝ) 1) 0 = iteratedDeriv k v 0 := by
intro k hk
have hcont : ContDiffAt ℝ k v 0 := by
have ho : IsOpen (openCube d) :=
isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo)
have hsub : openCube d ⊆ cube d := by
intro z hz i
exact ⟨le_of_lt (hz i (Set.mem_univ i)).1,
le_of_lt (hz i (Set.mem_univ i)).2⟩
have hux : ContDiffAt ℝ k u x :=
((hu.mono hsub).contDiffAt (ho.mem_nhds hx)).of_le (by exact_mod_cast hk)
have hlinek : ContDiffAt ℝ k (fun r : ℝ => x + r • (y - x)) 0 :=
(hline.of_le (by exact_mod_cast hk)).contDiffAt
have hux' : ContDiffAt ℝ k u (x + (0 : ℝ) • (y - x)) := by simpa using hux
change ContDiffAt ℝ k (u ∘ fun r : ℝ => x + r • (y - x)) 0
exact hux'.comp 0 hlinek
exact iteratedDerivWithin_eq_iteratedDeriv
(uniqueDiffOn_uIcc (by norm_num : (0 : ℝ) ≠ 1)) hcont Set.left_mem_uIcc
by_cases hm0 : m = 0
· subst m
have htop := topHolder_diagonal_derivative u hL hholder y x (y - x) hy
(by
intro i
exact ⟨le_of_lt (hx i (Set.mem_univ i)).1,
le_of_lt (hx i (Set.mem_univ i)).2⟩)
simp only [Finset.range_one, Finset.sum_singleton] at *
simp [iteratedFDeriv_zero] at htop ⊢
simpa [abs_sub_comm, norm_sub_rev] using htop
· have hmpos : 0 < m := Nat.pos_of_ne_zero hm0
let n := m - 1
have hn : n + 1 = m := Nat.succ_pred_eq_of_pos hmpos
have hcont : ContDiffOn ℝ (n + 1) v (uIcc (0 : ℝ) 1) := by
change ContDiffOn ℝ (↑(n + 1 : ℕ)) v (uIcc (0 : ℝ) 1)
rw [hn, Set.uIcc_of_le (by norm_num : (0 : ℝ) ≤ 1)]
exact hv
obtain ⟨ξ, hξ, hrem⟩ :=
taylor_mean_remainder_lagrange_iteratedDeriv
(f := v) (x := (1 : ℝ)) (x₀ := (0 : ℝ)) (n := n)
(by norm_num) hcont
have hξ' : ξ ∈ Ioo (0 : ℝ) 1 := by
simpa [Set.uIoo_of_le (by norm_num : (0 : ℝ) ≤ 1)] using hξ
have htop : |iteratedDeriv m v ξ - iteratedDeriv m v 0| ≤
((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) := by
have ht : 0 ≤ (ξ + 1) / 2 ∧ (ξ + 1) / 2 < 1 := by constructor <;> linarith [hξ'.1, hξ'.2]
have hξmem : ξ ∈ Icc (0 : ℝ) ((ξ + 1) / 2) := ⟨hξ'.1.le, by linarith [hξ'.2]⟩
have h0mem : (0 : ℝ) ∈ Icc (0 : ℝ) ((ξ + 1) / 2) := ⟨le_refl _, ht.1⟩
have h := segment_line_topHolder_before_endpoint hu hs hL hholder hx hy
ht.2 hξmem h0mem
have hp : |ξ - 0| ^ s ≤ (1 : ℝ) := by
rw [sub_zero, abs_of_pos hξ'.1]
simpa using Real.rpow_le_rpow (le_of_lt hξ'.1) hξ'.2.le hs.le
calc
_ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) * |ξ - 0| ^ s := h
_ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) * 1 :=
mul_le_mul_of_nonneg_left hp (by positivity)
_ = _ := by ring
have hpolyM :
(∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k) =
(∑ k ∈ range (n + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k) +
(Nat.factorial m : ℝ)⁻¹ * iteratedDeriv m v 0 * (1 - 0) ^ m := by
rw [hn, Finset.sum_range_succ]
have hpolyN : taylorWithinEval v n (uIcc (0 : ℝ) 1) 0 1 =
∑ k ∈ range (n + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k := by
rw [taylor_within_apply]
apply Finset.sum_congr rfl
intro k hk
have hk' : k ≤ m := by
have hk'' : k ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk)
omega
rw [hbase k hk']
simp only [smul_eq_mul]
ring
have hdiff : v 1 - (∑ k ∈ range (m + 1),
(Nat.factorial k : ℝ)⁻¹ * iteratedDeriv k v 0 * (1 - 0) ^ k) =
(iteratedDeriv m v ξ - iteratedDeriv m v 0) /
(Nat.factorial m : ℝ) := by
rw [hpolyM, ← hpolyN, sub_add_eq_sub_sub, hrem]
simp only [hn]
norm_num
ring
rw [← hvone, hpoly, hdiff]
have hfac : 1 ≤ (Nat.factorial m : ℝ) := by exact_mod_cast Nat.factorial_pos m
calc
|(iteratedDeriv m v ξ - iteratedDeriv m v 0) / (Nat.factorial m : ℝ)| =
|iteratedDeriv m v ξ - iteratedDeriv m v 0| / (Nat.factorial m : ℝ) := by
rw [abs_div, abs_of_nonneg (by linarith : (0 : ℝ) ≤ m.factorial)]
_ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) /
(Nat.factorial m : ℝ) := div_le_div_of_nonneg_right htop (by linarith)
_ ≤ ((d : ℝ) + 1) ^ m * L * ‖y - x‖ ^ ((m : ℝ) + s) :=
div_le_self (by positivity) hfac
TaylorLegendre 2 core · 2 supporting The headline combines independently derived multinomial grouping, the explicit degree-two inverse Legendre transform, its uniform coefficient norm bound, and the Euclidean within-cube Hölder remainder. ★ euclidean_multiindex_taylor_legendre_adapter
Euclidean sorted Taylor to scaled tensor Legendre adapter
The headline combines independently derived multinomial grouping, the explicit degree-two inverse Legendre transform, its uniform coefficient norm bound, and the Euclidean within-cube Hölder remainder. The coefficient vector is explicit, the polynomial is realized at every point, and the center value is exact. All constants are quantified before the function, scale, and Hölder exponent. The ambient cube can be the local cube itself or any larger cube; no global extension, research-model premise, or assumed Taylor representation is used.
def taylorLegendreCoefficients reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The Taylor-to-Legendre coefficient vector of a function on its derivative domain of degree m at a centre and side length h is the Legendre coefficient transform, at scale h, of the function's sorted Taylor coefficients at the centre.
Definition (Lean source)
parameters
def
given by
legendreCoefficients h (taylorCoefficient S u a)
theorem euclidean_multiindex_taylor_legendre_adapter reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
In a finite Euclidean dimension at a degree at most two, there is a positive constant C with the following property. Take a cube of positive side length, a nonnegative L, a positive exponent s at most one, and a function that is m times continuously differentiable on the cube, whose sorted coordinate partials of total order at most m are bounded by L on the cube, and whose sorted partials of total order exactly m change between any two cube points by at most L times their distance to the power s. Then for every smaller cube of positive side length h at most one half, contained in the big cube and centred at one of its interior points, the Taylor-to-Legendre coefficient vector at that centre satisfies four things: its scaled Legendre polynomial equals the multi-index Taylor polynomial everywhere; on the smaller cube the function differs from it by at most C times L times h to the power m + s; the Euclidean norm of the coefficient vector is at most C times L; and the polynomial takes the function's value at the centre.
Formal statement
hypotheses
d m :
ℕ
hm :
m ≤ 2
conclusion
∃ C : ℝ,
0 < C
conclusion 1
b a :
EuclideanSpace ℝ (Fin d)
H h L s :
ℝ
u :
EuclideanSpace ℝ (Fin d) → ℝ
0 < H
0 < h
h ≤ 1 / 2
0 ≤ L
0 < s
s ≤ 1
ContDiffOn ℝ m u (centeredCube b H)
(∀ κ : MultiIndex d m, ∀ x ∈ centeredCube b H, |coordinatePartial (centeredCube b H) u κ.1 x| ≤ L)
(∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H, ∀ z ∈ centeredCube b H, |coordinatePartial (centeredCube b H) u κ.1 x - coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s)
a ∈ interior (centeredCube b H)
centeredCube a h ⊆ centeredCube b H
∃ θ : MultiIndex d m → ℝ,
θ = taylorLegendreCoefficients (centeredCube b H) u m a h
x :
legendrePolynomial a h θ x = multiindexTaylor (centeredCube b H) u m a x
x ∈ centeredCube a h :
|u x - legendrePolynomial a h θ x| ≤ C * L * h ^ ((m : ℝ) + s)
sqrt (∑ κ, θ κ ^ 2) ≤ C * L
legendrePolynomial a h θ a = u a
Proof (Lean source)
theorem euclidean_multiindex_taylor_legendre_adapter (d m : ℕ) (hm : m ≤ 2) :
∃ C : ℝ, 0 < C ∧ ∀ (b a : EuclideanSpace ℝ (Fin d))
(H h L s : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ),
0 < H → 0 < h → h ≤ 1 / 2 → 0 ≤ L → 0 < s → s ≤ 1 →
ContDiffOn ℝ m u (centeredCube b H) →
(∀ κ : MultiIndex d m, ∀ x ∈ centeredCube b H,
|coordinatePartial (centeredCube b H) u κ.1 x| ≤ L) →
(∀ κ : ExactIndex d m, ∀ x ∈ centeredCube b H, ∀ z ∈ centeredCube b H,
|coordinatePartial (centeredCube b H) u κ.1 x -
coordinatePartial (centeredCube b H) u κ.1 z| ≤ L * ‖x - z‖ ^ s) →
a ∈ interior (centeredCube b H) → centeredCube a h ⊆ centeredCube b H →
∃ θ : MultiIndex d m → ℝ,
θ = taylorLegendreCoefficients (centeredCube b H) u m a h ∧
(∀ x, legendrePolynomial a h θ x = multiindexTaylor (centeredCube b H) u m a x) ∧
(∀ x ∈ centeredCube a h,
|u x - legendrePolynomial a h θ x| ≤ C * L * h ^ ((m : ℝ) + s)) ∧
sqrt (∑ κ, θ κ ^ 2) ≤ C * L ∧
legendrePolynomial a h θ a = u a := by
obtain ⟨Cr, hCr, hr⟩ := local_cube_multiindex_remainder d m
obtain ⟨Cb, hCb, hb⟩ := legendreCoefficients_l2_bound d m hm
refine ⟨max Cr Cb, lt_max_of_lt_left hCr, ?_⟩
intro b a H h L s u hH hh hhhalf hL hs hs1 hu hderiv hmod ha hsub
let θ := taylorLegendreCoefficients (centeredCube b H) u m a h
have heq : ∀ x, legendrePolynomial a h θ x =
multiindexTaylor (centeredCube b H) u m a x :=
fun x => taylorLegendreCoefficients_realize hm _ u a x h hh
refine ⟨θ, rfl, heq, ?_, ?_, ?_⟩
· intro x hx
rw [heq]
exact (hr b a H h L s u hH hh hL hs hs1 hu hmod ha hsub x hx).trans
(mul_le_mul_of_nonneg_right
(mul_le_mul_of_nonneg_right (le_max_left Cr Cb) hL)
(Real.rpow_nonneg hh.le _))
· have hc := taylorCoefficient_abs_le (centeredCube b H) u a L hL
(fun κ => hderiv κ a (interior_subset ha))
exact (hb h L (taylorCoefficient (centeredCube b H) u a)
hh hhhalf hL hc).trans
(mul_le_mul_of_nonneg_right (le_max_right Cr Cb) hL)
· rw [heq, multiindexTaylor_center]
2 supporting declarations (lemmas, instances)
-
taylorCoefficient_abs_letheorem — For a function on its derivative domain, a centre, and a bound L that is nonnegative, if every sorted coordinate partial of total order at most m is at most L in absolute value at the centre, then every sorted Taylor coefficient of total order at most m is at most L in absolute value.hypothesesd m :ℕS :u :EuclideanSpace ℝ (Fin d) → ℝa :EuclideanSpace ℝ (Fin d)L :ℝhL :0 ≤ Lhderiv :∀ κ : MultiIndex d m, |coordinatePartial S u κ.1 a| ≤ Lκ :MultiIndex d mconclusion|taylorCoefficient S u a κ| ≤ LProof (Lean source)
theorem taylorCoefficient_abs_le {d m : ℕ} (S : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ) (a : EuclideanSpace ℝ (Fin d)) (L : ℝ) (hL : 0 ≤ L) (hderiv : ∀ κ : MultiIndex d m, |coordinatePartial S u κ.1 a| ≤ L) : ∀ κ : MultiIndex d m, |taylorCoefficient S u a κ| ≤ L := by intro κ have hfac : 1 ≤ (multiFactorial κ.1 : ℝ) := by exact_mod_cast multiFactorial_pos κ.1 unfold taylorCoefficient rw [abs_div, abs_of_nonneg (by linarith : 0 ≤ (multiFactorial κ.1 : ℝ))] exact (div_le_div_of_nonneg_right (hderiv κ) (by linarith)).trans (div_le_self hL hfac) -
taylorLegendreCoefficients_realizetheorem — For a degree m at most two, a function on its derivative domain, a centre a and an evaluation point x, and a side length h that is positive, the scaled Legendre polynomial built from the Taylor-to-Legendre coefficients equals the degree-m multi-index Taylor polynomial at x.hypothesesd m :ℕhm :m ≤ 2S :u :EuclideanSpace ℝ (Fin d) → ℝa x :EuclideanSpace ℝ (Fin d)h :ℝhh :0 < hconclusionlegendrePolynomial a h (taylorLegendreCoefficients S u m a h) x= multiindexTaylor S u m a xProof (Lean source)
theorem taylorLegendreCoefficients_realize {d m : ℕ} (hm : m ≤ 2) (S : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ) (a x : EuclideanSpace ℝ (Fin d)) (h : ℝ) (hh : 0 < h) : legendrePolynomial a h (taylorLegendreCoefficients S u m a h) x = multiindexTaylor S u m a x := by exact legendreCoefficients_realize hm a x h hh (taylorCoefficient S u a)
Words 2 core · 6 supporting Coordinate words are grouped by their multiplicity vectors at arbitrary order. ★ word_fiber_card_eq_multinomial
Word fibers and multinomial grouping
Coordinate words are grouped by their multiplicity vectors at arbitrary order. These results are combinatorial: no smoothness, degree-two restriction, or Taylor realization is a premise. The grouped-sum lemma is the interface used by the Taylor layer.
The word count and factorial quotient conventions agree with the primary multinomial definition and formula https://dlmf.nist.gov/26.4#i and https://dlmf.nist.gov/26.4.E2, including admissible empty coordinate sets.
def wordFiber reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
The word fiber for a word length k and a vector of coordinate counts is the finite set of all length-k coordinate words in which each coordinate occurs exactly as often as its count prescribes.
Definition (Lean source)
parameters
given by
Finset.univ.filter fun w => coordCount w = κ
theorem word_fiber_card_eq_multinomial reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.CubeInterpolation
For a vector of coordinate counts whose total order is k, the number of length-k words with those counts is k factorial divided by the product of the factorials of the counts.
Formal statement
hypotheses
conclusion
(wordFiber k κ).card = k.factorial / multiFactorial κ
Proof (Lean source)
theorem word_fiber_card_eq_multinomial {d k : ℕ} (κ : Fin d → ℕ)
(hκ : multiOrder κ = k) :
(wordFiber k κ).card = k.factorial / multiFactorial κ := by
classical
let a : Fin d →₀ ℕ := Finsupp.equivFunOnFinite.symm κ
have ha : a.sum (fun _ n => n) = k := by
rw [Finsupp.sum_fintype _ _ (fun _ => rfl)]
exact hκ
have hcoeff (w : Fin k → Fin d) :
coeff a (∏ r, (MvPolynomial.X (w r) : MvPolynomial (Fin d) ℕ)) =
if coordCount w = κ then 1 else 0 := by
have hp : (∏ r, (MvPolynomial.X (w r) : MvPolynomial (Fin d) ℕ)) =
∏ i, MvPolynomial.X i ^ coordCount w i := by
simpa [coordCount] using
(Finset.prod_fiberwise' (Finset.univ : Finset (Fin k)) w
(fun i => (MvPolynomial.X i : MvPolynomial (Fin d) ℕ))).symm
rw [hp, MvPolynomial.coeff_prod_X_pow]
have he : a = Finsupp.indicator Finset.univ (fun i _ => coordCount w i) ↔
coordCount w = κ := by
constructor
· intro h
funext i
simpa [a, Finsupp.indicator_apply] using (congrArg (fun b => b i) h).symm
· intro h
ext i
simp [a, Finsupp.indicator_apply, h]
simp only [he]
have hc := MvPolynomial.coeff_sum_X_pow_of_fintype (R := ℕ) a k
rw [if_pos ha, Fintype.sum_pow, MvPolynomial.coeff_sum] at hc
simp_rw [hcoeff] at hc
rw [Finset.sum_boole] at hc
rw [Finsupp.multinomial_eq_of_support_subset (Finset.subset_univ _)] at hc
simpa [wordFiber, multinomial, ← hκ, multiOrder, multiFactorial, a] using hc
6 supporting declarations (lemmas, instances)
-
coordCount_ordertheorem — For a coordinate word of length k, its coordinate counts have total order k.Proof (Lean source)
theorem coordCount_order {d k : ℕ} (w : Fin k → Fin d) : multiOrder (coordCount w) = k := by simpa [multiOrder, coordCount] using Finset.sum_card_fiberwise_eq_card_filter (Finset.univ : Finset (Fin k)) (Finset.univ : Finset (Fin d)) w -
sortedWord_counttheorem — For a vector of coordinate counts, each coordinate occurs in the sorted word exactly as often as its count prescribes.Proof (Lean source)
theorem sortedWord_count {d : ℕ} (κ : Fin d → ℕ) : coordCount (sortedWord κ) = κ := by funext i let v : List.Vector (Fin d) (multiOrder κ) := ⟨countList κ, countList_length κ⟩ have hcount : coordCount (sortedWord κ) i = (countList κ).count i := by have hv : v.get = sortedWord κ := by funext r rfl change (Finset.univ.filter fun r => sortedWord κ r = i).card = _ rw [← hv] exact Fin.card_filter_univ_eq_vector_get_eq_count i v rw [hcount] simp [countList, List.count_flatten, List.map_ofFn, List.sum_ofFn, List.count_replicate, beq_iff_eq] -
coordCount_eq_iff_permtheorem — Two coordinate words of the same length have the same coordinate counts exactly when one is obtained from the other by permuting positions.hypothesesProof (Lean source)
theorem coordCount_eq_iff_perm {d k : ℕ} (v w : Fin k → Fin d) : coordCount v = coordCount w ↔ ∃ σ : Perm (Fin k), v = w ∘ σ := by -- List.ofFn translates count equality into List.Perm. Its position bijection -- gives the permutation; the reverse direction reindexes finite fibers. -- Alternatively, Equiv.ofFiberEquiv and Equiv.ofFiberEquiv_map assemble -- coordinate-fiber equivalences obtained from equal finite cardinalities. classical constructor · intro h have hc (i : Fin d) : card {r // v r = i} = card {r // w r = i} := by simpa [Fintype.card_subtype, coordCount] using congrFun h i let e (i : Fin d) : {r // v r = i} ≃ {r // w r = i} := Fintype.equivOfCardEq (hc i) exact ⟨Equiv.ofFiberEquiv e, funext fun r => (Equiv.ofFiberEquiv_map e r).symm⟩ · rintro ⟨σ, rfl⟩ funext i have hc := Fintype.card_congr (σ.subtypeEquiv (p := fun r => (w ∘ σ) r = i) (q := fun r => w r = i) (by intro r; rfl)) simpa [Fintype.card_subtype, coordCount] using hc -
word_fiber_card_mul_factorialtheorem — For a vector of coordinate counts whose total order is k, the number of length-k words with those counts, multiplied by the product of the factorials of the counts, equals k factorial.hypothesesconclusion(wordFiber k κ).card * multiFactorial κ = k.factorialProof (Lean source)
theorem word_fiber_card_mul_factorial {d k : ℕ} (κ : Fin d → ℕ) (hκ : multiOrder κ = k) : (wordFiber k κ).card * multiFactorial κ = k.factorial := by rw [word_fiber_card_eq_multinomial κ hκ] have h := Nat.multinomial_spec univ κ simpa [multinomial, ← hκ, multiOrder, multiFactorial, Nat.mul_comm] using h -
word_product_eq_count_producttheorem — For a coordinate word and a real vector z, the product of the coordinates of z selected along the word equals the product over coordinates of each coordinate of z raised to the number of times it occurs in the word.hypothesesconclusion(∏ r, z (w r)) = ∏ i, z i ^ coordCount w iProof (Lean source)
theorem word_product_eq_count_product {d k : ℕ} (w : Fin k → Fin d) (z : Fin d → ℝ) : (∏ r, z (w r)) = ∏ i, z i ^ coordCount w i := by simpa [coordCount] using (Finset.prod_fiberwise' (Finset.univ : Finset (Fin k)) w z).symm -
group_word_sum_by_counttheorem — For a real function of length-k coordinate words that takes equal values on words with the same coordinate counts, its sum over all words equals the sum over count vectors of total order k of the multinomial number k factorial over the product of count factorials, times the function's value at the sorted word of that count vector.hypothesesconclusion(∑ w, F w)= ∑ κ : ExactIndex d k, ((k.factorial / multiFactorial κ.1 : ℕ) : ℝ) * F (sortedWordOfOrder κ)Proof (Lean source)
theorem group_word_sum_by_count {d k : ℕ} (F : (Fin k → Fin d) → ℝ) (hF : ∀ v w, coordCount v = coordCount w → F v = F w) : (∑ w, F w) = ∑ κ : ExactIndex d k, ((k.factorial / multiFactorial κ.1 : ℕ) : ℝ) * F (sortedWordOfOrder κ) := by classical let count : (Fin k → Fin d) → ExactIndex d k := fun w => ⟨coordCount w, coordCount_order w⟩ have hs (κ : ExactIndex d k) : coordCount (sortedWordOfOrder κ) = κ.1 := by rcases κ with ⟨κ, hκ⟩ subst k have hw : sortedWordOfOrder ⟨κ, rfl⟩ = sortedWord κ := by funext r rfl rw [hw] exact sortedWord_count κ rw [← Finset.sum_fiberwise univ count F] apply Finset.sum_congr rfl intro κ _ have hf : (Finset.univ.filter fun w => count w = κ) = wordFiber k κ.1 := by ext w simp only [mem_filter, Finset.mem_univ, true_and, wordFiber] exact Subtype.ext_iff rw [hf] calc ∑ w ∈ wordFiber k κ.1, F w = ∑ _w ∈ wordFiber k κ.1, F (sortedWordOfOrder κ) := by apply Finset.sum_congr rfl intro w hw apply hF exact (Finset.mem_filter.mp hw).2.trans (hs κ).symm _ = ((wordFiber k κ.1).card : ℝ) * F (sortedWordOfOrder κ) := by simp _ = _ := by rw [word_fiber_card_eq_multinomial κ.1 κ.2]