Mathlib.Analysis.Calculus.CubeExtension
This package supplies extension-independent coordinate jets on closed finite-dimensional cubes, quantitative Hölder completion, affine transport, and controlled global extensions.
Basic 6 core · 3 supporting Coordinate jets are evaluated with iteratedFDerivWithin on the specified closed set. ★ continuousOn_coordJetOn_cube
Intrinsic coordinate jets on finite cubes
Coordinate jets are evaluated with iteratedFDerivWithin on the specified closed set.
Consequently the data depend only on the restriction of a response to that set.
The intrinsic coordinate jet of order j of a response u on a set S, in the coordinate directions f(0), …, f(j − 1) and at a point x, is the order-j iterated Fréchet derivative of u within S at x applied to the corresponding standard basis vectors.
A response u has a top-order intrinsic Hölder modulus on a set S, for derivative order m, exponent s and coefficient L, when for every choice of m coordinate directions the order-m intrinsic coordinate jets of u at any two points x, y of S differ in absolute value by at most L·‖x − y‖^s.
Definition (Lean source)
The intrinsic jet bound for a response u on a set S through order m with bound R states that every intrinsic coordinate jet of u of order at most m, in any coordinate directions, has absolute value at most R at every point of S.
On a set in dimension, a response with derivative order m, Hölder exponent s, and radius R lies in the intrinsic Hölder ball when it is m times continuously differentiable within the set, all its intrinsic coordinate jets of order at most m are bounded by R in absolute value on the set, and its order-m intrinsic coordinate jets have an s-Hölder modulus with coefficient R on the set.
Definition (Lean source)
The intrinsic Hölder ball on the normalized closed cube in dimension d, for derivative order m, exponent s and radius R, is the statement that a response u belongs to the intrinsic Hölder ball with these parameters on the cube [-1,1]^d.
Definition (Lean source)
If a response u is m times continuously differentiable within the closed cube and j ≤ m, then for any coordinate directions f the order-j intrinsic coordinate jet of u in those directions is continuous on the closed cube.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
coordJetOn_congrtheorem — If two responses u and v agree on a set S, then at every point x of S their intrinsic coordinate jets on S coincide, for every order and every choice of coordinate directions.hypothesesconclusioncoordJetOn S j u f x = coordJetOn S j v f xProof (Lean source)
theorem coordJetOn_congr {d j : ℕ} {S : Set (Fin d → ℝ)} {u v : (Fin d → ℝ) → ℝ} (h : EqOn u v S) {f : Fin j → Fin d} {x : Fin d → ℝ} (hx : x ∈ S) : coordJetOn S j u f x = coordJetOn S j v f x := by unfold coordJetOn rw [iteratedFDerivWithin_congr h hx j] -
holderBallOn_congrtheorem — If two responses u and v agree on a set S, then u lies in the intrinsic Hölder ball on S of a given order, exponent and radius exactly when v does.hypothesesconclusionHolderBallOn S m s R u ↔ HolderBallOn S m s R vProof (Lean source)
theorem holderBallOn_congr {d m : ℕ} {S : Set (Fin d → ℝ)} {s R : ℝ} {u v : (Fin d → ℝ) → ℝ} (h : EqOn u v S) : HolderBallOn S m s R u ↔ HolderBallOn S m s R v := by constructor · intro hu refine ⟨hu.regularity.congr (fun x hx => (h hx).symm), ?_, ?_⟩ · intro j hj f x hx rw [← coordJetOn_congr h hx] exact hu.derivBound j hj f x hx · intro f x hx y hy rw [← coordJetOn_congr h hx, ← coordJetOn_congr h hy] exact hu.modulus f x hx y hy · intro hv refine ⟨hv.regularity.congr (fun x hx => h hx), ?_, ?_⟩ · intro j hj f x hx rw [coordJetOn_congr h hx] exact hv.derivBound j hj f x hx · intro f x hx y hy rw [coordJetOn_congr h hx, coordJetOn_congr h hy] exact hv.modulus f x hx y hy -
coordJetOn_cube_eq_ambienttheorem — If a response u is m times continuously differentiable within the closed cube and j ≤ m, then at a point x of the open cube the order-j intrinsic coordinate jet of u on the closed cube equals the usual ambient order-j coordinate partial derivative.hypothesesd m j :ℕ(Fin d → ℝ) → ℝhu :ContDiffOn ℝ m u (cube d)hj :j ≤ mx :Fin d → ℝhx :x ∈ openCube dconclusioncoordJetOn (cube d) j u f x = coordPartial j u f xProof (Lean source)
theorem coordJetOn_cube_eq_ambient {d m j : ℕ} {u : (Fin d → ℝ) → ℝ} (hu : ContDiffOn ℝ m u (cube d)) (hj : j ≤ m) {f : Fin j → Fin d} {x : Fin d → ℝ} (hx : x ∈ openCube d) : coordJetOn (cube d) j u f x = coordPartial j u f x := by have hsub : openCube d ⊆ cube d := by intro z hz i exact ⟨(hz i trivial).1.le, (hz i trivial).2.le⟩ have hopen : IsOpen (openCube d) := isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo) have hreg : ContDiffAt ℝ j u x := (hu.mono hsub).contDiffAt (hopen.mem_nhds hx) |>.of_le (by exact_mod_cast hj) have hcube : cube d = Set.univ.pi (fun _ : Fin d => Icc (-1 : ℝ) 1) := by ext z simp [cube, normalizedCube, Pi.le_def, forall_and] have huniq : UniqueDiffOn ℝ (cube d) := by rw [hcube] exact UniqueDiffOn.pi (fun _ _ => uniqueDiffOn_Icc (by norm_num)) unfold coordJetOn coordPartial rw [iteratedFDerivWithin_eq_iteratedFDeriv huniq hreg (hsub hx)]
RectangularAffineGeometry 3 core · 2 supporting For boxes with positive side lengths, a point lies in the source box exactly when the coordinatewise affine map sends it into the target box. ★ exists_rectAffine_rpow_constant
Geometry of affine maps between closed rectangular boxes
For boxes with positive side lengths, a point lies in the source box exactly when the coordinatewise affine map sends it into the target box. The map's distance distortion also controls every real power of the distance, including negative exponents.
The closed coordinate box with lower corner lo and upper corner hi is the set of points whose i-th coordinate lies in [lo i, hi i] for every i.
The coordinatewise affine map from the box with corners lo, hi to the box with corners lo', hi' sends a point x to the point whose i-th coordinate is lo'_i + (hi'_i − lo'_i)/(hi_i − lo_i)·(x_i − lo_i). It carries the first box onto the second when both have positive side lengths.
If the source box and the target box both have positive side lengths, then for any real power s there is a positive constant C such that the s-th power of the distance between the images of any two points under the coordinatewise affine map is at most C times the s-th power of the distance between the points.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
uniqueDiffOn_rectBoxtheorem — If the box with corners lo and hi has strictly positive side lengths, then it has unique within-set derivatives at every point, including its faces.Proof (Lean source)
theorem uniqueDiffOn_rectBox {d : ℕ} (lo hi : Fin d → ℝ) (h : ∀ i, lo i < hi i) : UniqueDiffOn ℝ (rectBox lo hi) := by have hbox : rectBox lo hi = Set.univ.pi (fun i : Fin d => Icc (lo i) (hi i)) := by ext x simp [rectBox, Pi.le_def, forall_and] rw [hbox] exact UniqueDiffOn.pi (fun i _ => uniqueDiffOn_Icc (h i)) -
rectAffine_preimage_rectBoxtheorem — If the source box with corners lo, hi and the target box with corners lo', hi' both have positive side lengths, then a point lies in the source box exactly when its image under the coordinatewise affine map lies in the target box.hypothesesconclusionProof (Lean source)
theorem rectAffine_preimage_rectBox {d : ℕ} (lo hi lo' hi' : Fin d → ℝ) (hsource : ∀ i, lo i < hi i) (htarget : ∀ i, lo' i < hi' i) : rectAffine lo hi lo' hi' ⁻¹' rectBox lo' hi' = rectBox lo hi := by ext x simp only [Set.mem_preimage, rectBox, Set.mem_ofPred_eq] constructor <;> intro hx i · have hs : 0 < hi i - lo i := sub_pos.mpr (hsource i) have ht : 0 < hi' i - lo' i := sub_pos.mpr (htarget i) have ha : 0 < (hi' i - lo' i) / (hi i - lo i) := div_pos ht hs have heq : (hi' i - lo' i) / (hi i - lo i) * (hi i - lo i) = hi' i - lo' i := div_mul_cancel₀ _ hs.ne' have h := hx i change lo' i ≤ lo' i + (hi' i - lo' i) / (hi i - lo i) * (x i - lo i) ∧ lo' i + (hi' i - lo' i) / (hi i - lo i) * (x i - lo i) ≤ hi' i at h constructor · have : 0 ≤ (hi' i - lo' i) / (hi i - lo i) * (x i - lo i) := by linarith [h.1] exact sub_nonneg.mp ((mul_nonneg_iff_of_pos_left ha).mp this) · have : (hi' i - lo' i) / (hi i - lo i) * (x i - lo i) ≤ (hi' i - lo' i) / (hi i - lo i) * (hi i - lo i) := by linarith [h.2] exact sub_nonneg.mp (by nlinarith [(mul_le_mul_iff_of_pos_left ha).mp this]) · have hs : 0 < hi i - lo i := sub_pos.mpr (hsource i) have ht : 0 < hi' i - lo' i := sub_pos.mpr (htarget i) have ha : 0 < (hi' i - lo' i) / (hi i - lo i) := div_pos ht hs have heq : (hi' i - lo' i) / (hi i - lo i) * (hi i - lo i) = hi' i - lo' i := div_mul_cancel₀ _ hs.ne' have h := hx i change lo i ≤ x i ∧ x i ≤ hi i at h change lo' i ≤ lo' i + (hi' i - lo' i) / (hi i - lo i) * (x i - lo i) ∧ lo' i + (hi' i - lo' i) / (hi i - lo i) * (x i - lo i) ≤ hi' i constructor · have := mul_nonneg ha.le (sub_nonneg.mpr h.1) linarith · have := (mul_le_mul_iff_of_pos_left ha).mpr (sub_le_sub_right h.2 (lo i)) linarith
ReflectionOperator 3 core · 1 supporting Reflection weights combine inward samples to define a response on a thin collar outside one face. ★ leftFaceReflection_continuousOn
One-face reflection on a cube collar
Reflection weights combine inward samples to define a response on a thin collar outside one face. This module records the operator, its exact agreement on the original cube, and the first gluing obligation at the face.
The left collar of the normalized cube in dimension d, for derivative order m and coordinate i, is the closed box whose i-th coordinate ranges over [-1 - 1/(m+1), 1] and whose other coordinates range over [-1,1]; it extends the cube outward by 1/(m + 1) past its left face in coordinate i.
The one-face reflection of a response u across the left face in coordinate i of the normalized cube in dimension d, with reflection weights a_0, …, a_m for derivative order m, equals u at points whose i-th coordinate is at least −1, and at points with i-th coordinate below −1 equals the weighted sum over q of a_q times u at the inward reflection sample with dilation index q.
If the reflection weights a sum to one, so that the reflection reproduces constants, and a response u is continuous on the closed cube, then the one-face reflection of u is continuous on the closed left collar.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
leftFaceReflection_eqOn_cubetheorem — The one-face reflection of a response u agrees with u at every point of the normalized cube, whatever the reflection weights and whatever the values of u outside the cube.hypothesesconclusionEqOn (leftFaceReflection d m i a u) u (cube d)Proof (Lean source)
theorem leftFaceReflection_eqOn_cube (d m : ℕ) (i : Fin d) (a : Fin (m + 1) → ℝ) (u : (Fin d → ℝ) → ℝ) : EqOn (leftFaceReflection d m i a u) u (cube d) := by intro x hx have hxi : -1 ≤ x i := (hx i).1 simp [leftFaceReflection, not_lt.mpr hxi]
RectangularCutoffFunction 2 core · 0 supporting A fixed smooth cutoff equals one on the normalized cube and vanishes near the boundary of a prescribed larger closed box. ★ exists_rectangular_smooth_cutoff
Smooth cutoffs between nested rectangular boxes
A fixed smooth cutoff equals one on the normalized cube and vanishes near the boundary of a prescribed larger closed box. Its finitely many derivatives are uniformly bounded by constants depending only on the boxes and order.
The open coordinate box with corners lo and hi consists of the points lying strictly between lo_i and hi_i in every coordinate i.
If the box with corners lo and hi strictly contains the normalized cube in every coordinate, that is lo_i < −1 and 1 < hi_i, then for any order m there is a smooth function χ equal to one on the cube, with closed support inside the open box, whose ambient derivatives of every order up to m + 1 are bounded in operator norm by a positive constant B.
Formal statement
Proof (Lean source)
RectangularCutoffZero 2 core · 1 supporting Multiplying a response by a smooth cutoff supported strictly inside the box makes its zero extension smooth across the boundary of that box. ★ rectCutoffExtension_contDiff_eqOn_cube
Zero extension of a localized rectangular response
Multiplying a response by a smooth cutoff supported strictly inside the box makes its zero extension smooth across the boundary of that box.
The cutoff extension of a response v by a cutoff χ from the closed box with corners lo and hi takes, at a point x, the value χ(x)·v(x) when x lies in the box and zero otherwise.
If the box with corners lo, hi strictly contains the normalized cube, a cutoff χ is smooth with closed support inside the open box and equal to one on the cube, and a response v is m times continuously differentiable within the closed box, then the zero extension of χ·v from the closed box is m times continuously differentiable on the whole space and agrees with v on the cube.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
rectCutoffExtension_contDifftheorem — If a cutoff χ is smooth and its closed support lies inside the open box, and a response v is m times continuously differentiable within the closed box, then the zero extension of χ·v from the closed box is m times continuously differentiable on the whole space. No normalization of the cutoff on the cube is needed.hypothesesd :ℕm :ℕlo hi :Fin d → ℝχ v :(Fin d → ℝ) → ℝhχ :ContDiff ℝ ∞ χhsupp :tsupport χ ⊆ rectOpenBox lo hihv :ContDiffOn ℝ m v (rectBox lo hi)conclusionContDiff ℝ m (rectCutoffExtension lo hi χ v)Proof (Lean source)
theorem rectCutoffExtension_contDiff {d : ℕ} (m : ℕ) (lo hi : Fin d → ℝ) (χ v : (Fin d → ℝ) → ℝ) (hχ : ContDiff ℝ ∞ χ) (hsupp : tsupport χ ⊆ rectOpenBox lo hi) (hv : ContDiffOn ℝ m v (rectBox lo hi)) : ContDiff ℝ m (rectCutoffExtension lo hi χ v) := by have hopen : IsOpen (rectOpenBox lo hi) := by have h := isOpen_set_pi (Set.finite_univ : (Set.univ : Set (Fin d)).Finite) (s := fun i => Ioo (lo i) (hi i)) (fun i _ => isOpen_Ioo) simpa [rectOpenBox, pi, Set.mem_Ioo] using h have hsub : rectOpenBox lo hi ⊆ rectBox lo hi := by intro x hx i exact ⟨(hx i).1.le, (hx i).2.le⟩ rw [contDiff_iff_contDiffAt] intro x by_cases hx : x ∈ rectOpenBox lo hi · have hvx : ContDiffAt ℝ m v x := hv.contDiffAt (Filter.mem_of_superset (hopen.mem_nhds hx) hsub) have hprod : ContDiffAt ℝ m (fun y => χ y * v y) x := hχ.contDiffAt.of_le (by exact_mod_cast le_top) |>.mul hvx apply hprod.congr_of_eventuallyEq filter_upwards [hopen.mem_nhds hx] with y hy simp [rectCutoffExtension, hsub hy] · have hnot : x ∉ tsupport χ := fun h => hx (hsupp h) have hnhds : (tsupport χ)ᶜ ∈ nhds x := (isClosed_tsupport χ).isOpen_compl.mem_nhds hnot have hzero : ContDiffAt ℝ m (fun _ : Fin d → ℝ => (0 : ℝ)) x := contDiffAt_const apply hzero.congr_of_eventuallyEq filter_upwards [hnhds] with y hy have hχy : χ y = 0 := image_eq_zero_of_notMem_tsupport hy by_cases hbox : y ∈ rectBox lo hi <;> simp [rectCutoffExtension, hbox, hχy]
ReflectionGeometry 3 core · 3 supporting An exterior point in a thin collar of the left face has finitely many reflected sample points inside the closed cube. ★ leftFaceSample_mem_cube
Geometry of inward samples at a cube face
An exterior point in a thin collar of the left face has finitely many reflected sample points inside the closed cube. These affine samples are the arguments of the one-sided reflection operator.
The inward reflection sample of a point x across the left face in coordinate i, with dilation index q, in dimension d, replaces the i-th coordinate of x by −1 + (q + 1)·(−1 − x_i) and keeps every other coordinate; it reflects a point just outside the face to a point q + 1 times as far inside.
The open exterior collar at the left face of the normalized cube in dimension d, for derivative order m and coordinate i, is the set of points whose i-th coordinate lies strictly between −1 − 1/(m + 1) and −1 and whose other coordinates lie strictly between −1 and 1.
If the i-th coordinate of x lies in [-1 - 1/(m+1), -1], so that x is at most 1/(m + 1) outside the left face, and every other coordinate of x lies in [-1,1], then for every dilation index q ≤ m the inward reflection sample of x lies in the closed normalized cube.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
leftFaceSample_mem_openCubetheorem — If x lies in the open exterior collar at the left face in coordinate i, then for every dilation index q ≤ m, the inward reflection sample of x lies in the open normalized cube.hypothesesconclusionleftFaceSample d i q x ∈ openCube dProof (Lean source)
theorem leftFaceSample_mem_openCube {d m : ℕ} (i : Fin d) (q : Fin (m + 1)) (x : Fin d → ℝ) (hx : x ∈ leftOpenCubeCollar d m i) : leftFaceSample d i q x ∈ openCube d := by have hxi : x i ∈ Ioo (-1 - (1 : ℝ) / ((m : ℝ) + 1)) (-1) := by simpa [leftOpenCubeCollar] using hx i have ht0 : 0 < -1 - x i := by linarith [hxi.2] have ht1 : -1 - x i < 1 / ((m : ℝ) + 1) := by linarith [hxi.1] have hq : ((q : ℕ) : ℝ) + 1 ≤ (m : ℝ) + 1 := by exact_mod_cast (succ_le_of_lt q.isLt) have hprod : (((q : ℕ) : ℝ) + 1) * (-1 - x i) < 1 := by calc _ ≤ ((m : ℝ) + 1) * (-1 - x i) := mul_le_mul_of_nonneg_right hq ht0.le _ < ((m : ℝ) + 1) * (1 / ((m : ℝ) + 1)) := mul_lt_mul_of_pos_left ht1 (by positivity) _ = 1 := by field_simp have hpos : 0 < (((q : ℕ) : ℝ) + 1) * (-1 - x i) := mul_pos (by positivity) ht0 intro j hj by_cases hji : j = i · subst j simpa [leftFaceSample] using (show -1 < -1 + (((q : ℕ) : ℝ) + 1) * (-1 - x i) ∧ -1 + (((q : ℕ) : ℝ) + 1) * (-1 - x i) < 1 by constructor <;> linarith) · simpa [leftFaceSample, leftOpenCubeCollar, hji] using hx j -
leftFaceSample_othertheorem — If coordinate j differs from the face coordinate i, then the inward reflection sample of a point leaves its j-th coordinate unchanged.hypothesesconclusionleftFaceSample d i q x j = x jProof (Lean source)
theorem leftFaceSample_other {d : ℕ} (i j : Fin d) (q : ℕ) (x : Fin d → ℝ) (hji : j ≠ i) : leftFaceSample d i q x j = x j := by simp [leftFaceSample, hji] -
leftFaceSample_fixedtheorem — If a point x lies on the left face, that is its i-th coordinate equals −1, then every inward reflection sample of x equals x.Proof (Lean source)
theorem leftFaceSample_fixed {d : ℕ} (i : Fin d) (q : ℕ) (x : Fin d → ℝ) (hxi : x i = -1) : leftFaceSample d i q x = x := by ext j by_cases h : j = i · subst j simp [leftFaceSample, hxi] · exact leftFaceSample_other i j q x h
JetBounds 3 core · 6 supporting This independent module packages ordinary ambient value, derivative, and Hessian bounds. ★ value_holder
Real bounds for scalar jets through order two
This independent module packages ordinary ambient value, derivative, and Hessian bounds. Compact support and order-two regularity imply such bounds. Mean-value and elementary power interpolation yield single-function Hölder estimates.
Uniform order-two jet data for a scalar function with a common bound consist of a nonnegative bound, global order-two regularity, and bounds for its value, first derivative, and second derivative.
Bandwidth-weighted jet data for an exponent β, bandwidth h, function, and constant C consist of a nonnegative constant, global order-two regularity, and bounds, at every point, of C·h^β on the absolute value, C·h^(β−1) on the norm of the first derivative, and C·h^(β−2) on the norm of the second derivative.
Scaled jet bounds with exponent β, bandwidth h and constant C give the bandwidth-independent Hölder bound |f(x) − f(y)| ≤ 2C‖x − y‖^β for all points x and y when the exponent β lies in (0,1] and the bandwidth is positive.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
jets_zero_of_eventually_zerotheorem — At a point where a scalar function is zero on a neighborhood, its value and both ambient jets vanish, without a differentiability hypothesis.hypothesesProof (Lean source)
theorem jets_zero_of_eventually_zero {f : E → ℝ} (x : E) (hf : ∀ᶠ y in nhds x, f y = 0) : f x = 0 ∧ fderiv ℝ f x = 0 ∧ fderiv ℝ (fderiv ℝ f) x = 0 := by have h0 : f =ᶠ[nhds x] (fun _ => (0 : ℝ)) := hf refine ⟨h0.eq_of_nhds, ?_, ?_⟩ · simpa using h0.fderiv_eq (𝕜 := ℝ) · simpa using (h0.fderiv (𝕜 := ℝ)).fderiv_eq (𝕜 := ℝ) -
exists_jetBounds_of_compactSupporttheorem — A globally twice continuously differentiable function with compact support admits a finite common bound on all three jets.hypothesesProof (Lean source)
theorem exists_jetBounds_of_compactSupport {f : E → ℝ} (hf : ContDiff ℝ 2 f) (hc : HasCompactSupport f) : ∃ C : ℝ, 1 ≤ C ∧ JetBounds f C := by have hdf : ContDiff ℝ 1 (fderiv ℝ f) := (contDiff_succ_iff_fderiv.mp hf).2.2 obtain ⟨C₀, h₀⟩ := hf.continuous.bounded_above_of_compact_support hc obtain ⟨C₁, h₁⟩ := hdf.continuous.bounded_above_of_compact_support (hc.fderiv ℝ) obtain ⟨C₂, h₂⟩ := (hdf.continuous_fderiv (by norm_num)).bounded_above_of_compact_support ((hc.fderiv ℝ).fderiv ℝ) refine ⟨max 1 (max C₀ (max C₁ C₂)), le_max_left _ _, ?_⟩ have hC₀ : C₀ ≤ max 1 (max C₀ (max C₁ C₂)) := (le_max_left _ _).trans (le_max_right _ _) have hC₁ : C₁ ≤ max 1 (max C₀ (max C₁ C₂)) := (le_max_left _ _).trans ((le_max_right _ _).trans (le_max_right _ _)) have hC₂ : C₂ ≤ max 1 (max C₀ (max C₁ C₂)) := (le_max_right _ _).trans ((le_max_right _ _).trans (le_max_right _ _)) refine ⟨(by positivity), hf, ?_, fun x => (h₁ x).trans hC₁, fun x => (h₂ x).trans hC₂⟩ intro x simpa only [Real.norm_eq_abs] using (h₀ x).trans hC₀ -
value_lipschitztheorem — Scaled first-jet bounds imply a global scalar Lipschitz estimate for the exponent and bandwidth at any two points.hypothesesconclusion|f x - f y| ≤ C * h ^ (β - 1) * ‖x - y‖Proof (Lean source)
theorem ScaledJetBounds.value_lipschitz {β h C : ℝ} {f : E → ℝ} (hf : ScaledJetBounds β h f C) (x y : E) : |f x - f y| ≤ C * h ^ (β - 1) * ‖x - y‖ := by simpa only [Real.norm_eq_abs] using Convex.norm_image_sub_le_of_norm_fderiv_le (fun z (_ : z ∈ univ) => (hf.regularity.differentiable (by norm_num)) z) (fun z _ => hf.first z) convex_univ (Set.mem_univ y) (Set.mem_univ x) -
first_lipschitztheorem — Scaled second-jet bounds imply a global derivative Lipschitz estimate for the exponent and bandwidth at any two points.hypothesesconclusion‖fderiv ℝ f x - fderiv ℝ f y‖ ≤ C * h ^ (β - 2) * ‖x - y‖Proof (Lean source)
theorem ScaledJetBounds.first_lipschitz {β h C : ℝ} {f : E → ℝ} (hf : ScaledJetBounds β h f C) (x y : E) : ‖fderiv ℝ f x - fderiv ℝ f y‖ ≤ C * h ^ (β - 2) * ‖x - y‖ := by have hdf : ContDiff ℝ 1 (fderiv ℝ f) := (contDiff_succ_iff_fderiv.mp hf.regularity).2.2 exact Convex.norm_image_sub_le_of_norm_fderiv_le (fun z (_ : z ∈ univ) => (hdf.differentiable (by norm_num)) z) (fun z _ => hf.second z) convex_univ (Set.mem_univ y) (Set.mem_univ x) -
scaled_min_holdertheorem — A nonnegative quantity bounded both by a scaled supremum and a scaled Lipschitz bound has the interpolated Hölder bound when the exponent s lies in (0,1], the bandwidth is positive, and the constant and distance are nonnegative.hypothesesa C h r s :ℝha :0 ≤ ahC :0 ≤ Chh :0 < hhr :0 ≤ rhs :0 < shs1 :s ≤ 1hsup :a ≤ 2 * C * h ^ shlip :a ≤ C * h ^ (s - 1) * rconclusiona ≤ 2 * C * r ^ sProof (Lean source)
theorem scaled_min_holder {a C h r s : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (hh : 0 < h) (hr : 0 ≤ r) (hs : 0 < s) (hs1 : s ≤ 1) (hsup : a ≤ 2 * C * h ^ s) (hlip : a ≤ C * h ^ (s - 1) * r) : a ≤ 2 * C * r ^ s := by by_cases hr0 : r = 0 · subst r have ha0 : a = 0 := le_antisymm (by simpa only [mul_zero] using hlip) ha simp only [ha0, Real.zero_rpow hs.ne', mul_zero, le_refl] have hrpos : 0 < r := lt_of_le_of_ne hr (Ne.symm hr0) by_cases hrh : r ≤ h · have hp : h ^ (s - 1) ≤ r ^ (s - 1) := Real.rpow_le_rpow_of_nonpos hrpos hrh (by linarith) have heq : r ^ (s - 1) * r = r ^ s := by calc r ^ (s - 1) * r = r ^ (s - 1) * r ^ (1 : ℝ) := by rw [Real.rpow_one] _ = r ^ (s - 1 + 1) := (Real.rpow_add hrpos _ _).symm _ = r ^ s := by congr 1; ring calc a ≤ C * h ^ (s - 1) * r := hlip _ ≤ C * r ^ (s - 1) * r := mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hp hC) hr _ = C * r ^ s := by rw [mul_assoc, heq] _ ≤ 2 * C * r ^ s := by have := Real.rpow_nonneg hr s nlinarith [mul_nonneg hC this] · exact hsup.trans (mul_le_mul_of_nonneg_left (Real.rpow_le_rpow hh.le (le_of_not_ge hrh) hs.le) (by positivity)) -
first_holdertheorem — Scaled jet bounds give a bandwidth-independent derivative Hölder modulus when the exponent β lies in (1,2] and the bandwidth is positive.hypothesesE :sharedType u_1β h C :ℝf :E → ℝhf :ScaledJetBounds β h f Chβ :1 < βhβ2 :β ≤ 2hh :0 < hx y :Econclusion‖fderiv ℝ f x - fderiv ℝ f y‖ ≤ 2 * C * ‖x - y‖ ^ (β - 1)Proof (Lean source)
theorem ScaledJetBounds.first_holder {β h C : ℝ} {f : E → ℝ} (hf : ScaledJetBounds β h f C) (hβ : 1 < β) (hβ2 : β ≤ 2) (hh : 0 < h) (x y : E) : ‖fderiv ℝ f x - fderiv ℝ f y‖ ≤ 2 * C * ‖x - y‖ ^ (β - 1) := by apply scaled_min_holder (norm_nonneg _) hf.nonneg hh (norm_nonneg _) (by linarith : 0 < β - 1) (by linarith : β - 1 ≤ 1) · calc ‖fderiv ℝ f x - fderiv ℝ f y‖ ≤ ‖fderiv ℝ f x‖ + ‖fderiv ℝ f y‖ := norm_sub_le _ _ _ ≤ 2 * C * h ^ (β - 1) := by linarith [hf.first x, hf.first y] · simpa only [show β - 1 - 1 = β - 2 by ring] using hf.first_lipschitz x y
ReflectionClosedExterior 2 core · 0 supporting The finite reflection sum inherits within-set regularity on the closed exterior part of a one-face cube collar. ★ leftFaceReflection_contDiffOn_closedExterior
Regularity on the closed exterior face slab
The finite reflection sum inherits within-set regularity on the closed exterior part of a one-face cube collar. This includes its edges and corners, where ambient derivatives of an arbitrary representative need not exist.
The closed exterior slab of the normalized cube's left collar in dimension d, for derivative order m and coordinate i, is the part of that collar whose i-th coordinate is at most −1, that is, on or beyond the left face.
Definition (Lean source)
If the reflection weights a sum to one, so that the reflection reproduces constants, and a response u is m times continuously differentiable within the closed cube, then the one-face reflection of u across the left face in coordinate i is m times continuously differentiable within the closed exterior slab of the left collar, including all exterior edges and corners.
Formal statement
Proof (Lean source)
RectangularFaceGeometry 3 core · 2 supporting The affine normalizer of a nondegenerate box also identifies its lower-face collar with the corresponding normalized cube collar. ★ rectAffine_normalize_denormalize
Geometry of normalized rectangular face collars
The affine normalizer of a nondegenerate box also identifies its lower-face collar with the corresponding normalized cube collar. These elementary facts isolate the geometry needed for quantitative reflection transport.
The lower corner of the left collar of the box with corners lo and hi, for derivative order m and coordinate i, agrees with lo except in coordinate i, where it is lowered by the fraction 1/(2(m + 1)) of the side length hi_i − lo_i.
The left collar of the box with corners lo and hi, for derivative order m and coordinate i, is the closed box that extends the original box past its lower face in coordinate i only, by the fraction 1/(2(m + 1)) of that coordinate's side length.
If the box with corners lo, hi has positive side lengths, then mapping a point from the normalized cube's coordinates to the box's coordinates and back returns the original point, for every point of the ambient space.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
rectAffine_leftCollar_eq_normalizetheorem — If the box with corners lo, hi has positive side lengths, then at every point x, the affine map sending the left collar of the box in coordinate i onto the left collar of the normalized cube coincides with the affine map sending the original box onto the normalized cube.hypothesesconclusionrectAffine (rectLeftLower lo hi m i) hi (fun j => if j = i then -1 - (1 : ℝ) / ((m : ℝ) + 1) else -1) (fun _ => 1) x= rectAffine lo hi (fun _ => -1) (fun _ => 1) xProof (Lean source)
theorem rectAffine_leftCollar_eq_normalize {d : ℕ} (lo hi : Fin d → ℝ) (m : ℕ) (i : Fin d) (hbox : ∀ j, lo j < hi j) (x : Fin d → ℝ) : rectAffine (rectLeftLower lo hi m i) hi (fun j => if j = i then -1 - (1 : ℝ) / ((m : ℝ) + 1) else -1) (fun _ => 1) x = rectAffine lo hi (fun _ => -1) (fun _ => 1) x := by funext j by_cases hji : j = i · subst j have hp : 0 < hi i - lo i := sub_pos.mpr (hbox i) have hw : hi i - lo i ≠ 0 := ne_of_gt hp have hm : (m : ℝ) + 1 ≠ 0 := by positivity have hw' : hi i - (lo i - (hi i - lo i) / (2 * ((m : ℝ) + 1))) ≠ 0 := by have hpos : 0 < (hi i - lo i) / (2 * ((m : ℝ) + 1)) := by positivity exact ne_of_gt (by linarith) have hslope : (1 - (-1 - (1 : ℝ) / ((m : ℝ) + 1))) / (hi i - (lo i - (hi i - lo i) / (2 * ((m : ℝ) + 1)))) = 2 / (hi i - lo i) := by apply (div_eq_iff hw').2 field_simp [hw, hm] ring simp only [rectAffine, rectLeftLower, ↓reduceIte] rw [hslope] field_simp [hw, hm] ring · simp only [rectAffine, rectLeftLower, hji, ↓reduceIte] -
rectAffine_preimage_leftCubeCollartheorem — If the box with corners lo, hi has positive side lengths, then the affine normalization of the box onto the normalized cube maps the box's left collar in coordinate i exactly onto the normalized cube's left collar in coordinate i, in the sense that the collar is the preimage of the cube's collar.hypothesesconclusionrectAffine lo hi (fun _ => -1) (fun _ => 1) ⁻¹' leftCubeCollar d m i= rectLeftCollar lo hi m iProof (Lean source)
theorem rectAffine_preimage_leftCubeCollar {d : ℕ} (lo hi : Fin d → ℝ) (m : ℕ) (i : Fin d) (hbox : ∀ j, lo j < hi j) : rectAffine lo hi (fun _ => -1) (fun _ => 1) ⁻¹' leftCubeCollar d m i = rectLeftCollar lo hi m i := by let lower : Fin d → ℝ := fun j => if j = i then -1 - (1 : ℝ) / ((m : ℝ) + 1) else -1 have hsource : ∀ j, rectLeftLower lo hi m i j < hi j := by intro j by_cases hji : j = i · subst j have hp : 0 < hi i - lo i := sub_pos.mpr (hbox i) have hpos : 0 < (hi i - lo i) / (2 * ((m : ℝ) + 1)) := by positivity simp only [rectLeftLower, ↓reduceIte] linarith · simpa [rectLeftLower, hji] using hbox j have htarget : ∀ j, lower j < (1 : ℝ) := by intro j by_cases hji : j = i · simp only [lower, hji, ↓reduceIte] have : 0 < (1 : ℝ) / ((m : ℝ) + 1) := by positivity linarith · simp [lower, hji] have hcollar : leftCubeCollar d m i = rectBox lower (fun _ => 1) := by ext x simp only [leftCubeCollar, rectBox, Set.mem_ofPred_eq] constructor <;> intro hx j · by_cases hji : j = i · have hj := hx j simp only [hji, ↓reduceIte, Set.mem_Icc] at hj simp only [lower, hji, ↓reduceIte, Set.mem_Icc] exact hj · have hj := hx j simp only [hji, ↓reduceIte, Set.mem_Icc] at hj simp only [lower, hji, ↓reduceIte, Set.mem_Icc] exact hj · by_cases hji : j = i · have hj := hx j simp only [lower, hji, ↓reduceIte, Set.mem_Icc] at hj simp only [hji, ↓reduceIte, Set.mem_Icc] exact hj · have hj := hx j simp only [lower, hji, ↓reduceIte, Set.mem_Icc] at hj simp only [hji, ↓reduceIte, Set.mem_Icc] exact hj rw [hcollar] have hmap : rectAffine lo hi (fun _ => -1) (fun _ => 1) = rectAffine (rectLeftLower lo hi m i) hi lower (fun _ => 1) := by funext x simpa [lower] using (rectAffine_leftCollar_eq_normalize lo hi m i hbox x).symm rw [hmap, rectAffine_preimage_rectBox _ _ _ _ hsource htarget] rfl
Locality 4 core · 6 supporting The separation interface uses arbitrary closed support sets at a positive scale. ★ signedSum_jets_eq
Separated supports and finite signed-sum locality
The separation interface uses arbitrary closed support sets at a positive scale. The jet interface explicitly requires value, first-jet, and second-jet vanishing off those sets. Finite signed sums reduce to one summand at each point; constants never count the number of indices. This module is independent of the profiles.
Scale separation for a family of supports, bandwidth, and separation factor requires closed supports and distance at least δh between points in distinct supports.
Jet locality for a function family and its supports means values, first jets, and second jets vanish off each support.
For coefficients and a finite scalar family, the signed sum at a point is the finite sum of coefficient times function values.
Definition (Lean source)
If a family of supports is closed and pairwise separated by at least δh with h > 0 and δ > 0, each function of the family vanishes together with its first and second derivatives off its own support, and every function is twice continuously differentiable on the whole space, then for any coefficients σ and any point x of the i-th support the signed sum at x equals σ_i·f_i(x), its derivative at x equals σ_i times the derivative of f_i at x, and its second derivative at x equals σ_i times the second derivative of f_i at x: only the i-th summand contributes.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
uniquetheorem — Under scale separation with positive scale and factor, if a point x lies in the support K_i and in the support K_j, then i = j: a point lies in at most one support.hypothesesE :sharedType u_1h δ :ℝhsep :SupportSeparation K h δhh :0 < hhδ :0 < δi j :ιx :Ehi :x ∈ K ihj :x ∈ K jconclusioni = jProof (Lean source)
theorem SupportSeparation.unique {K : ι → Set E} {h δ : ℝ} (hsep : SupportSeparation K h δ) (hh : 0 < h) (hδ : 0 < δ) {i j : ι} {x : E} (hi : x ∈ K i) (hj : x ∈ K j) : i = j := by by_contra hij have h := hsep.separated i j hij x hi x hj have hp := mul_pos hδ hh simp only [sub_self, norm_zero] at h exact (not_le_of_gt hp) h -
signedSum_contDifftheorem — A finite signed sum is globally twice continuously differentiable when each summand is globally twice continuously differentiable, for any coefficients and family.hypothesesProof (Lean source)
theorem signedSum_contDiff (σ : ι → ℝ) (f : ι → E → ℝ) (hf : ∀ i, ContDiff ℝ 2 (f i)) : ContDiff ℝ 2 (signedSum σ f) := by classical unfold signedSum exact ContDiff.sum fun i _ => by simpa only [smul_eq_mul] using (hf i).const_smul (σ i) -
signedSum_fderivtheorem — For globally order-two summands and any coefficients, the first derivative of the signed sum is the signed sum of derivatives at every point.hypothesesProof (Lean source)
theorem signedSum_fderiv (σ : ι → ℝ) (f : ι → E → ℝ) (hf : ∀ i, ContDiff ℝ 2 (f i)) (x : E) : fderiv ℝ (signedSum σ f) x = ∑ i, σ i • fderiv ℝ (f i) x := by classical unfold signedSum rw [fderiv_fun_sum (fun i _ => ((hf i).differentiable (by norm_num) x).const_mul (σ i))] exact Finset.sum_congr rfl fun i _ => fderiv_const_mul ((hf i).differentiable (by norm_num) x) (σ i) -
signedSum_second_fderivtheorem — For globally order-two summands and any coefficients, the second derivative of the signed sum is the signed sum of second derivatives at every point.hypothesesProof (Lean source)
theorem signedSum_second_fderiv (σ : ι → ℝ) (f : ι → E → ℝ) (hf : ∀ i, ContDiff ℝ 2 (f i)) (x : E) : fderiv ℝ (fderiv ℝ (signedSum σ f)) x = ∑ i, σ i • fderiv ℝ (fderiv ℝ (f i)) x := by classical have hd : ∀ i, Differentiable ℝ (fderiv ℝ (f i)) := fun i => ((hf i).fderiv_right (by norm_num : (1 : WithTop ℕ∞) + 1 ≤ 2)).differentiable_one have heq : fderiv ℝ (signedSum σ f) = fun y => ∑ i, σ i • fderiv ℝ (f i) y := funext (signedSum_fderiv σ f hf) rw [heq, fderiv_fun_sum (u := univ) (A := fun i y => σ i • fderiv ℝ (f i) y) (fun i _ => (hd i x).const_smul (σ i))] exact Finset.sum_congr rfl fun i _ => fderiv_fun_const_smul (hd i x) (σ i) -
signedSum_jets_zerotheorem — For a family with jet locality and global order-two regularity, all signed-sum jets vanish at a point outside every support for any coefficients.hypothesesE :sharedType u_1hloc :JetLocality f Khf :∀ i, ContDiff ℝ 2 (f i)σ :ι → ℝx :Ehx :∀ i, x ∉ K iProof (Lean source)
theorem signedSum_jets_zero {K : ι → Set E} {f : ι → E → ℝ} (hloc : JetLocality f K) (hf : ∀ i, ContDiff ℝ 2 (f i)) (σ : ι → ℝ) (x : E) (hx : ∀ i, x ∉ K i) : signedSum σ f x = 0 ∧ fderiv ℝ (signedSum σ f) x = 0 ∧ fderiv ℝ (fderiv ℝ (signedSum σ f)) x = 0 := by classical refine ⟨?_, ?_, ?_⟩ · simp only [signedSum, hloc.value _ _ (hx _), mul_zero, Finset.sum_const_zero] · rw [signedSum_fderiv σ f hf x] simp only [hloc.first _ _ (hx _), smul_zero, Finset.sum_const_zero] · rw [signedSum_second_fderiv σ f hf x] simp only [hloc.second _ _ (hx _), smul_zero, Finset.sum_const_zero] -
signedSum_sub_outsidetheorem — At a point in one support and a point outside that support, subtracting signed sums splits into that summand's difference and the remaining signed sum at the second point, under separation, positive scale and factor, jet locality, and global order-two regularity.hypothesesE :sharedType u_1h δ :ℝf :ι → E → ℝhsep :SupportSeparation K h δhh :0 < hhδ :0 < δhloc :JetLocality f Khf :∀ i, ContDiff ℝ 2 (f i)σ :ι → ℝi :ιx y :Ehx :x ∈ K ihy :y ∉ K iProof (Lean source)
theorem signedSum_sub_outside {K : ι → Set E} {h δ : ℝ} {f : ι → E → ℝ} (hsep : SupportSeparation K h δ) (hh : 0 < h) (hδ : 0 < δ) (hloc : JetLocality f K) (hf : ∀ i, ContDiff ℝ 2 (f i)) (σ : ι → ℝ) (i : ι) (x y : E) (hx : x ∈ K i) (hy : y ∉ K i) : signedSum σ f x - signedSum σ f y = σ i * (f i x - f i y) - signedSum σ f y := by rw [(signedSum_jets_eq hsep hh hδ hloc hf σ i x hx).1, hloc.value i y hy, sub_zero]
Plateau 4 core · 17 supporting The real extension equals one on the entire half-line r ≤ 1, transitions by the specified quintic on (1,2), and vanishes on r ≥ 2. ★ plateau_contDiff
The exact quintic radial plateau
The real extension equals one on the entire half-line r ≤ 1, transitions by
the specified quintic on (1,2), and vanishes on r ≥ 2. Its real support is
therefore (-∞,2), not a compact interval. On nonnegative radii its support is
contained in [0,2]; composition with a norm is treated in Radial.
At a real radius r, the plateau is one for r ≤ 1, the quintic 1 − 10(r − 1)³ + 15(r − 1)⁴ − 6(r − 1)⁵ for 1 < r < 2, and zero for r ≥ 2.
Definition (Lean source)
At a real radius r, the first plateau jet is the derivative −30(r − 1)² + 60(r − 1)³ − 30(r − 1)⁴ of the transition quintic for 1 < r < 2, and zero elsewhere.
Definition (Lean source)
At a real radius r, the second plateau jet is the second derivative −60(r − 1) + 180(r − 1)² − 120(r − 1)³ of the transition quintic for 1 < r < 2, and zero elsewhere.
Definition (Lean source)
The exact quintic plateau is globally twice continuously differentiable.
Proof (Lean source)
17 supporting declarations (lemmas, instances)
-
plateau_polynomial_hasDerivAttheorem — At every real radius, the transition polynomial has its exact first derivative, before the constant branches are glued.hypothesesr :ℝconclusionHasDerivAt (fun v : ℝ => 1 - 10 * (v - 1) ^ 3 + 15 * (v - 1) ^ 4 - 6 * (v - 1) ^ 5) (-30 * (r - 1) ^ 2 + 60 * (r - 1) ^ 3 - 30 * (r - 1) ^ 4) rProof (Lean source)
theorem plateau_polynomial_hasDerivAt (r : ℝ) : HasDerivAt (fun v : ℝ => 1 - 10 * (v - 1) ^ 3 + 15 * (v - 1) ^ 4 - 6 * (v - 1) ^ 5) (-30 * (r - 1) ^ 2 + 60 * (r - 1) ^ 3 - 30 * (r - 1) ^ 4) r := by have ht := (hasDerivAt_id r).sub_const 1 convert! ((((hasDerivAt_const r (1 : ℝ)).sub ((ht.pow 3).const_mul 10)).add ((ht.pow 4).const_mul 15)).sub ((ht.pow 5).const_mul 6)) using 1 <;> (try simp) <;> ring -
plateau_polynomialD1_hasDerivAttheorem — At every real radius, the first transition polynomial has its exact second derivative, before the constant branches are glued.hypothesesr :ℝconclusionHasDerivAt (fun v : ℝ => -30 * (v - 1) ^ 2 + 60 * (v - 1) ^ 3 - 30 * (v - 1) ^ 4) (-60 * (r - 1) + 180 * (r - 1) ^ 2 - 120 * (r - 1) ^ 3) rProof (Lean source)
theorem plateau_polynomialD1_hasDerivAt (r : ℝ) : HasDerivAt (fun v : ℝ => -30 * (v - 1) ^ 2 + 60 * (v - 1) ^ 3 - 30 * (v - 1) ^ 4) (-60 * (r - 1) + 180 * (r - 1) ^ 2 - 120 * (r - 1) ^ 3) r := by have ht := (hasDerivAt_id r).sub_const 1 convert! ((((ht.pow 2).const_mul (-30)).add ((ht.pow 3).const_mul 60)).sub ((ht.pow 4).const_mul 30)) using 1 <;> (try simp) <;> ring -
plateau_polynomial_factortheorem — At every real radius, the quintic factors into a cubic boundary zero and a positive quadratic on the transition interval.hypothesesr :ℝconclusion1 - 10 * (r - 1) ^ 3 + 15 * (r - 1) ^ 4 - 6 * (r - 1) ^ 5= (2 - r) ^ 3 * (1 + 3 * (r - 1) + 6 * (r - 1) ^ 2)Proof (Lean source)
theorem plateau_polynomial_factor (r : ℝ) : 1 - 10 * (r - 1) ^ 3 + 15 * (r - 1) ^ 4 - 6 * (r - 1) ^ 5 = (2 - r) ^ 3 * (1 + 3 * (r - 1) + 6 * (r - 1) ^ 2) := by ring -
plateau_polynomial_complement_factortheorem — At every real radius, the complement of the quintic factors into a cubic boundary zero and a positive quadratic on the transition interval.hypothesesr :ℝconclusion1 - (1 - 10 * (r - 1) ^ 3 + 15 * (r - 1) ^ 4 - 6 * (r - 1) ^ 5)= (r - 1) ^ 3 * (1 + 3 * (2 - r) + 6 * (2 - r) ^ 2)Proof (Lean source)
theorem plateau_polynomial_complement_factor (r : ℝ) : 1 - (1 - 10 * (r - 1) ^ 3 + 15 * (r - 1) ^ 4 - 6 * (r - 1) ^ 5) = (r - 1) ^ 3 * (1 + 3 * (2 - r) + 6 * (2 - r) ^ 2) := by ring -
plateau_eq_onetheorem — At a radius at most one, the plateau is one.Proof (Lean source)
-
plateau_eq_zerotheorem — At a radius at least two, the plateau vanishes.Proof (Lean source)
theorem plateau_eq_zero (r : ℝ) (hr : 2 ≤ r) : plateau r = 0 := by simp [plateau, show ¬r ≤ 1 by linarith, show ¬r < 2 by linarith] -
plateau_boundstheorem — The plateau lies between zero and one at every real input.Proof (Lean source)
theorem plateau_bounds (r : ℝ) : 0 ≤ plateau r ∧ plateau r ≤ 1 := by by_cases h₁ : r ≤ 1 · simp [plateau, h₁] by_cases h₂ : r < 2 · have ha : 0 ≤ r - 1 := by linarith have hb : 0 ≤ 2 - r := by linarith have hp : 0 ≤ (2 - r) ^ 3 * (1 + 3 * (r - 1) + 6 * (r - 1) ^ 2) := mul_nonneg (pow_nonneg hb 3) (by positivity) have hc : 0 ≤ (r - 1) ^ 3 * (1 + 3 * (2 - r) + 6 * (2 - r) ^ 2) := mul_nonneg (pow_nonneg ha 3) (by positivity) rw [← plateau_polynomial_factor] at hp rw [← plateau_polynomial_complement_factor] at hc simp only [plateau, if_neg h₁, if_pos h₂] exact ⟨hp, by linarith⟩ · simp [plateau, h₁, h₂] -
plateau_supporttheorem — The nonzero support of the real plateau is the radius-two left half-line.Proof (Lean source)
theorem plateau_support : support plateau = Iio 2 := by ext r simp only [Function.mem_support, Set.mem_Iio] constructor · intro h by_contra hn exact h (plateau_eq_zero r (le_of_not_gt hn)) · intro h₂ by_cases h₁ : r ≤ 1 · simp [plateau_eq_one r h₁] · have ha : 0 ≤ r - 1 := by linarith have hb : 0 < 2 - r := by linarith have hp : 0 < (2 - r) ^ 3 * (1 + 3 * (r - 1) + 6 * (r - 1) ^ 2) := mul_pos (pow_pos hb 3) (by positivity) rw [← plateau_polynomial_factor] at hp simpa only [plateau, if_neg h₁, if_pos h₂] using ne_of_gt hp -
plateau_nonnegative_supporttheorem — The support among nonnegative radii is contained in the closed radius-two interval. -
plateau_eventually_onetheorem — The plateau is locally constant one near zero.Proof (Lean source)
theorem plateau_eventually_one : ∀ᶠ r in nhds (0 : ℝ), plateau r = 1 := by filter_upwards [Iio_mem_nhds (show (0 : ℝ) < 1 by norm_num)] with r hr exact plateau_eq_one r (le_of_lt hr) -
plateau_hasDerivAttheorem — At every radius, the plateau has the explicit first derivative.Proof (Lean source)
theorem plateau_hasDerivAt (r : ℝ) : HasDerivAt plateau (plateauD1 r) r := by rw [plateau_eq_join, plateauD1_eq_join] have hi := joinAt_hasDerivAt 2 plateau_polynomial_hasDerivAt (fun x => hasDerivAt_const x (0 : ℝ)) (by norm_num) (by norm_num) exact joinAt_hasDerivAt 1 (fun x => hasDerivAt_const x (1 : ℝ)) hi (by norm_num [joinAt]) (by norm_num [joinAt]) r -
plateauD1_hasDerivAttheorem — At every radius, the first jet has the explicit second derivative.Proof (Lean source)
theorem plateauD1_hasDerivAt (r : ℝ) : HasDerivAt plateauD1 (plateauD2 r) r := by rw [plateauD1_eq_join, plateauD2_eq_join] have hi := joinAt_hasDerivAt 2 plateau_polynomialD1_hasDerivAt (fun x => hasDerivAt_const x (0 : ℝ)) (by norm_num) (by norm_num) exact joinAt_hasDerivAt 1 (fun x => hasDerivAt_const x (0 : ℝ)) hi (by norm_num [joinAt]) (by norm_num [joinAt]) r -
plateau_deriv_of_transitiontheorem — At a radius in the transition region, the first derivative has the exact quintic derivative formula.hypothesesr :ℝhr :1 < r ∧ r < 2Proof (Lean source)
theorem plateau_deriv_of_transition (r : ℝ) (hr : 1 < r ∧ r < 2) : deriv plateau r = -30 * (r - 1) ^ 2 + 60 * (r - 1) ^ 3 - 30 * (r - 1) ^ 4 := by simp [plateau_deriv, plateauD1, hr] -
plateau_second_deriv_of_transitiontheorem — At a radius in the transition region, the second derivative has the exact quintic second derivative formula.hypothesesr :ℝhr :1 < r ∧ r < 2Proof (Lean source)
theorem plateau_second_deriv_of_transition (r : ℝ) (hr : 1 < r ∧ r < 2) : deriv (deriv plateau) r = -60 * (r - 1) + 180 * (r - 1) ^ 2 - 120 * (r - 1) ^ 3 := by simp [plateau_deriv_two, plateauD2, hr] -
plateau_jets_zerotheorem — At a radius outside the open transition region, both derivative jets vanish, including radii one and two.hypothesesr :ℝhr :r ≤ 1 ∨ 2 ≤ rProof (Lean source)
theorem plateau_jets_zero (r : ℝ) (hr : r ≤ 1 ∨ 2 ≤ r) : deriv plateau r = 0 ∧ deriv (deriv plateau) r = 0 := by have hn : ¬(1 < r ∧ r < 2) := by intro h rcases hr with hr | hr <;> linarith [h.1, h.2] rw [plateau_deriv_two, plateau_deriv] simp [plateauD1, plateauD2, hn]
Profiles 4 core · 9 supporting The profile is coordinate zero times the product of all cutoffs in positive dimension. ★ oddProduct_jetBounds
Odd products of exact coordinate cutoffs
The profile is coordinate zero times the product of all cutoffs in positive dimension. In dimension zero it is defined to be zero. Both the sup-norm coordinate space and its Euclidean counterpart are exposed.
In a finite dimension, the closed coordinate support is the set where every coordinate has absolute value at most one.
At a coordinate vector x in dimension d, the odd product profile is the first coordinate of x times the product over all coordinates i of the cutoff of x_i when d is positive, and zero in dimension zero; the cutoff of a real u is (1 − u²)³ for |u| ≤ 1 and zero otherwise.
At a Euclidean vector x in dimension d, the Euclidean odd profile is the odd product profile evaluated at the coordinates of x; only the norm on the domain differs from the coordinate version.
Definition (Lean source)
In every dimension d there is a constant C ≥ 1 such that the odd product profile is twice continuously differentiable on the whole space and its absolute value, the operator norm of its derivative and the operator norm of its second derivative are all at most C at every point.
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
oddProduct_dim_zerotheorem — The dimension-zero odd profile is identically zero.conclusionoddProduct (d := 0) = fun _ => 0Proof (Lean source)
theorem oddProduct_dim_zero : oddProduct (d := 0) = fun _ => 0 := by funext x simp [oddProduct] -
oddProduct_negtheorem — The odd product changes sign under simultaneous coordinate negation in every dimension at every point.Proof (Lean source)
theorem oddProduct_neg {d : ℕ} (x : Fin d → ℝ) : oddProduct (-x) = -oddProduct x := by by_cases hd : 0 < d · simp [oddProduct, hd, cutoff_neg] · simp [oddProduct, hd] -
oddProduct_hasCompactSupporttheorem — The odd product has compact support in every finite dimension.Proof (Lean source)
-- Reuse the cube argument of CubeExtension.productBump_hasCompactSupport: -- `isCompact_pi_infinite (fun _ => isCompact_Icc)` and -- `HasCompactSupport.intro`. Off the cube, one cutoff factor is zero. -- The d = 0 branch is identically zero; do not introduce a positive-dimension premise. theorem oddProduct_hasCompactSupport {d : ℕ} : HasCompactSupport (oddProduct (d := d)) := by classical apply HasCompactSupport.intro (K := {x : Fin d → ℝ | ∀ i, x i ∈ Icc (-1) 1}) (isCompact_pi_infinite (fun _ => isCompact_Icc)) intro x hx have hx' : ¬∀ i, |x i| ≤ 1 := by simpa only [Set.mem_ofPred_eq, Set.mem_Icc, ← abs_le] using hx obtain ⟨i, hi⟩ := not_forall.mp hx' have hz : ∏ j : Fin d, cutoff (x j) = 0 := Finset.prod_eq_zero (Finset.mem_univ i) (by simp [cutoff, hi]) simp [oddProduct, hz] -
oddProduct_contDifftheorem — The odd product is globally twice continuously differentiable in every finite dimension.Proof (Lean source)
-- Split `0 < d`, then use `contDiff_prod`, `cutoff_contDiff.comp`, -- the coordinate evaluation continuous linear maps, and `ContDiff.mul`. theorem oddProduct_contDiff {d : ℕ} : ContDiff ℝ 2 (oddProduct (d := d)) := by classical change ContDiff ℝ 2 (fun x : Fin d → ℝ => oddProduct x) by_cases hd : 0 < d · simp only [oddProduct, dif_pos hd] apply ContDiff.mul · fun_prop · apply contDiff_prod intro i _ exact cutoff_contDiff.comp (by fun_prop) · simpa only [oddProduct, dif_neg hd] using (contDiff_const : ContDiff ℝ 2 (fun _ : Fin d → ℝ => (0 : ℝ))) -
oddProduct_jets_zerotheorem — At a point off the closed coordinate support in dimension, the value and both ambient jets vanish.hypothesesProof (Lean source)
-- Failure of closed coordinate support supplies a STRICT exterior coordinate. -- Its continuous absolute value stays > 1 on a neighborhood; the product is -- eventually zero there. Apply the closed `jets_zero_of_eventually_zero` helper. theorem oddProduct_jets_zero {d : ℕ} (x : Fin d → ℝ) (hx : x ∉ coordinateSupport d) : oddProduct x = 0 ∧ fderiv ℝ oddProduct x = 0 ∧ fderiv ℝ (fderiv ℝ (oddProduct (d := d))) x = 0 := by classical have hx' : ¬∀ i, |x i| ≤ 1 := hx obtain ⟨i, hi⟩ := not_forall.mp hx' have hcont : Continuous (fun y : Fin d → ℝ => |y i|) := (continuous_apply i).abs have hnear : ∀ᶠ y in nhds x, 1 < |y i| := hcont.continuousAt.eventually (lt_mem_nhds (lt_of_not_ge hi)) apply jets_zero_of_eventually_zero filter_upwards [hnear] with y hy have hz : ∏ j : Fin d, cutoff (y j) = 0 := Finset.prod_eq_zero (Finset.mem_univ i) (by simp [cutoff, not_le.mpr hy]) simp [oddProduct, hz] -
oddEuclidean_hasCompactSupporttheorem — The Euclidean odd product has compact support in dimension.Proof (Lean source)
-- `EuclideanSpace.equiv (Fin d) ℝ` is the existing continuous linear equivalence -- to the coordinate sup-norm space. Transfer compact support via its homeomorphism. theorem oddEuclidean_hasCompactSupport {d : ℕ} : HasCompactSupport (oddEuclidean (d := d)) := by exact oddProduct_hasCompactSupport.comp_homeomorph (EuclideanSpace.equiv (Fin d) ℝ).toHomeomorph -
oddEuclidean_contDifftheorem — The Euclidean odd product is globally twice continuously differentiable in dimension.Proof (Lean source)
-- Compose `oddProduct_contDiff` with `EuclideanSpace.equiv (Fin d) ℝ`. -- Its coercion evaluates to the same coordinates as the unchanged definition. theorem oddEuclidean_contDiff {d : ℕ} : ContDiff ℝ 2 (oddEuclidean (d := d)) := by exact oddProduct_contDiff.comp (EuclideanSpace.equiv (Fin d) ℝ).contDiff -
oddEuclidean_jets_zerotheorem — All three Euclidean jets vanish at a point in dimension off its closed coordinate support.hypothesesProof (Lean source)
theorem oddEuclidean_jets_zero {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (hx : ¬∀ i, |x i| ≤ 1) : oddEuclidean x = 0 ∧ fderiv ℝ oddEuclidean x = 0 ∧ fderiv ℝ (fderiv ℝ (oddEuclidean (d := d))) x = 0 := by classical obtain ⟨i, hi⟩ := not_forall.mp hx have hcont : Continuous (fun y : EuclideanSpace ℝ (Fin d) => |y i|) := ((continuous_apply i).comp (EuclideanSpace.equiv (Fin d) ℝ).continuous).abs have hnear : ∀ᶠ y in nhds x, 1 < |y i| := hcont.continuousAt.eventually (lt_mem_nhds (lt_of_not_ge hi)) apply jets_zero_of_eventually_zero filter_upwards [hnear] with y hy have hz : ∏ j : Fin d, cutoff (y j) = 0 := Finset.prod_eq_zero (Finset.mem_univ i) (by simp [cutoff, not_le.mpr hy]) simp [oddEuclidean, oddProduct, hz] -
oddEuclidean_jetBoundstheorem — A finite dimension-dependent constant bounds all Euclidean jets through order two in dimension.hypothesesd :ℕProof (Lean source)
theorem oddEuclidean_jetBounds (d : ℕ) : ∃ C : ℝ, 1 ≤ C ∧ JetBounds (oddEuclidean (d := d)) C := by exact exists_jetBounds_of_compactSupport oddEuclidean_contDiff oddEuclidean_hasCompactSupport
Radial 3 core · 3 supporting The mixed profile is the exact tangent odd product multiplied by the quintic plateau of the complementary Euclidean radius. ★ mixedProfile_jetBounds
Odd tangent products with a complementary radial plateau
The mixed profile is the exact tangent odd product multiplied by the quintic plateau of the complementary Euclidean radius. Its support is a coordinate cube times a radius-two ball, and its global jets have dimension-dependent bounds.
In fixed tangent and complementary dimensions, the mixed profile at a Euclidean coordinate vector is the tangent odd product multiplied by the plateau of the complementary Euclidean norm.
Definition (Lean source)
In fixed dimensions, the closed mixed support is the tangent coordinate cube times the complementary radius-two ball.
For every tangent dimension t and complementary dimension c there is a constant C ≥ 1 such that the mixed profile is twice continuously differentiable on the whole space and its absolute value, the operator norm of its derivative and the operator norm of its second derivative are all at most C at every point.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
mixedProfile_hasCompactSupporttheorem — The mixed profile has compact support in fixed dimensions.Proof (Lean source)
-- Split the ambient space using `EuclideanSpace.sumEquivProd`. On the product, -- use the compact set `tsupport oddEuclidean ×ˢ closedBall 0 2`, -- then transfer it through the inverse homeomorphism. Outside this set either -- the tangent factor is zero or `plateau_eq_zero` kills the radial factor. -- Neither individual factor pulled back to the ambient space has compact -- support in general: both coordinate projections can have nontrivial kernels. theorem mixedProfile_hasCompactSupport {t c : ℕ} : HasCompactSupport (mixedProfile (t := t) (c := c)) := by let e : EuclideanSpace ℝ (Fin t ⊕ Fin c) ≃L[ℝ] EuclideanSpace ℝ (Fin t) × EuclideanSpace ℝ (Fin c) := EuclideanSpace.sumEquivProd have hp : HasCompactSupport (fun p : EuclideanSpace ℝ (Fin t) × EuclideanSpace ℝ (Fin c) => oddEuclidean p.1 * plateau ‖p.2‖) := by apply HasCompactSupport.intro (K := tsupport (oddEuclidean (d := t)) ×ˢ closedBall 0 2) (oddEuclidean_hasCompactSupport.isCompact.prod (isCompact_closedBall _ _)) intro p hp by_cases ht : p.1 ∈ tsupport (oddEuclidean (d := t)) · have hc : p.2 ∉ closedBall (0 : EuclideanSpace ℝ (Fin c)) 2 := fun hc => hp ⟨ht, hc⟩ have hr : ¬ ‖p.2‖ ≤ 2 := by simpa using hc rw [plateau_eq_zero _ (lt_of_not_ge hr).le, mul_zero] · rw [image_eq_zero_of_notMem_tsupport ht, zero_mul] exact hp.comp_homeomorph e.toHomeomorph -
mixedProfile_contDifftheorem — The mixed profile is globally twice continuously differentiable in fixed dimensions.Proof (Lean source)
-- Compose `oddEuclidean_contDiff` with the first continuous linear projection -- of `EuclideanSpace.sumEquivProd`, and use `radialPlateau_contDiff` for the -- second projection. Multiply the two C² functions and unfold only to identify -- the exact existing formula. This reuses local constancy at projected zero. -- Primary source: Mathlib/Analysis/InnerProductSpace/PiL2.lean, sumEquivProd, -- and `radialPlateau_contDiff` for the norm composition. theorem mixedProfile_contDiff {t c : ℕ} : ContDiff ℝ 2 (mixedProfile (t := t) (c := c)) := by let e : EuclideanSpace ℝ (Fin t ⊕ Fin c) ≃L[ℝ] EuclideanSpace ℝ (Fin t) × EuclideanSpace ℝ (Fin c) := EuclideanSpace.sumEquivProd let P := (ContinuousLinearMap.fst ℝ (EuclideanSpace ℝ (Fin t)) (EuclideanSpace ℝ (Fin c))).comp e.toContinuousLinearMap let Q := (ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin t)) (EuclideanSpace ℝ (Fin c))).comp e.toContinuousLinearMap exact (oddEuclidean_contDiff.comp P.contDiff).mul (radialPlateau_contDiff Q) -
mixedProfile_jets_zerotheorem — At a point off the mixed closed support in fixed dimensions, the value and both ambient jets vanish.hypothesesProof (Lean source)
-- Negating mixedSupport gives a strict tangent exterior coordinate or a strict -- complementary radius > 2. Continuity keeps that strict inequality on a -- neighborhood, where one factor vanishes. Apply `jets_zero_of_eventually_zero` -- to the whole product, avoiding second-derivative product expansions. -- Keep the t = 0 and c = 0 cases; no positive-dimension hypothesis is needed. theorem mixedProfile_jets_zero {t c : ℕ} (x : EuclideanSpace ℝ (Fin t ⊕ Fin c)) (hx : x ∉ mixedSupport t c) : mixedProfile x = 0 ∧ fderiv ℝ mixedProfile x = 0 ∧ fderiv ℝ (fderiv ℝ (mixedProfile (t := t) (c := c))) x = 0 := by classical apply jets_zero_of_eventually_zero by_cases ht : ∀ i : Fin t, |x (inl i)| ≤ 1 · let e : EuclideanSpace ℝ (Fin t ⊕ Fin c) ≃L[ℝ] EuclideanSpace ℝ (Fin t) × EuclideanSpace ℝ (Fin c) := EuclideanSpace.sumEquivProd let Q := (ContinuousLinearMap.snd ℝ (EuclideanSpace ℝ (Fin t)) (EuclideanSpace ℝ (Fin c))).comp e.toContinuousLinearMap have hr : 2 < ‖Q x‖ := lt_of_not_ge (fun hr => hx ⟨ht, hr⟩) have hnear := Q.continuous.norm.continuousAt.eventually (Ioi_mem_nhds hr) filter_upwards [hnear] with y hy change 2 < ‖(toLp 2 (fun i : Fin c => y (inr i)) : EuclideanSpace ℝ (Fin c))‖ at hy simp only [mixedProfile, plateau_eq_zero _ hy.le, mul_zero] · obtain ⟨i, hi⟩ := not_forall.mp ht have hcont : Continuous (fun y : EuclideanSpace ℝ (Fin t ⊕ Fin c) => |y (inl i)|) := ((continuous_apply (inl i)).comp (EuclideanSpace.equiv (Fin t ⊕ Fin c) ℝ).continuous).abs have hnear := hcont.continuousAt.eventually (Ioi_mem_nhds (lt_of_not_ge hi)) filter_upwards [hnear] with y hy have hz : oddProduct (fun j : Fin t => y (inl j)) = 0 := (oddProduct_jets_zero _ (fun h => (not_le.mpr hy) (h i))).1 simp only [mixedProfile, hz, zero_mul]
RectangularUpperFaceReflection 3 core · 0 supporting This is the upper-face counterpart of rectangular lower-face reflection. ★ exists_rectRightFaceReflection_holder_constant
Controlled reflection across an upper face of a rectangular box
This is the upper-face counterpart of rectangular lower-face reflection. The collar width is a fixed fraction of the side length, so successive reflections can be applied to nondegenerate boxes with quantitative control.
The upper corner of the right collar of the box with corners lo and hi, for derivative order m and coordinate i, agrees with hi except in coordinate i, where it is raised by the fraction 1/(2(m + 1)) of the side length hi_i − lo_i.
The right collar of the box with corners lo and hi, for derivative order m and coordinate i, is the closed box that extends the original box past its upper face in coordinate i only, by the fraction 1/(2(m + 1)) of that coordinate's side length.
If 0 < s and the box with corners lo, hi has positive side lengths, then for derivative order m and coordinate i there is a positive constant C such that every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the box agrees on the box with a response in the intrinsic Hölder ball of radius C·L on the box's right collar in coordinate i. The constant depends only on the box, m, s and i.
Formal statement
Proof (Lean source)
ScalingCore 3 core · 5 supporting Amplitude scaling by a real bandwidth power, inverse dilation, and translation have exact first, second, and iterated derivative identities. ★ scaledCopy_jetBounds
Generic translated and dilated order-two scalar jets
Amplitude scaling by a real bandwidth power, inverse dilation, and translation have exact first, second, and iterated derivative identities. These identities transfer uniform normalized jet bounds and off-support vanishing to scaled copies without depending on a particular cutoff, plateau, or coordinate profile.
For a profile, exponent and bandwidth, and a center, the scaled copy at a point is the translated, inversely dilated profile multiplied by h to the exponent.
Definition (Lean source)
The scaled support of a set at a bandwidth and center is its inverse image under translation and inverse dilation.
If a profile is twice continuously differentiable on the whole space with its values, first derivative, and second derivative all bounded in norm by a nonnegative constant C, then for a positive bandwidth and any exponent β, bandwidth h, and center, the scaled copy is twice continuously differentiable and its values, first derivative, and second derivative are bounded everywhere by C times h to the powers β, β − 1, and β − 2 respectively.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
scaledCopy_contDifftheorem — A globally order-two profile has globally order-two scaled copies for any exponent, bandwidth, and center.hypothesesconclusionContDiff ℝ 2 (scaledCopy β h z f)Proof (Lean source)
theorem scaledCopy_contDiff (β h : ℝ) (z : E) {f : E → ℝ} (hf : ContDiff ℝ 2 f) : ContDiff ℝ 2 (scaledCopy β h z f) := by unfold scaledCopy exact contDiff_const.mul (hf.comp (by fun_prop)) -
scaledCopy_iteratedFDerivtheorem — For an order-two profile, a jet order at most two, an exponent, bandwidth, center, and point, the iterated jet scales by the amplitude and the inverse bandwidth to the jet order.hypothesesconclusioniteratedFDeriv ℝ j (scaledCopy β h z f) x= (h ^ β) • ((h⁻¹) ^ j • iteratedFDeriv ℝ j f (h⁻¹ • (x - z)))Proof (Lean source)
-- Restrict hf to the finite natural order j using hj (casts into WithTop ℕ∞). -- These Mathlib identities include j=0 and h=0; this theorem deliberately -- imposes neither a positive bandwidth nor an infinite-order smoothness premise. theorem scaledCopy_iteratedFDeriv (β h : ℝ) (z x : E) {f : E → ℝ} (hf : ContDiff ℝ 2 f) (j : ℕ) (hj : j ≤ 2) : iteratedFDeriv ℝ j (scaledCopy β h z f) x = (h ^ β) • ((h⁻¹) ^ j • iteratedFDeriv ℝ j f (h⁻¹ • (x - z))) := by have hfj : ContDiff ℝ (j : WithTop ℕ∞) f := hf.of_le (by exact_mod_cast hj) have hg : ContDiff ℝ (j : WithTop ℕ∞) (fun y : E => f (h⁻¹ • y)) := hfj.comp (by fun_prop) have ht : ContDiff ℝ (j : WithTop ℕ∞) (fun y : E => f (h⁻¹ • (y - z))) := hg.comp (by fun_prop) change iteratedFDeriv ℝ j (fun y : E => (h ^ β) • f (h⁻¹ • (y - z))) x = _ rw [iteratedFDeriv_const_smul_apply' ht.contDiffAt] rw [iteratedFDeriv_comp_sub (f := fun y : E => f (h⁻¹ • y)) j z x] rw [iteratedFDeriv_comp_const_smul h⁻¹ hfj] -
scaledCopy_fderivtheorem — For a globally order-two profile and an exponent, bandwidth, center, and point, the ambient first derivative has the expected amplitude and inverse-bandwidth factor.hypothesesconclusionProof (Lean source)
theorem scaledCopy_fderiv (β h : ℝ) (z x : E) {f : E → ℝ} (hf : ContDiff ℝ 2 f) : fderiv ℝ (scaledCopy β h z f) x = (h ^ β * h⁻¹) • fderiv ℝ f (h⁻¹ • (x - z)) := by have ht : ContDiff ℝ 2 (fun y : E => f (h⁻¹ • (y - z))) := hf.comp (by fun_prop) change fderiv ℝ (fun y : E => (h ^ β) • f (h⁻¹ • (y - z))) x = _ rw [fderiv_fun_const_smul (ht.differentiable (by norm_num) x)] rw [fderiv_comp_sub (f := fun y : E => f (h⁻¹ • y)) z, fderiv_comp_smul] rw [smul_smul] -
scaledCopy_second_fderivtheorem — For a globally order-two profile and an exponent, bandwidth, center, and point, the ambient second derivative has the expected amplitude and squared inverse-bandwidth factor.hypothesesconclusionProof (Lean source)
-- First prove scaledCopy_fderiv as an equality of functions (funext). -- Differentiate that identity using C¹ regularity of fderiv f from hf. -- Constant scalar dilation contributes another h⁻¹; no third derivative is needed. theorem scaledCopy_second_fderiv (β h : ℝ) (z x : E) {f : E → ℝ} (hf : ContDiff ℝ 2 f) : fderiv ℝ (fderiv ℝ (scaledCopy β h z f)) x = (h ^ β * (h⁻¹) ^ 2) • fderiv ℝ (fderiv ℝ f) (h⁻¹ • (x - z)) := by have heq : fderiv ℝ (scaledCopy β h z f) = fun y => (h ^ β * h⁻¹) • fderiv ℝ f (h⁻¹ • (y - z)) := by funext y exact scaledCopy_fderiv β h z y hf have hdf : ContDiff ℝ 1 (fderiv ℝ f) := (contDiff_succ_iff_fderiv.mp hf).2.2 have ht : ContDiff ℝ 1 (fun y : E => fderiv ℝ f (h⁻¹ • (y - z))) := hdf.comp (by fun_prop) rw [heq, fderiv_fun_const_smul (ht.differentiable (by norm_num) x)] rw [fderiv_comp_sub (f := fun y : E => fderiv ℝ f (h⁻¹ • y)) z, fderiv_comp_smul, smul_smul] congr 1 ring -
scaledCopy_jets_zerotheorem — If a twice continuously differentiable profile has value and first two derivatives vanishing off a set K, then for any exponent, bandwidth and center, and a point outside the scaled support of K, the scaled copy and its first two derivatives vanish at that point.hypothesesE :sharedType u_1β h :ℝz :Ef :E → ℝK :Set Ehf :ContDiff ℝ 2 fx :Ehx :x ∉ scaledSupport h z Kconclusionconclusion 1scaledCopy β h z f x = 0conclusion 2fderiv ℝ (scaledCopy β h z f) x = 0conclusion 3Proof (Lean source)
theorem scaledCopy_jets_zero (β h : ℝ) (z : E) {f : E → ℝ} {K : Set E} (hf : ContDiff ℝ 2 f) (hzero : ∀ x ∉ K, f x = 0 ∧ fderiv ℝ f x = 0 ∧ fderiv ℝ (fderiv ℝ f) x = 0) (x : E) (hx : x ∉ scaledSupport h z K) : scaledCopy β h z f x = 0 ∧ fderiv ℝ (scaledCopy β h z f) x = 0 ∧ fderiv ℝ (fderiv ℝ (scaledCopy β h z f)) x = 0 := by obtain ⟨hv, h₁, h₂⟩ := hzero (h⁻¹ • (x - z)) hx refine ⟨?_, ?_, ?_⟩ · simp only [scaledCopy, hv, mul_zero] · rw [scaledCopy_fderiv β h z x hf, h₁, smul_zero] · rw [scaledCopy_second_fderiv β h z x hf, h₂, smul_zero]
Affine 2 core · 1 supporting Composing with the coordinatewise affine map x ↦ 2x − 1 or its inverse x ↦ (x + 1)/2 carries the intrinsic Hölder ball of derivative order m and exponent s ∈ (0, 1] on one cube into the Hölder ball on the other, with the ★ unit_holder_affine_transport
Affine transport of Hölder balls between the cubes [0,1]^d and [−1,1]^d
Composing with the coordinatewise affine map x ↦ 2x − 1 or its inverse x ↦ (x + 1)/2 carries the intrinsic Hölder ball of derivative order m and exponent s ∈ (0, 1] on one cube into the Hölder ball on the other, with the radius multiplied by a constant depending only on the dimension d, on m and on s. Results proved on the normalized cube [−1,1]^d therefore transfer to the unit cube [0,1]^d and back.
Main definitions
cubeAffineInv— the map x ↦ (x + 1)/2, coordinate by coordinate, from [−1,1]^d onto [0,1]^d.
Main results
* cube_holder_affine_transport — u in the radius-R Hölder ball on [−1,1]^d implies
x ↦ u(2x − 1) in the radius-C·R Hölder ball on [0,1]^d.
* unit_holder_affine_transport — the converse direction, for x ↦ u((x + 1)/2).
The inverse coordinatewise affine map sends a point x to the point whose i-th coordinate is (x_i + 1)/2; it carries the normalized cube [-1,1]^d onto the unit cube [0,1]^d.
In dimension d, for derivative order m and a Hölder exponent s with 0 < s, there is a positive constant C such that whenever a response u lies in the intrinsic Hölder ball of order m, exponent s and radius R ≥ 0 on the unit cube [0,1]^d, its pullback x ↦ u((x + 1)/2) along the inverse coordinatewise affine map lies in the intrinsic Hölder ball of radius C·R on the normalized cube [-1,1]^d. The constant depends only on d, m and s.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
cube_holder_affine_transporttheorem — In dimension d, for derivative order m and a Hölder exponent s with s ≤ 1, there is a positive constant C such that whenever a response u lies in the intrinsic Hölder ball of order m, exponent s and radius R ≥ 0 on the normalized cube [-1,1]^d, its pullback x ↦ u(2x − 1) along the coordinatewise affine map lies in the intrinsic Hölder ball of radius C·R on the unit cube [0,1]^d. The constant depends only on d, m and s.hypothesesd m :ℕs :ℝhs1 :s ≤ 1conclusion∃ C : ℝ,0 < Cconclusion 1HolderBallOn (unitCube d) m s (C * R) (fun x => u (cubeAffine x))Proof (Lean source)
theorem cube_holder_affine_transport (d m : ℕ) (s : ℝ) (hs1 : s ≤ 1) : ∃ C : ℝ, 0 < C ∧ ∀ (u : (Fin d → ℝ) → ℝ) (R : ℝ), 0 ≤ R → CubeHolderBall d m s R u → HolderBallOn (unitCube d) m s (C * R) (fun x => u (cubeAffine x)) := by refine ⟨(2 : ℝ) ^ (m + 1), by positivity, ?_⟩ intro u R hR hu have hreg : ContDiffOn ℝ m (fun x => u (cubeAffine x)) (unitCube d) := by exact hu.regularity.comp cubeAffine_contDiff.contDiffOn (fun _ hx => cubeAffine_mem_cube hx) refine ⟨hreg, ?_, ?_⟩ · intro j hj f x hx rw [coordJetOn_cubeAffine u f x hx, abs_mul, abs_of_nonneg (by positivity : 0 ≤ (2 : ℝ) ^ j)] calc (2 : ℝ) ^ j * |coordJetOn (cube d) j u f (cubeAffine x)| ≤ (2 : ℝ) ^ j * R := mul_le_mul_of_nonneg_left (hu.derivBound j hj f (cubeAffine x) (cubeAffine_mem_cube hx)) (by positivity) _ ≤ (2 : ℝ) ^ (m + 1) * R := mul_le_mul_of_nonneg_right (pow_le_pow_right₀ (by norm_num : (1 : ℝ) ≤ 2) (Nat.le_succ_of_le hj)) hR · intro f x hx y hy rw [coordJetOn_cubeAffine u f x hx, coordJetOn_cubeAffine u f y hy] have hmod := hu.modulus f (cubeAffine x) (cubeAffine_mem_cube hx) (cubeAffine y) (cubeAffine_mem_cube hy) have hpow : (2 : ℝ) ^ s ≤ 2 := Real.rpow_le_self_of_one_le (by norm_num) hs1 have hn : 0 ≤ ‖x - y‖ ^ s := Real.rpow_nonneg (norm_nonneg _) _ calc |(2 : ℝ) ^ m * coordJetOn (cube d) m u f (cubeAffine x) - (2 : ℝ) ^ m * coordJetOn (cube d) m u f (cubeAffine y)| = (2 : ℝ) ^ m * |coordJetOn (cube d) m u f (cubeAffine x) - coordJetOn (cube d) m u f (cubeAffine y)| := by rw [← mul_sub, abs_mul, abs_of_nonneg (by positivity)] _ ≤ (2 : ℝ) ^ m * (R * ‖cubeAffine x - cubeAffine y‖ ^ s) := mul_le_mul_of_nonneg_left hmod (by positivity) _ = ((2 : ℝ) ^ m * (2 : ℝ) ^ s * R) * ‖x - y‖ ^ s := by rw [cubeAffine_norm_sub, Real.mul_rpow (by norm_num : (0 : ℝ) ≤ 2) (norm_nonneg _)] ring _ ≤ ((2 : ℝ) ^ m * 2 * R) * ‖x - y‖ ^ s := by gcongr _ = (2 : ℝ) ^ (m + 1) * R * ‖x - y‖ ^ s := by rw [pow_succ]
AmbientBridge 2 core · 0 supporting The library carries two Hölder balls on the closed normalized cube [-1,1]^d. ★ cubeHolderBall_of_holderBall★ exists_holderBall_extension
Ambient and within-cube Hölder balls are interchangeable
The library carries two Hölder balls on the closed normalized cube [-1,1]^d. The within-cube
ball CubeHolderBall is the standard one: all derivatives are taken within the cube, so
membership depends only on the values of the function on the cube. The ambient ball
CubeInterpolation.HolderBall takes the derivatives in the whole space, so at boundary points
membership also depends on the function outside the cube.
This file proves that the two describe the same functions on the cube, up to a constant in the
radius; the extension direction, from the within-cube ball to the ambient ball, is proved for
Hölder exponents in (0,1].
Main results
* cubeHolderBall_of_holderBall — a function in the ambient ball of radius R lies in the
within-cube ball of the same radius.
* exists_holderBall_extension — for a Hölder exponent in (0,1] there is a constant A,
depending only on the dimension, the order and the exponent, such that every function in the
within-cube ball of radius L agrees on the cube with a function in the ambient ball of radius
A·L.
A function in the ambient Hölder ball of order m, nonnegative exponent s and radius R on the closed normalized cube lies in the within-cube Hölder ball with the same order, exponent and radius: replacing the whole-space derivatives by derivatives taken within the cube keeps every derivative bound and the top-order Hölder modulus.
Formal statement
Proof (Lean source)
In dimension d, for derivative order m and a Hölder exponent s with 0 < s and s ≤ 1, there is a positive constant A such that every function in the within-cube Hölder ball of order m, exponent s and radius L ≥ 0 on the closed normalized cube agrees on the cube with a function in the ambient Hölder ball of order m, exponent s and radius A·L. The constant depends only on d, m and s, so on the cube the ambient ball and the standard within-cube ball contain the same functions up to this factor in the radius.
Formal statement
Proof (Lean source)
Clamping 2 core · 2 supporting Clamping each coordinate to [-1,1] fixes the cube and is nonexpansive in the supremum norm. ★ cubeClamp_nonexpansive
Coordinatewise retraction onto the normalized cube
Clamping each coordinate to [-1,1] fixes the cube and is nonexpansive in
the supremum norm. This is the extension map for the zero-order Hölder case.
Coordinatewise clamping in dimension d sends a point x to the point whose i-th coordinate is max(−1, min(1, x_i)), that is, x_i truncated to [-1,1]; the result lies in the normalized cube.
Coordinatewise clamping is nonexpansive for the supremum norm: the clamped images of two points are no farther apart than the points themselves.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
cubeClamp_mem_cubetheorem — Every coordinatewise clamped point lies in the normalized closed cube [-1,1]^d. -
cubeClamp_fixedtheorem — Coordinatewise clamping leaves fixed every point already in the normalized cube.Proof (Lean source)
theorem cubeClamp_fixed {d : ℕ} {x : Fin d → ℝ} (hx : x ∈ cube d) : cubeClamp d x = x := by ext i have hi := hx i change -1 ≤ x i ∧ x i ≤ 1 at hi simp [cubeClamp, min_eq_right hi.2, max_eq_right hi.1]
ClosedPieceGluing 1 core · 1 supporting These lemmas isolate the local gluing argument needed when a cube face joins two regions carrying the same response and matching intrinsic jets. ★ contDiffOn_closed_union_of_matching_jets
Differentiability across two closed pieces
These lemmas isolate the local gluing argument needed when a cube face joins two regions carrying the same response and matching intrinsic jets.
If two sets s and t are closed, each has unique within-set derivatives, a function f is m times continuously differentiable within s and within t, and for every order j ≤ m the j-th within-s and within-t derivatives of f agree on s ∩ t, then f is m times continuously differentiable within s ∪ t.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
differentiableOn_closed_union_of_matching_fderivtheorem — If two sets s and t are closed, a function f is differentiable within s and within t, and the within-s and within-t derivatives of f agree at every point of s ∩ t, then f is differentiable within s ∪ t.hypothesesd :ℕhs :IsClosed sht :IsClosed tf :(Fin d → ℝ) → ℝhfs :DifferentiableOn ℝ f shft :DifferentiableOn ℝ f thmatch :∀ x ∈ s ∩ t, fderivWithin ℝ f s x = fderivWithin ℝ f t xconclusionDifferentiableOn ℝ f (s ∪ t)Proof (Lean source)
theorem differentiableOn_closed_union_of_matching_fderiv (d : ℕ) (s t : Set (Fin d → ℝ)) (hs : IsClosed s) (ht : IsClosed t) (f : (Fin d → ℝ) → ℝ) (hfs : DifferentiableOn ℝ f s) (hft : DifferentiableOn ℝ f t) (hmatch : ∀ x ∈ s ∩ t, fderivWithin ℝ f s x = fderivWithin ℝ f t x) : DifferentiableOn ℝ f (s ∪ t) := by intro x hx rcases hx with hx | hx · by_cases hxt : x ∈ t · have hds := (hfs x hx).hasFDerivWithinAt have hdt := (hft x hxt).hasFDerivWithinAt rw [hmatch x ⟨hx, hxt⟩] at hds exact (hds.union hdt).differentiableWithinAt · have hnear : s ∈ nhdsWithin x (s ∪ t) := by filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ht.isOpen_compl.mem_nhds hxt)] with y hy hyt exact hy.resolve_right hyt exact ((hfs x hx).hasFDerivWithinAt.mono_of_mem_nhdsWithin hnear).differentiableWithinAt · by_cases hxs : x ∈ s · have hds := (hfs x hxs).hasFDerivWithinAt have hdt := (hft x hx).hasFDerivWithinAt rw [hmatch x ⟨hxs, hx⟩] at hds exact (hds.union hdt).differentiableWithinAt · have hnear : t ∈ nhdsWithin x (s ∪ t) := by filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (hs.isOpen_compl.mem_nhds hxs)] with y hy hys exact hy.resolve_left hys exact ((hft x hx).hasFDerivWithinAt.mono_of_mem_nhdsWithin hnear).differentiableWithinAt
Completion 1 core · 3 supporting Interior interpolation is stated for within-cube jets. ★ cube_holder_completion
Intrinsic fixed-cube Hölder completion
Interior interpolation is stated for within-cube jets. Continuous traces pass its derivative bounds to every face of the closed cube.
In dimension d, for derivative order m and an exponent s with 0 < s, there is a positive constant K such that every response u that is m times continuously differentiable within the closed cube, bounded in absolute value by M ≥ 0 there, and whose top-order intrinsic jets have an s-Hölder modulus with coefficient L ≥ 0, lies in the intrinsic Hölder ball of order m, exponent s and radius K·(M + L) on the closed cube. The constant depends only on d, m and s.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
interior_coordJet_bound_extendstheorem — If a response u is m times continuously differentiable within the closed normalized cube, j ≤ m, and the order-j intrinsic coordinate jet of u in a fixed choice of coordinate directions is bounded in absolute value by B at every interior point of the cube, then the same bound B holds at every point of the closed cube.hypothesesd m j :ℕ(Fin d → ℝ) → ℝB :ℝhu :ContDiffOn ℝ m u (cube d)hj :j ≤ mhinterior :∀ x ∈ openCube d, |coordJetOn (cube d) j u f x| ≤ Bx ∈ cube d :conclusion|coordJetOn (cube d) j u f x| ≤ BProof (Lean source)
theorem interior_coordJet_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, |coordJetOn (cube d) j u f x| ≤ B) : ∀ x ∈ cube d, |coordJetOn (cube d) j u f x| ≤ B := by apply within_coordPartial_bound_extends hu hj f intro x hx have h := hinterior x hx rw [coordJetOn_cube_eq_ambient hu hj hx] at h exact h -
interior_fixed_cube_interpolation_withintheorem — In any dimension d, for derivative order m and an exponent s with 0 < s, there is a positive constant K such that, for every response u that is m times continuously differentiable within the closed cube, bounded in absolute value by M ≥ 0 there, and whose top-order intrinsic jets have an s-Hölder modulus with coefficient L ≥ 0, every intrinsic coordinate jet of order at most m is bounded in absolute value by K·(M + L) at every interior point of the cube. The constant depends only on d, m and s.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)TopHolderOn (cube d) m s L uj ≤ m :x ∈ openCube d :|coordJetOn (cube d) j u f x| ≤ K * (M + L)Proof (Lean source)
theorem interior_fixed_cube_interpolation_within (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) → TopHolderOn (cube d) m s L u → ∀ j ≤ m, ∀ f : Fin j → Fin d, ∀ x ∈ openCube d, |coordJetOn (cube d) j u f x| ≤ K * (M + L) := by obtain ⟨K, hK, hinterp⟩ := interior_fixed_cube_interpolation d m s hs refine ⟨K, hK, ?_⟩ intro u M L hM hL hu hbound hholder j hj f x hx have hsub : openCube d ⊆ cube d := by intro z hz i exact ⟨(hz i trivial).1.le, (hz i trivial).2.le⟩ have hopen : IsOpen (openCube d) := isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo) have hscaled (t : ℝ) (ht0 : 0 < t) (ht1 : t < 1) (z : Fin d → ℝ) (hz : z ∈ cube d) : t • z ∈ openCube d := by intro i _ have hi := hz i change -1 ≤ z i ∧ z i ≤ 1 at hi change -1 < t * z i ∧ t * z i < 1 constructor <;> nlinarith [mul_nonneg ht0.le (sub_nonneg.mpr hi.1), mul_nonneg ht0.le (sub_nonneg.mpr hi.2)] have hjet (t : ℝ) (ht0 : 0 < t) (ht1 : t < 1) : coordPartial j (fun z => u (t • z)) f x = t ^ j * coordJetOn (cube d) j u f (t • x) := by let g : (Fin d → ℝ) ≃L[ℝ] (Fin d → ℝ) := ContinuousLinearEquiv.smulLeft (R₁ := ℝ) (M₁ := Fin d → ℝ) (Units.mk0 t (ne_of_gt ht0)) have hg (z : Fin d → ℝ) : g z = t • z := by ext i simp [g] have hfun : (fun z => u (t • z)) = u ∘ g := by funext z simp [hg z] have hpreopen : IsOpen (g ⁻¹' openCube d) := hopen.preimage g.continuous have hsource : ContDiffAt ℝ j u (g x) := (hu.mono hsub).contDiffAt (hopen.mem_nhds (by simpa [hg] using hscaled t ht0 ht1 x (hsub hx))) |>.of_le (by exact_mod_cast hj) have htarget : ContDiffAt ℝ j (u ∘ g) x := ((hu.mono hsub).comp g.contDiff.contDiffOn (fun _ hz => hz)).contDiffAt (hpreopen.mem_nhds (by simpa [hg] using hscaled t ht0 ht1 x (hsub hx))) |>.of_le (by exact_mod_cast hj) have hchain := g.iteratedFDerivWithin_comp_right u hopen.uniqueDiffOn (by simpa [hg] using hscaled t ht0 ht1 x (hsub hx)) j rw [coordJetOn_cube_eq_ambient hu hj (hscaled t ht0 ht1 x (hsub hx))] unfold coordPartial rw [hfun] rw [← iteratedFDerivWithin_eq_iteratedFDeriv hpreopen.uniqueDiffOn htarget (by simpa [hg] using hscaled t ht0 ht1 x (hsub hx))] rw [hchain] rw [iteratedFDerivWithin_eq_iteratedFDeriv hopen.uniqueDiffOn hsource (by simpa [hg] using hscaled t ht0 ht1 x (hsub hx))] simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousLinearEquiv.coe_coe] have hb (k : Fin j) : g (single (f k) (1 : ℝ)) = t • single (f k) (1 : ℝ) := hg _ simp only [hb] rw [ContinuousMultilinearMap.map_smul_univ] simp [Finset.prod_const, smul_eq_mul, hg] have hbound_t (t : ℝ) (ht : t ∈ Ioo (0 : ℝ) 1) : |t ^ j * coordJetOn (cube d) j u f (t • x)| ≤ K * (M + L) := by obtain ⟨hreg, hsup, htop⟩ := contracted_cube_ambient_data ht.1 ht.2 hs u hu hbound hholder rw [← hjet t ht.1 ht.2] exact hinterp (fun z => u (t • z)) M L hM hL hreg hsup htop j hj f x hx have hmap : Set.MapsTo (fun t : ℝ => t • x) (Icc (0 : ℝ) 1) (cube d) := by intro t ht i rcases ht with ⟨ht0, ht1⟩ have hi := (hsub hx) i change -1 ≤ x i ∧ x i ≤ 1 at hi change -1 ≤ t * x i ∧ t * x i ≤ 1 constructor <;> nlinarith [mul_nonneg ht0 (by linarith : 0 ≤ x i + 1), mul_nonneg ht0 (by linarith : 0 ≤ 1 - x i)] have hcontsmul : Continuous (fun t : ℝ => t • x) := by fun_prop have hcontjet : ContinuousOn (fun t : ℝ => coordJetOn (cube d) j u f (t • x)) (Icc (0 : ℝ) 1) := (continuousOn_coordJetOn_cube hu hj f).comp hcontsmul.continuousOn hmap have hcont : ContinuousOn (fun t : ℝ => |t ^ j * coordJetOn (cube d) j u f (t • x)|) (Icc (0 : ℝ) 1) := by fun_prop have hclosure : closure (Ioo (0 : ℝ) 1) = Icc 0 1 := by rw [closure_Ioo (by norm_num : (0 : ℝ) ≠ 1)] have hfinal := le_on_closure hbound_t (by simpa [hclosure] using hcont) (by fun_prop : ContinuousOn (fun _ : ℝ => K * (M + L)) (closure (Ioo (0 : ℝ) 1))) (by simp [hclosure] : (1 : ℝ) ∈ closure (Ioo (0 : ℝ) 1)) simpa using hfinal -
fixed_cube_interpolation_withintheorem — In any dimension d, for derivative order m and an exponent s with 0 < s, there is a positive constant K such that, for every response u that is m times continuously differentiable within the closed cube, bounded in absolute value by M ≥ 0 there, and whose top-order intrinsic jets have an s-Hölder modulus with coefficient L ≥ 0, every intrinsic coordinate jet of order at most m is bounded in absolute value by K·(M + L) on the whole closed cube. The constant depends only on d, m and s.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)TopHolderOn (cube d) m s L uDerivBoundOn (cube d) m (K * (M + L)) uProof (Lean source)
theorem fixed_cube_interpolation_within (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) → TopHolderOn (cube d) m s L u → DerivBoundOn (cube d) m (K * (M + L)) u := by obtain ⟨K, hK, hinterior⟩ := interior_fixed_cube_interpolation_within d m s hs refine ⟨K, hK, ?_⟩ intro u M L hM hL hu hbound hholder j hj f x hx exact interior_coordJet_bound_extends hu hj f (hinterior u M L hM hL hu hbound hholder j hj f) x hx
Contraction 1 core · 0 supporting A strict contraction sends the closed cube into its interior. ★ contracted_cube_ambient_data
Contracting intrinsic cube data to ambient cube data
A strict contraction sends the closed cube into its interior. Pulling an intrinsic response back by this contraction gives ambient coordinate jets on the entire closed cube, with the original supremum and Hölder bounds.
If 0 < t and t < 1, s > 0, and a response u is m times continuously differentiable within the closed cube, bounded in absolute value by M on the cube, and has a top-order intrinsic s-Hölder modulus with coefficient L on the cube, then the contracted response x ↦ u(t·x) is m times continuously differentiable within the cube, is still bounded by M on the cube, and its top-order ambient coordinate partial derivatives have an s-Hölder modulus with coefficient L on the cube.
Formal statement
Proof (Lean source)
ConvexJetLipschitz 1 core · 0 supporting On a convex set, a bound on the next within-set Fréchet derivative gives a Lipschitz bound for the preceding jet. ★ norm_iteratedFDerivWithin_sub_le_of_succ_bound
Lipschitz control of lower intrinsic jets
On a convex set, a bound on the next within-set Fréchet derivative gives a Lipschitz bound for the preceding jet. This supplies the lower-order modulus used when a smooth cutoff is multiplied by intrinsic Hölder data.
If a set S is convex and has unique within-set derivatives, a function v is m times continuously differentiable within S, j < m, and the order-(j + 1) within-S derivative of v has operator norm at most R throughout S, then for two points x and y of S the order-j within-S derivatives of v at x and at y differ in operator norm by at most R·‖x − y‖.
Formal statement
Proof (Lean source)
CoordinateLimit 1 core · 0 supporting For multilinear maps on a finite product of finite-dimensional coordinate spaces, convergence on all tuples of coordinate vectors implies convergence in the operator norm. ★ tendsto_multilinearMap_of_coordinate_tendsto
Coordinate criterion for convergence of multilinear maps
For multilinear maps on a finite product of finite-dimensional coordinate spaces, convergence on all tuples of coordinate vectors implies convergence in the operator norm. This isolates the topological step in face trace proofs.
Let F be a family, indexed along a filter, of continuous j-linear maps on d-dimensional coordinate space and T a continuous j-linear map on the same space. If for every tuple of coordinate directions the values of F on the corresponding standard basis vectors converge to the value of T on those vectors, then F converges to T along the filter.
Formal statement
Proof (Lean source)
Cutoff 4 core · 15 supporting This file supplies the compactly supported scalar profile equal to (1-u^2)^3 on |u| ≤ 1 and zero elsewhere, including both glued derivatives. ★ cutoff_contDiff
The exact cubic-power coordinate cutoff
This file supplies the compactly supported scalar profile equal to
(1-u^2)^3 on |u| ≤ 1 and zero elsewhere, including both glued derivatives.
At a scalar input u, the cutoff is (1 − u²)³ when u is at most one in absolute value, and zero otherwise.
Definition (Lean source)
At a scalar input u, the explicit first jet of the cutoff is −6u(1 − u²)², the derivative of (1 − u²)³, when u is at most one in absolute value, and zero otherwise.
Definition (Lean source)
At a scalar input u, the explicit second jet of the cutoff is −6(1 − u²)² + 24u²(1 − u²), the second derivative of (1 − u²)³, when u is at most one in absolute value, and zero otherwise.
Definition (Lean source)
The cutoff is globally twice continuously differentiable.
Proof (Lean source)
15 supporting declarations (lemmas, instances)
-
cutoff_polynomial_hasDerivAttheorem — At every real input, the cubic-power branch has its exact first derivative, before it is glued to the zero branch.Proof (Lean source)
theorem cutoff_polynomial_hasDerivAt (u : ℝ) : HasDerivAt (fun v : ℝ => (1 - v ^ 2) ^ 3) (-6 * u * (1 - u ^ 2) ^ 2) u := by convert! (((hasDerivAt_const u (1 : ℝ)).sub ((hasDerivAt_id u).pow 2)).pow 3) using 1 <;> (try simp) <;> ring -
cutoff_polynomialD1_hasDerivAttheorem — At every real input, the first polynomial branch has its exact second derivative, before either branch is glued.hypothesesu :ℝconclusionHasDerivAt (fun v : ℝ => -6 * v * (1 - v ^ 2) ^ 2) (-6 * (1 - u ^ 2) ^ 2 + 24 * u ^ 2 * (1 - u ^ 2)) uProof (Lean source)
theorem cutoff_polynomialD1_hasDerivAt (u : ℝ) : HasDerivAt (fun v : ℝ => -6 * v * (1 - v ^ 2) ^ 2) (-6 * (1 - u ^ 2) ^ 2 + 24 * u ^ 2 * (1 - u ^ 2)) u := by convert! (((hasDerivAt_id u).const_mul (-6)).mul (((hasDerivAt_const u (1 : ℝ)).sub ((hasDerivAt_id u).pow 2)).pow 2)) using 1 <;> (try simp) <;> ring -
cutoff_boundstheorem — The cutoff lies between zero and one at every scalar input.Proof (Lean source)
-
cutoff_supporttheorem — The nonzero support is exactly the open unit interval.Proof (Lean source)
theorem cutoff_support : support cutoff = Ioo (-1) 1 := by ext u change cutoff u ≠ 0 ↔ -1 < u ∧ u < 1 rw [← abs_lt] constructor · intro h have hle : |u| ≤ 1 := by by_contra hn exact h (by simp [cutoff, hn]) refine lt_of_le_of_ne hle ?_ intro heq have hsq : u ^ 2 = 1 := by nlinarith [sq_abs u] exact h (by simp [cutoff, hle, hsq]) · intro h have hsq : u ^ 2 < 1 := (sq_lt_one_iff_abs_lt_one u).2 h simp only [cutoff, if_pos h.le] exact pow_ne_zero 3 (ne_of_gt (sub_pos.mpr hsq)) -
cutoff_tsupporttheorem — The closed support is exactly the closed unit interval. -
cutoff_hasCompactSupporttheorem — The cutoff has compact support.conclusionProof (Lean source)
theorem cutoff_hasCompactSupport : HasCompactSupport cutoff := by change IsCompact (tsupport cutoff) rw [cutoff_tsupport] exact isCompact_Icc -
cutoff_hasDerivAttheorem — The cutoff has the stated first derivative at every input, including both glue points.Proof (Lean source)
theorem cutoff_hasDerivAt (u : ℝ) : HasDerivAt cutoff (cutoffD1 u) u := by exact cutoff_branch_hasDerivAt (fun v => (1 - v ^ 2) ^ 3) (fun v => -6 * v * (1 - v ^ 2) ^ 2) cutoff_polynomial_hasDerivAt (by norm_num) (by norm_num) (by norm_num) (by norm_num) u -
cutoffD1_hasDerivAttheorem — The explicit first jet has the stated second derivative at every input, including both glue points.Proof (Lean source)
theorem cutoffD1_hasDerivAt (u : ℝ) : HasDerivAt cutoffD1 (cutoffD2 u) u := by exact cutoff_branch_hasDerivAt (fun v => -6 * v * (1 - v ^ 2) ^ 2) (fun v => -6 * (1 - v ^ 2) ^ 2 + 24 * v ^ 2 * (1 - v ^ 2)) cutoff_polynomialD1_hasDerivAt (by norm_num) (by norm_num) (by norm_num) (by norm_num) u -
cutoff_deriv_of_abs_letheorem — At an input in the closed polynomial region, the first derivative has the exact polynomial formula.Proof (Lean source)
theorem cutoff_deriv_of_abs_le (u : ℝ) (hu : |u| ≤ 1) : deriv cutoff u = -6 * u * (1 - u ^ 2) ^ 2 := by simp [cutoff_deriv, cutoffD1, hu] -
cutoff_second_deriv_of_abs_letheorem — At an input in the closed polynomial region, the second derivative has the exact polynomial formula.hypothesesu :ℝhu :|u| ≤ 1Proof (Lean source)
theorem cutoff_second_deriv_of_abs_le (u : ℝ) (hu : |u| ≤ 1) : deriv (deriv cutoff) u = -6 * (1 - u ^ 2) ^ 2 + 24 * u ^ 2 * (1 - u ^ 2) := by simp [cutoff_deriv_two, cutoffD2, hu] -
cutoff_jets_zerotheorem — At an input on or outside the unit boundary, the value and both ordinary jets vanish.hypothesesu :ℝhu :1 ≤ |u|Proof (Lean source)
theorem cutoff_jets_zero (u : ℝ) (hu : 1 ≤ |u|) : cutoff u = 0 ∧ deriv cutoff u = 0 ∧ deriv (deriv cutoff) u = 0 := by rw [cutoff_deriv_two, cutoff_deriv] by_cases hle : |u| ≤ 1 · have heq : |u| = 1 := le_antisymm hle hu have hsq : u ^ 2 = 1 := by nlinarith [sq_abs u] simp [cutoff, cutoffD1, cutoffD2, hle, hsq] · simp [cutoff, cutoffD1, cutoffD2, hle]
Extension 1 core · 0 supporting An intrinsic cube Hölder ball admits an ambient representative with uniform quantitative derivative bounds. ★ exists_global_holder_extension
Controlled extension of intrinsic cube Hölder data
An intrinsic cube Hölder ball admits an ambient representative with uniform quantitative derivative bounds. The representative agrees with the original response on the cube; the original response itself need not have valid ambient boundary derivatives.
In dimension d, for derivative order m and a Hölder exponent s with 0 < s and s ≤ 1, there is a positive constant A such that every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the closed normalized cube has an extension U to the whole space that agrees with u on the cube, is m times continuously differentiable, has ambient derivatives of every order at most m bounded in operator norm by A·L everywhere, and whose order-m derivative is globally s-Hölder with coefficient A·L. The constant depends only on d, m and s.
Formal statement
Proof (Lean source)
FixedCubeNeighborhood 1 core · 0 supporting Finite iteration of the two-face reflection theorem enlarges every face of the normalized cube with one uniform Hölder radius factor. ★ exists_fixedCubeNeighborhood_holder_constant
A controlled rectangular neighborhood of the fixed cube
Finite iteration of the two-face reflection theorem enlarges every face of the normalized cube with one uniform Hölder radius factor.
In dimension d, for derivative order m and a Hölder exponent s with 0 < s, there are a closed coordinate box strictly containing the normalized cube in every coordinate and a positive constant C such that every response in the intrinsic Hölder ball of radius L ≥ 0 on the cube agrees on the cube with a response in the intrinsic Hölder ball of radius C·L on that box. The box and the constant depend only on d, m and s.
Formal statement
Proof (Lean source)
Glue 2 core · 2 supporting The reusable gluing lemmas in this file assemble scalar branches with matching value, first derivative, and second derivative at a single junction. ★ joinAt_contDiff_two
Scalar gluing through two derivatives
The reusable gluing lemmas in this file assemble scalar branches with matching value, first derivative, and second derivative at a single junction. They do not assume that the branches agree on a neighborhood of the junction.
The join of two scalar branches f and g at a junction a, evaluated at a point x, equals f(x) when x ≤ a and g(x) otherwise.
Definition (Lean source)
Twice continuously differentiable scalar branches whose value, first derivative, and second derivative match at the junction have a globally twice continuously differentiable join.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
joinAt_continuoustheorem — Continuous branches with matching junction values have a continuous join at the junction.hypothesesconclusionContinuous (joinAt a f g)Proof (Lean source)
theorem joinAt_continuous (a : ℝ) {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (hv : f a = g a) : Continuous (joinAt a f g) := by apply hf.if (p := fun x => x ≤ a) _ hg intro x hx have hx' : x = a := by simpa only [show {x : ℝ | x ≤ a} = Iic a from rfl, frontier_Iic, Set.mem_singleton_iff] using hx simpa only [hx'] using hv -
joinAt_hasDerivAttheorem — Differentiable branches with specified derivative functions and matching value and derivative at a junction have the joined derivative at every point.hypothesesa :ℝf g df dg :ℝ → ℝhf :∀ x, HasDerivAt f (df x) xhg :∀ x, HasDerivAt g (dg x) xhv :f a = g ahd :df a = dg ax :ℝconclusionProof (Lean source)
theorem joinAt_hasDerivAt (a : ℝ) {f g df dg : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (df x) x) (hg : ∀ x, HasDerivAt g (dg x) x) (hv : f a = g a) (hd : df a = dg a) (x : ℝ) : HasDerivAt (joinAt a f g) (joinAt a df dg x) x := by rcases lt_trichotomy x a with hxa | hEq | hax · simp only [joinAt, if_pos hxa.le] apply (hf x).congr_of_eventuallyEq filter_upwards [Iio_mem_nhds hxa] with y hy simp only [joinAt, if_pos (le_of_lt (Set.mem_Iio.mp hy))] · subst x simp only [joinAt, if_pos le_rfl] have hl : HasDerivWithinAt (joinAt a f g) (df a) (Iic a) a := (hf a).hasDerivWithinAt.congr (fun y hy => by simp only [joinAt, if_pos (Set.mem_Iic.mp hy)]) (by simp only [joinAt, if_pos le_rfl]) have hr : HasDerivWithinAt (joinAt a f g) (df a) (Ioi a) a := by rw [hd] exact (hg a).hasDerivWithinAt.congr (fun y hy => by simp only [joinAt, if_neg (not_le_of_gt (Set.mem_Ioi.mp hy))]) (by simpa only [joinAt, if_pos le_rfl] using hv) simpa only [Set.Iic_union_Ioi, hasDerivWithinAt_univ] using hl.union hr · simp only [joinAt, if_neg (not_le_of_gt hax)] apply (hg x).congr_of_eventuallyEq filter_upwards [Ioi_mem_nhds hax] with y hy simp only [joinAt, if_neg (not_le_of_gt (Set.mem_Ioi.mp hy))]
Holder 3 core · 9 supporting Real inequalities for values and ambient derivative operator norms are primary. ★ scaledSignedSum_uniform_holder
Cardinality-independent Hölder bounds for disjoint signed sums
Real inequalities for values and ambient derivative operator norms are primary. The coefficient depends on the normalized profile bound and the fixed support separation factor, never the bandwidth, centers, signs, or index cardinality. The final bridge uses CubeExtension's intrinsic coordinate jets and HolderBallOn.
Uniform Hölder data for an exponent, radius, and function consist of a nonnegative radius, global order-two regularity, a scalar sup bound, a scalar β-Hölder bound when β ≤ 1, and a first-derivative sup bound and (β-1)-Hölder bound when β > 1.
Definition (Lean source)
For an exponent and bandwidth, signs, and an unweighted profile family, the amplitude-scaled signed sum at a point is h to the exponent times the finite signed sum.
Definition (Lean source)
The amplitude-scaled signed sum h^β·Σ_i σ_i p_i satisfies the uniform Hölder bounds of exponent β with radius 2C(1 + 1/δ) provided the supports K_i are closed and pairwise at distance at least δh, and each profile p_i and its first two derivatives vanish outside K_i, each profile is twice continuously differentiable with value at most C, first derivative at most C/h and second derivative at most C/h² in norm everywhere, C is nonnegative, β lies in (0,2], h lies in (0,1], δ is positive, and every sign σ_i is at most one in absolute value.
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
signedSum_value_boundtheorem — A scale-separated signed sum with jet locality, single-profile scaled bounds, a nonnegative constant, and coefficients of absolute value at most one has the single-profile scalar sup bound, for positive bandwidth and factor, any exponent, and every point.hypothesesE :sharedType u_1β h δ C :ℝf :ι → E → ℝhsep :SupportSeparation K h δhh :0 < hhδ :0 < δhloc :JetLocality f Khbound :∀ i, ScaledJetBounds β h (f i) ChC :0 ≤ Cσ :ι → ℝhσ :∀ i, |σ i| ≤ 1x :Econclusion|signedSum σ f x| ≤ C * h ^ βProof (Lean source)
theorem signedSum_value_bound {K : ι → Set E} {β h δ C : ℝ} {f : ι → E → ℝ} (hsep : SupportSeparation K h δ) (hh : 0 < h) (hδ : 0 < δ) (hloc : JetLocality f K) (hbound : ∀ i, ScaledJetBounds β h (f i) C) (hC : 0 ≤ C) (σ : ι → ℝ) (hσ : ∀ i, |σ i| ≤ 1) (x : E) : |signedSum σ f x| ≤ C * h ^ β := by classical by_cases hx : ∃ i, x ∈ K i · obtain ⟨i, hi⟩ := hx rw [(signedSum_jets_eq hsep hh hδ hloc (fun i => (hbound i).regularity) σ i x hi).1, abs_mul] exact (mul_le_mul_of_nonneg_right (hσ i) (abs_nonneg _)).trans (by simpa using (hbound i).value x) · rw [(signedSum_jets_zero hloc (fun i => (hbound i).regularity) σ x (not_exists.mp hx)).1, abs_zero] exact mul_nonneg hC (Real.rpow_nonneg hh.le _) -
signedSum_first_boundtheorem — A scale-separated signed sum with jet locality, single-profile scaled bounds, a nonnegative constant, and coefficients of absolute value at most one has the single-profile first-jet bound, for positive bandwidth and factor, any exponent, and every point.hypothesesE :sharedType u_1β h δ C :ℝf :ι → E → ℝhsep :SupportSeparation K h δhh :0 < hhδ :0 < δhloc :JetLocality f Khbound :∀ i, ScaledJetBounds β h (f i) ChC :0 ≤ Cσ :ι → ℝhσ :∀ i, |σ i| ≤ 1x :Econclusion‖fderiv ℝ (signedSum σ f) x‖ ≤ C * h ^ (β - 1)Proof (Lean source)
theorem signedSum_first_bound {K : ι → Set E} {β h δ C : ℝ} {f : ι → E → ℝ} (hsep : SupportSeparation K h δ) (hh : 0 < h) (hδ : 0 < δ) (hloc : JetLocality f K) (hbound : ∀ i, ScaledJetBounds β h (f i) C) (hC : 0 ≤ C) (σ : ι → ℝ) (hσ : ∀ i, |σ i| ≤ 1) (x : E) : ‖fderiv ℝ (signedSum σ f) x‖ ≤ C * h ^ (β - 1) := by classical by_cases hx : ∃ i, x ∈ K i · obtain ⟨i, hi⟩ := hx rw [(signedSum_jets_eq hsep hh hδ hloc (fun i => (hbound i).regularity) σ i x hi).2.1, norm_smul, Real.norm_eq_abs] exact (mul_le_mul_of_nonneg_right (hσ i) (norm_nonneg _)).trans (by simpa using (hbound i).first x) · rw [(signedSum_jets_zero hloc (fun i => (hbound i).regularity) σ x (not_exists.mp hx)).2.1, norm_zero] exact mul_nonneg hC (Real.rpow_nonneg hh.le _) -
separated_distance_holdertheorem — A quantity with a scaled sup bound is bounded by the separated-distance Hölder coefficient when distance is at least δh, bandwidth and separation factor are positive, the constant and distance are nonnegative, and the exponent lies in (0,1].hypothesesa C h δ r s :ℝhC :0 ≤ Chh :0 < hhδ :0 < δhr :0 ≤ rhs :0 < shs1 :s ≤ 1hsep :δ * h ≤ rhaC :a ≤ 2 * C * h ^ sconclusiona ≤ (2 * C * (1 + δ⁻¹)) * r ^ sProof (Lean source)
theorem separated_distance_holder {a C h δ r s : ℝ} (hC : 0 ≤ C) (hh : 0 < h) (hδ : 0 < δ) (hr : 0 ≤ r) (hs : 0 < s) (hs1 : s ≤ 1) (hsep : δ * h ≤ r) (haC : a ≤ 2 * C * h ^ s) : a ≤ (2 * C * (1 + δ⁻¹)) * r ^ s := by have hi : 0 ≤ δ⁻¹ := inv_nonneg.mpr hδ.le have hp : δ⁻¹ ^ s ≤ 1 + δ⁻¹ := by by_cases hi1 : δ⁻¹ ≤ 1 · exact (Real.rpow_le_one hi hi1 hs.le).trans (by linarith) · have := Real.rpow_le_rpow_of_exponent_le (le_of_not_ge hi1) hs1 rw [Real.rpow_one] at this linarith have hhr : h ≤ δ⁻¹ * r := by calc h = δ⁻¹ * (δ * h) := by rw [← mul_assoc, inv_mul_cancel₀ hδ.ne', one_mul] _ ≤ δ⁻¹ * r := mul_le_mul_of_nonneg_left hsep hi calc a ≤ 2 * C * h ^ s := haC _ ≤ 2 * C * (δ⁻¹ * r) ^ s := mul_le_mul_of_nonneg_left (Real.rpow_le_rpow hh.le hhr hs.le) (by positivity) _ = 2 * C * (δ⁻¹ ^ s * r ^ s) := by rw [Real.mul_rpow hi hr] _ ≤ 2 * C * ((1 + δ⁻¹) * r ^ s) := by gcongr _ = (2 * C * (1 + δ⁻¹)) * r ^ s := by ring -
signedSum_value_holdertheorem — With separated supports, jet locality, single-profile scaled bounds with a nonnegative constant, and bounded signs, the signed sum has a cardinality-independent scalar β-Hölder modulus for β in (0,1] and positive bandwidth and separation factor.hypothesesE :sharedType u_1β h δ C :ℝf :ι → E → ℝhsep :SupportSeparation K h δhh :0 < hhδ :0 < δhloc :JetLocality f Khbound :∀ i, ScaledJetBounds β h (f i) ChC :0 ≤ Chβ :0 < βhβ1 :β ≤ 1σ :ι → ℝhσ :∀ i, |σ i| ≤ 1x y :EProof (Lean source)
theorem signedSum_value_holder {K : ι → Set E} {β h δ C : ℝ} {f : ι → E → ℝ} (hsep : SupportSeparation K h δ) (hh : 0 < h) (hδ : 0 < δ) (hloc : JetLocality f K) (hbound : ∀ i, ScaledJetBounds β h (f i) C) (hC : 0 ≤ C) (hβ : 0 < β) (hβ1 : β ≤ 1) (σ : ι → ℝ) (hσ : ∀ i, |σ i| ≤ 1) (x y : E) : |signedSum σ f x - signedSum σ f y| ≤ (2 * C * (1 + δ⁻¹)) * ‖x - y‖ ^ β := by classical have hreg : ∀ i, ContDiff ℝ 2 (f i) := fun i => (hbound i).regularity have hcoef : 2 * C ≤ 2 * C * (1 + δ⁻¹) := by have : 0 ≤ δ⁻¹ := inv_nonneg.mpr hδ.le nlinarith have heq (i : ι) (z : E) (hz : z ∈ K i) : signedSum σ f z = σ i • f i z := by simpa only [smul_eq_mul] using (signedSum_jets_eq hsep hh hδ hloc hreg σ i z hz).1 have hzero (z : E) (hz : ∀ i, z ∉ K i) : signedSum σ f z = 0 := (signedSum_jets_zero hloc hreg σ z hz).1 have hsingle (i : ι) (u v : E) : ‖σ i • f i u - σ i • f i v‖ ≤ (2 * C * (1 + δ⁻¹)) * ‖u - v‖ ^ β := by rw [← smul_sub, norm_smul, Real.norm_eq_abs] calc _ ≤ ‖f i u - f i v‖ := by simpa using mul_le_mul_of_nonneg_right (hσ i) (norm_nonneg (f i u - f i v)) _ ≤ 2 * C * ‖u - v‖ ^ β := by simpa only [Real.norm_eq_abs] using (hbound i).value_holder hβ hβ1 hh u v _ ≤ _ := mul_le_mul_of_nonneg_right hcoef (Real.rpow_nonneg (norm_nonneg _) _) simp only [← Real.norm_eq_abs] change ‖signedSum σ f x - signedSum σ f y‖ ≤ _ by_cases hx : ∃ i, x ∈ K i · obtain ⟨i, hi⟩ := hx by_cases hy : ∃ j, y ∈ K j · obtain ⟨j, hj⟩ := hy by_cases hij : i = j · subst j rw [heq i x hi, heq i y hj] exact hsingle i x y · apply separated_distance_holder hC hh hδ (norm_nonneg _) hβ hβ1 (hsep.separated i j hij x hi y hj) calc _ ≤ ‖signedSum σ f x‖ + ‖signedSum σ f y‖ := norm_sub_le _ _ _ ≤ 2 * C * h ^ β := by have hxbound := signedSum_value_bound hsep hh hδ hloc hbound hC σ hσ x have hybound := signedSum_value_bound hsep hh hδ hloc hbound hC σ hσ y simp only [Real.norm_eq_abs] linarith · have hyoff := not_exists.mp hy rw [heq i x hi, hzero y hyoff] have hpzero : f i y = 0 := hloc.value i y (hyoff i) simpa only [hpzero, smul_zero, sub_zero] using hsingle i x y · have hxoff := not_exists.mp hx by_cases hy : ∃ j, y ∈ K j · obtain ⟨j, hj⟩ := hy rw [hzero x hxoff, heq j y hj] have hpzero : f j x = 0 := hloc.value j x (hxoff j) simpa only [hpzero, smul_zero, zero_sub] using hsingle j x y · rw [hzero x hxoff, hzero y (not_exists.mp hy)] simp only [sub_self, norm_zero] positivity -
signedSum_first_holdertheorem — With separated supports, jet locality, single-profile scaled bounds with a nonnegative constant, and bounded signs, the signed sum has a cardinality-independent derivative (β-1)-Hölder modulus for β in (1,2] and positive bandwidth and separation factor.hypothesesE :sharedType u_1β h δ C :ℝf :ι → E → ℝhsep :SupportSeparation K h δhh :0 < hhδ :0 < δhloc :JetLocality f Khbound :∀ i, ScaledJetBounds β h (f i) ChC :0 ≤ Chβ :1 < βhβ2 :β ≤ 2σ :ι → ℝhσ :∀ i, |σ i| ≤ 1x y :EProof (Lean source)
theorem signedSum_first_holder {K : ι → Set E} {β h δ C : ℝ} {f : ι → E → ℝ} (hsep : SupportSeparation K h δ) (hh : 0 < h) (hδ : 0 < δ) (hloc : JetLocality f K) (hbound : ∀ i, ScaledJetBounds β h (f i) C) (hC : 0 ≤ C) (hβ : 1 < β) (hβ2 : β ≤ 2) (σ : ι → ℝ) (hσ : ∀ i, |σ i| ≤ 1) (x y : E) : ‖fderiv ℝ (signedSum σ f) x - fderiv ℝ (signedSum σ f) y‖ ≤ (2 * C * (1 + δ⁻¹)) * ‖x - y‖ ^ (β - 1) := by classical have hreg : ∀ i, ContDiff ℝ 2 (f i) := fun i => (hbound i).regularity have hcoef : 2 * C ≤ 2 * C * (1 + δ⁻¹) := by have : 0 ≤ δ⁻¹ := inv_nonneg.mpr hδ.le nlinarith have heq (i : ι) (z : E) (hz : z ∈ K i) : fderiv ℝ (signedSum σ f) z = σ i • fderiv ℝ (f i) z := by exact (signedSum_jets_eq hsep hh hδ hloc hreg σ i z hz).2.1 have hzero (z : E) (hz : ∀ i, z ∉ K i) : fderiv ℝ (signedSum σ f) z = 0 := (signedSum_jets_zero hloc hreg σ z hz).2.1 have hsingle (i : ι) (u v : E) : ‖σ i • fderiv ℝ (f i) u - σ i • fderiv ℝ (f i) v‖ ≤ (2 * C * (1 + δ⁻¹)) * ‖u - v‖ ^ (β - 1) := by rw [← smul_sub, norm_smul, Real.norm_eq_abs] calc _ ≤ ‖fderiv ℝ (f i) u - fderiv ℝ (f i) v‖ := by simpa using mul_le_mul_of_nonneg_right (hσ i) (norm_nonneg _) _ ≤ 2 * C * ‖u - v‖ ^ (β - 1) := by exact (hbound i).first_holder hβ hβ2 hh u v _ ≤ _ := mul_le_mul_of_nonneg_right hcoef (Real.rpow_nonneg (norm_nonneg _) _) change ‖fderiv ℝ (signedSum σ f) x - fderiv ℝ (signedSum σ f) y‖ ≤ _ by_cases hx : ∃ i, x ∈ K i · obtain ⟨i, hi⟩ := hx by_cases hy : ∃ j, y ∈ K j · obtain ⟨j, hj⟩ := hy by_cases hij : i = j · subst j rw [heq i x hi, heq i y hj] exact hsingle i x y · apply separated_distance_holder hC hh hδ (norm_nonneg _) (by linarith : 0 < β - 1) (by linarith : β - 1 ≤ 1) (hsep.separated i j hij x hi y hj) calc _ ≤ ‖fderiv ℝ (signedSum σ f) x‖ + ‖fderiv ℝ (signedSum σ f) y‖ := norm_sub_le _ _ _ ≤ 2 * C * h ^ (β - 1) := by have hxbound := signedSum_first_bound hsep hh hδ hloc hbound hC σ hσ x have hybound := signedSum_first_bound hsep hh hδ hloc hbound hC σ hσ y linarith · have hyoff := not_exists.mp hy rw [heq i x hi, hzero y hyoff] have hpzero : fderiv ℝ (f i) y = 0 := hloc.first i y (hyoff i) simpa only [hpzero, smul_zero, sub_zero] using hsingle i x y · have hxoff := not_exists.mp hx by_cases hy : ∃ j, y ∈ K j · obtain ⟨j, hj⟩ := hy rw [hzero x hxoff, heq j y hj] have hpzero : fderiv ℝ (f j) x = 0 := hloc.first j x (hxoff j) simpa only [hpzero, smul_zero, zero_sub] using hsingle j x y · rw [hzero x hxoff, hzero y (not_exists.mp hy)] simp only [sub_self, norm_zero] positivity -
signedSum_uniform_holdertheorem — Under the generic separation and locality interfaces, single-profile scaled bounds with nonnegative constant, β in (0,2], h in (0,1], positive separation factor, and bounded signs, the finite signed sum satisfies the uniform Hölder bounds of exponent β with radius 2C(1 + 1/δ), a radius independent of the bandwidth and of the number of summands.hypothesesE :sharedType u_1β h δ C :ℝf :ι → E → ℝhsep :SupportSeparation K h δhh :0 < hhh1 :h ≤ 1hδ :0 < δhloc :JetLocality f Khbound :∀ i, ScaledJetBounds β h (f i) ChC :0 ≤ Chβ :0 < βhβ2 :β ≤ 2σ :ι → ℝhσ :∀ i, |σ i| ≤ 1conclusionUniformHolderBounds β (2 * C * (1 + δ⁻¹)) (signedSum σ f)Proof (Lean source)
theorem signedSum_uniform_holder {K : ι → Set E} {β h δ C : ℝ} {f : ι → E → ℝ} (hsep : SupportSeparation K h δ) (hh : 0 < h) (hh1 : h ≤ 1) (hδ : 0 < δ) (hloc : JetLocality f K) (hbound : ∀ i, ScaledJetBounds β h (f i) C) (hC : 0 ≤ C) (hβ : 0 < β) (hβ2 : β ≤ 2) (σ : ι → ℝ) (hσ : ∀ i, |σ i| ≤ 1) : UniformHolderBounds β (2 * C * (1 + δ⁻¹)) (signedSum σ f) := by have hcoef : C ≤ 2 * C * (1 + δ⁻¹) := by have : 0 ≤ δ⁻¹ := inv_nonneg.mpr hδ.le nlinarith refine ⟨by positivity, signedSum_contDiff σ f (fun i => (hbound i).regularity), ?_, ?_, ?_, ?_⟩ · intro x exact (signedSum_value_bound hsep hh hδ hloc hbound hC σ hσ x).trans ((mul_le_mul_of_nonneg_left (Real.rpow_le_one hh.le hh1 hβ.le) hC).trans (by simpa using hcoef)) · intro hβ1 x y exact signedSum_value_holder hsep hh hδ hloc hbound hC hβ hβ1 σ hσ x y · intro hβ1 x exact (signedSum_first_bound hsep hh hδ hloc hbound hC σ hσ x).trans ((mul_le_mul_of_nonneg_left (Real.rpow_le_one hh.le hh1 (by linarith : 0 ≤ β - 1)) hC).trans (by simpa using hcoef)) · intro hβ1 x y exact signedSum_first_holder hsep hh hδ hloc hbound hC hβ1 hβ2 σ hσ x y -
signedSum_contDiffOntheorem — A finite signed sum has order-two regularity on any supplied set, in particular on any supplied closed cube, when its summands are globally order-two regular, for any coefficients, family, and set.hypothesesE :sharedType u_1ι :sharedType u_2σ :ι → ℝf :ι → E → ℝhf :∀ i, ContDiff ℝ 2 (f i)S :Set EconclusionContDiffOn ℝ 2 (signedSum σ f) SProof (Lean source)
theorem signedSum_contDiffOn (σ : ι → ℝ) (f : ι → E → ℝ) (hf : ∀ i, ContDiff ℝ 2 (f i)) (S : Set E) : ContDiffOn ℝ 2 (signedSum σ f) S := by exact (signedSum_contDiff σ f hf).contDiffOn -
holderBallOn_of_uniformBoundstheorem — Ambient real uniform Hölder bounds of exponent β and radius R imply membership in the intrinsic Hölder ball of radius R on the set, of order 0 and exponent β when β ≤ 1 and of order 1 and exponent β − 1 otherwise, on a set with unique differentiability.hypothesesconclusionHolderBallOn S (if β ≤ 1 then 0 else 1) (if β ≤ 1 then β else β - 1) R fProof (Lean source)
theorem holderBallOn_of_uniformBounds {d : ℕ} {S : Set (Fin d → ℝ)} {β R : ℝ} {f : (Fin d → ℝ) → ℝ} (hS : UniqueDiffOn ℝ S) (hf : UniformHolderBounds β R f) : HolderBallOn S (if β ≤ 1 then 0 else 1) (if β ≤ 1 then β else β - 1) R f := by classical have hzero (v : Fin 0 → Fin d) (x : Fin d → ℝ) : coordJetOn S 0 f v x = f x := by exact iteratedFDerivWithin_zero_apply _ have hone (v : Fin 1 → Fin d) (x : Fin d → ℝ) (hx : x ∈ S) : coordJetOn S 1 f v x = fderiv ℝ f x (single (v 0) (1 : ℝ)) := by unfold coordJetOn rw [iteratedFDerivWithin_eq_iteratedFDeriv hS (hf.regularity.contDiffAt.of_le (by norm_num)) hx, iteratedFDeriv_one_apply] have heval (T : (Fin d → ℝ) →L[ℝ] ℝ) (i : Fin d) : |T (single i (1 : ℝ))| ≤ ‖T‖ := by calc _ = ‖T (single i (1 : ℝ))‖ := (Real.norm_eq_abs _).symm _ ≤ ‖T‖ * ‖(single i (1 : ℝ) : Fin d → ℝ)‖ := T.le_opNorm _ _ = ‖T‖ := by simp only [Pi.norm_single, norm_one, mul_one] by_cases hb : β ≤ 1 · simp only [if_pos hb] refine ⟨hf.regularity.contDiffOn.of_le (by norm_num), ?_, ?_⟩ · intro j hj v x hx have hj0 : j = 0 := by omega subst j rw [hzero] exact hf.value x · intro v x hx y hy rw [hzero, hzero] exact hf.value_modulus hb x y · simp only [if_neg hb] have hb1 : 1 < β := lt_of_not_ge hb refine ⟨hf.regularity.contDiffOn.of_le (by norm_num), ?_, ?_⟩ · intro j hj v x hx rcases Nat.le_one_iff_eq_zero_or_eq_one.mp hj with rfl | rfl · rw [hzero] exact hf.value x · rw [hone v x hx] exact (heval _ _).trans (hf.first hb1 x) · intro v x hx y hy rw [hone v x hx, hone v y hy, ← sub_apply] exact (heval _ _).trans (hf.first_modulus hb1 x y) -
holderBallOn_cube_of_uniformBoundstheorem — Ambient uniform Hölder bounds of exponent β and radius R give membership in the same-radius intrinsic Hölder ball on the normalized closed cube, of order 0 and exponent β when β ≤ 1 and of order 1 and exponent β − 1 otherwise.hypothesesconclusionHolderBallOn (cube d) (if β ≤ 1 then 0 else 1) (if β ≤ 1 then β else β - 1) R fProof (Lean source)
theorem holderBallOn_cube_of_uniformBounds {d : ℕ} {β R : ℝ} {f : (Fin d → ℝ) → ℝ} (hf : UniformHolderBounds β R f) : HolderBallOn (cube d) (if β ≤ 1 then 0 else 1) (if β ≤ 1 then β else β - 1) R f := by apply holderBallOn_of_uniformBounds (hf := hf) have hcube : cube d = Set.univ.pi (fun _ : Fin d => Icc (-1 : ℝ) 1) := by ext x simp [cube, normalizedCube, Pi.le_def, forall_and] rw [hcube] exact UniqueDiffOn.pi (fun _ _ => uniqueDiffOn_Icc (by norm_num))
JetNorm 1 core · 1 supporting Finite-dimensional coordinate bounds control the operator norm of a multilinear derivative. ★ exists_full_intrinsic_jet_bounds
From coordinate jets to full multilinear jets
Finite-dimensional coordinate bounds control the operator norm of a multilinear derivative. This converts intrinsic cube balls into full-jet estimates needed by quantitative extension constructions.
In dimension d, for derivative order m and exponent s, there is a positive constant C such that every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the closed cube has within-cube Fréchet derivatives of every order at most m with operator norm at most C·L on the cube, and its order-m within-cube Fréchet derivative is s-Hölder on the cube with coefficient C·L. The constant does not depend on the response or the radius.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
exists_coord_multilinear_norm_constanttheorem — In dimension d and through order m, there is a positive constant C such that every continuous j-linear map T on coordinate space with j ≤ m whose values on all tuples of standard basis vectors are bounded in absolute value by B ≥ 0 has operator norm at most C·B.hypothesesd m :ℕProof (Lean source)
theorem exists_coord_multilinear_norm_constant (d m : ℕ) : ∃ C : ℝ, 0 < C ∧ ∀ j ≤ m, ∀ T : ContinuousMultilinearMap ℝ (fun _ : Fin j => Fin d → ℝ) ℝ, ∀ B : ℝ, 0 ≤ B → (∀ f : Fin j → Fin d, |T (fun k => single (f k) (1 : ℝ))| ≤ B) → ‖T‖ ≤ C * B := by classical refine ⟨((d + 1 : ℕ) : ℝ) ^ m, by positivity, ?_⟩ intro j hj T B hB hcoord apply ContinuousMultilinearMap.opNorm_le_bound (by positivity) intro v have hsum (k : Fin j) : (∑ i : Fin d, (v k i) • single i (1 : ℝ)) = v k := by ext i simp [Pi.single_apply] have hterm (f : Fin j → Fin d) : ‖T (fun k => (v k (f k)) • single (f k) (1 : ℝ))‖ ≤ B * ∏ k, ‖v k‖ := by rw [T.map_smul_univ, norm_smul, Real.norm_eq_abs, Finset.abs_prod] have hc : ‖T (fun k => single (f k) (1 : ℝ))‖ ≤ B := by simpa [Real.norm_eq_abs] using hcoord f have hp : (∏ k, |v k (f k)|) ≤ ∏ k, ‖v k‖ := by apply Finset.prod_le_prod (fun k hk => abs_nonneg _) intro k hk simpa [Real.norm_eq_abs] using norm_le_pi_norm (v k) (f k) calc (∏ k, |v k (f k)|) * ‖T (fun k => single (f k) (1 : ℝ))‖ ≤ (∏ k, |v k (f k)|) * B := by gcongr _ = B * (∏ k, |v k (f k)|) := by ring _ ≤ B * (∏ k, ‖v k‖) := by gcongr have hcard : ((card (Fin j → Fin d) : ℕ) : ℝ) ≤ ((d + 1 : ℕ) : ℝ) ^ m := by simp only [Fintype.card_fun, Fintype.card_fin] exact_mod_cast (calc d ^ j ≤ (d + 1) ^ j := Nat.pow_le_pow_left (by omega) j _ ≤ (d + 1) ^ m := Nat.pow_le_pow_right (by omega) hj) calc ‖T v‖ = ‖∑ f : Fin j → Fin d, T (fun k => (v k (f k)) • single (f k) (1 : ℝ))‖ := by congr 1 conv_lhs => rw [← funext hsum] exact T.map_sum (fun k i => (v k i) • single i (1 : ℝ)) _ ≤ ∑ f : Fin j → Fin d, ‖T (fun k => (v k (f k)) • single (f k) (1 : ℝ))‖ := norm_sum_le _ _ _ ≤ ∑ _f : Fin j → Fin d, B * ∏ k, ‖v k‖ := Finset.sum_le_sum (fun f _ => hterm f) _ = ((card (Fin j → Fin d) : ℕ) : ℝ) * (B * ∏ k, ‖v k‖) := by simp _ ≤ (((d + 1 : ℕ) : ℝ) ^ m) * (B * ∏ k, ‖v k‖) := by gcongr _ = (((d + 1 : ℕ) : ℝ) ^ m * B) * ∏ k, ‖v k‖ := by ring
ProductJetDiagonal 1 core · 0 supporting The product rule for iterated Fréchet derivatives is first isolated on tuples whose directions are all equal. ★ iteratedFDerivWithin_mul_diagonal
Diagonal Leibniz formula for within-set jets
The product rule for iterated Fréchet derivatives is first isolated on tuples
whose directions are all equal. This scalar identity is the analytic input to
the symmetric multilinear pairing formula in ProductJetDifference.
If a set S has unique within-set derivatives, two functions v and w are m times continuously differentiable within S, and x lies in S, then the order-m within-S derivative of the product v·w at x, evaluated with the same direction z in every slot, equals the sum over i ≤ m of (m choose i) times the order-i within-S derivative of v times the order-(m − i) within-S derivative of w, each evaluated with z in every slot.
Formal statement
Proof (Lean source)
ProductJetDifference 1 core · 1 supporting This module constructs the fixed contractive pairings in the within-set product rule and uses them to bound differences of product jets. ★ norm_iteratedFDerivWithin_mul_sub_le
Product-jet pairing and difference estimates
This module constructs the fixed contractive pairings in the within-set product rule and uses them to bound differences of product jets. It is the algebraic part of Hölder control for smooth cutoff extensions.
If a set S has unique within-set derivatives, two functions v and w are m times continuously differentiable within S, and two points x and y lie in S and in the closure of the interior of S, then the order-m within-S derivatives of v·w at x and at y differ in norm by at most the sum over i ≤ m of (m choose i) times ‖Dⁱv(x) − Dⁱv(y)‖·‖D^(m−i)w(x)‖ + ‖Dⁱv(y)‖·‖D^(m−i)w(x) − D^(m−i)w(y)‖, where D^k denotes the order-k within-S derivative.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
exists_contracting_productJet_pairingstheorem — In dimension d and for order m, there are continuous bilinear pairings B_i, one for each i ≤ m, taking an order-i and an order-(m − i) multilinear map to an order-m multilinear map, each of operator norm at most one, such that for every set S with unique within-set derivatives, all functions v and w that are m times continuously differentiable within S, and every point x of S lying in the closure of the interior of S, the order-m within-S derivative of v·w at x equals the sum over i ≤ m of (m choose i) times B_i applied to the order-i within-S derivative of v and the order-(m − i) within-S derivative of w at x. The pairings do not depend on the functions, the set, or the point.hypothesesd m :ℕconclusion∃ B : ∀ i : ℕifandandL[ℝ] (ContinuousMultilinearMap ℝ (fun _ : Fin m => Fin d → ℝ) ℝ), (∀ i ∈ range (m + 1), ‖B i‖ ≤ 1) ∧andContDiffOn ℝ m v SandContDiffOn ℝ m w Sandx ∈ StheniteratedFDerivWithin ℝ m (fun z => v z * w z) S x= ∑ i ∈ range (m + 1), (m.choose i : ℝ) • B i (iteratedFDerivWithin ℝ i v S x) (iteratedFDerivWithin ℝ (m - i) w S x)Proof (Lean source)
theorem exists_contracting_productJet_pairings (d m : ℕ) : ∃ B : ∀ i : ℕ, (ContinuousMultilinearMap ℝ (fun _ : Fin i => Fin d → ℝ) ℝ) →L[ℝ] (ContinuousMultilinearMap ℝ (fun _ : Fin (m - i) => Fin d → ℝ) ℝ) →L[ℝ] (ContinuousMultilinearMap ℝ (fun _ : Fin m => Fin d → ℝ) ℝ), (∀ i ∈ range (m + 1), ‖B i‖ ≤ 1) ∧ ∀ (S : Set (Fin d → ℝ)) (v w : (Fin d → ℝ) → ℝ) (x : Fin d → ℝ), UniqueDiffOn ℝ S → ContDiffOn ℝ m v S → ContDiffOn ℝ m w S → x ∈ S → x ∈ closure (interior S) → iteratedFDerivWithin ℝ m (fun z => v z * w z) S x = ∑ i ∈ range (m + 1), (m.choose i : ℝ) • B i (iteratedFDerivWithin ℝ i v S x) (iteratedFDerivWithin ℝ (m - i) w S x) := by classical let B : ∀ i : ℕ, (ContinuousMultilinearMap ℝ (fun _ : Fin i => Fin d → ℝ) ℝ) →L[ℝ] (ContinuousMultilinearMap ℝ (fun _ : Fin (m - i) => Fin d → ℝ) ℝ) →L[ℝ] (ContinuousMultilinearMap ℝ (fun _ : Fin m => Fin d → ℝ) ℝ) := fun i => if hi : i ≤ m then choose (exists_contracting_symmetric_productJet_pairing d m i hi) else 0 have hBnorm (i : ℕ) (hi : i ≤ m) : ‖B i‖ ≤ 1 := by simpa only [B, dif_pos hi] using (Classical.choose_spec (exists_contracting_symmetric_productJet_pairing d m i hi)).1 have hBdiag (i : ℕ) (hi : i ≤ m) (a : ContinuousMultilinearMap ℝ (fun _ : Fin i => Fin d → ℝ) ℝ) (b : ContinuousMultilinearMap ℝ (fun _ : Fin (m - i) => Fin d → ℝ) ℝ) (z : Fin d → ℝ) : B i a b (fun _ => z) = a (fun _ => z) * b (fun _ => z) := by simpa only [B, dif_pos hi] using (Classical.choose_spec (exists_contracting_symmetric_productJet_pairing d m i hi)).2.1 a b z have hBperm (i : ℕ) (hi : i ≤ m) (a : ContinuousMultilinearMap ℝ (fun _ : Fin i => Fin d → ℝ) ℝ) (b : ContinuousMultilinearMap ℝ (fun _ : Fin (m - i) => Fin d → ℝ) ℝ) (σ : Perm (Fin m)) (z : Fin m → Fin d → ℝ) : B i a b (z ∘ σ) = B i a b z := by simpa only [B, dif_pos hi] using (Classical.choose_spec (exists_contracting_symmetric_productJet_pairing d m i hi)).2.2 a b σ z refine ⟨B, ?_, ?_⟩ · intro i hi exact hBnorm i (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)) · intro S v w x huniq hv hw hx hxcl apply continuousMultilinearMap_eq_of_symmetric_diagonal · intro σ z exact iteratedFDerivWithin_comp_perm_of_contDiffOn huniq (hv.mul hw) hx hxcl σ z · intro σ z simp only [sum_apply, smul_apply] apply Finset.sum_congr rfl intro i hi rw [hBperm i (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi))] · intro z rw [iteratedFDerivWithin_mul_diagonal huniq hv hw hx z] simp only [sum_apply, smul_apply, smul_eq_mul] apply Finset.sum_congr rfl intro i hi rw [hBdiag i (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi))]
ProductJetDifferenceAlgebra 1 core · 0 supporting This finite-sum estimate is the algebraic step in comparing two evaluations of a Leibniz expansion. ★ norm_bilinear_sum_sub_le
Bilinear sum differences
This finite-sum estimate is the algebraic step in comparing two evaluations of a Leibniz expansion. It applies to any contractive continuous bilinear map, including multiplication and the multilinear contractions in product jets.
If a continuous bilinear map B has operator norm at most one and the coefficients c_i are nonnegative on a finite index set t, then the norm of the difference between Σ_{i ∈ t} c_i·B(a_i, b_i) and Σ_{i ∈ t} c_i·B(a'_i, b'_i) is at most Σ_{i ∈ t} c_i·(‖a_i − a'_i‖·‖b_i‖ + ‖a'_i‖·‖b_i − b'_i‖).
Formal statement
Proof (Lean source)
ProductJetDifferenceFirstOrder 1 core · 0 supporting The first-order case isolates the two-point bilinear estimate needed in the induction for higher within-set product jets. ★ norm_iteratedFDerivWithin_mul_sub_le_one
First-order difference estimate for a product jet
The first-order case isolates the two-point bilinear estimate needed in the induction for higher within-set product jets.
If a set S has unique within-set derivatives, two functions v and w are continuously differentiable within S, and x and y lie in S, then the first within-S derivatives of the product v·w at x and at y differ in norm by at most ‖v(x) − v(y)‖·‖Dw(x)‖ + ‖v(y)‖·‖Dw(x) − Dw(y)‖ + ‖Dv(x) − Dv(y)‖·‖w(x)‖ + ‖Dv(y)‖·‖w(x) − w(y)‖, where D denotes the first within-S derivative; these are the four terms obtained by changing one factor at a time in the product rule.
Formal statement
Proof (Lean source)
ProductJetPairingAlgebra 1 core · 0 supporting A pair of multilinear maps can be combined into a multilinear map by averaging over the ways to assign argument slots to the two factors. ★ exists_contracting_symmetric_productJet_pairing
Algebraic pairings for product jets
A pair of multilinear maps can be combined into a multilinear map by averaging over the ways to assign argument slots to the two factors. This module isolates the algebraic construction from the derivative product rule.
If i ≤ m, then there is a continuous bilinear pairing B taking an order-i and an order-(m − i) scalar multilinear map on d-dimensional coordinate space to an order-m multilinear map, with operator norm at most one, whose value B(a, b) on m copies of a vector z is a(z, …, z)·b(z, …, z), and whose output is invariant under every permutation of its m arguments.
Formal statement
Proof (Lean source)
ProductJetPolarization 1 core · 0 supporting This algebraic fact is the polarization step in the exact product-jet formula. ★ continuousMultilinearMap_eq_of_symmetric_diagonal
Symmetric multilinear maps are determined by their diagonal
This algebraic fact is the polarization step in the exact product-jet formula. It is stated for scalar continuous multilinear maps on a finite-dimensional real space, but does not use differentiability.
If two continuous real-valued m-linear maps A and B on d-dimensional coordinate space are symmetric under permutations of their arguments and agree whenever every argument is the same vector, then A = B.
Formal statement
Proof (Lean source)
ProductJetSlotPairing 1 core · 0 supporting The first i argument slots of an order-m multilinear map can feed one factor, and the remaining slots can feed a second factor. ★ exists_contracting_productJet_slot_pairing
A fixed-slot pairing of multilinear jets
The first i argument slots of an order-m multilinear map can feed one
factor, and the remaining slots can feed a second factor. The resulting
bilinear operation is contractive and has the expected value on diagonal
tuples. Symmetrizing this operation is handled in the next module.
If i ≤ m, then there is a continuous bilinear pairing B taking an order-i and an order-(m − i) scalar multilinear map on d-dimensional coordinate space to an order-m multilinear map, with operator norm at most one, whose value B(a, b) on m copies of a vector z is a(z, …, z)·b(z, …, z).
Formal statement
Proof (Lean source)
ProductJetSymmetry 1 core · 0 supporting At points approached by the interior of a uniquely differentiable set, iterated within-set derivatives of a C^m function are symmetric in their direction slots. ★ iteratedFDerivWithin_comp_perm_of_contDiffOn
Symmetry of finite-order within-set jets
At points approached by the interior of a uniquely differentiable set,
iterated within-set derivatives of a C^m function are symmetric in their
direction slots. This recovers the product-jet formula from its diagonal form.
If a set S in d-dimensional coordinate space has unique within-set derivatives, a scalar function f is m times continuously differentiable within S, and a point x lies in S and in the closure of the interior of S, then for every permutation σ of the m argument slots and every choice of m directions v the order-m within-S derivative of f at x takes the same value on the permuted directions as on the original ones.
Formal statement
Proof (Lean source)
RadialBase 2 core · 5 supporting Local constancy near the projection kernel removes the norm singularity. ★ radialPlateau_contDiff
Exact radial plateau on projected Euclidean norms
Local constancy near the projection kernel removes the norm singularity. Uniform first and second jet bounds are obtained from the compactly supported codomain profile, with one and two factors of the projection operator norm. This module is independent of coordinate product profiles and bandwidth scaling.
For a continuous linear map P into an inner product space, the radial plateau at a point x is the scalar plateau evaluated at the norm of P x.
Definition (Lean source)
For a continuous linear map P into a finite-dimensional inner product space, the radial plateau is twice continuously differentiable on the whole space, including at points that P sends to zero.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
radialPlateau_boundstheorem — For a coordinate map at a point, the radial plateau lies between zero and one.hypothesesE :sharedType u_1F :sharedType u_2P :E →L[ℝ] Fx :EProof (Lean source)
theorem radialPlateau_bounds (P : E →L[ℝ] F) (x : E) : 0 ≤ radialPlateau P x ∧ radialPlateau P x ≤ 1 := by exact plateau_bounds ‖P x‖ -
radialPlateau_eventually_onetheorem — The radial plateau is locally constant one near a point whose projected norm is less than one for the projection.hypothesesE :sharedType u_1F :sharedType u_2P :E →L[ℝ] Fx :Ehx :‖P x‖ < 1conclusion∀ᶠ y in nhds x, radialPlateau P y = 1Proof (Lean source)
theorem radialPlateau_eventually_one (P : E →L[ℝ] F) (x : E) (hx : ‖P x‖ < 1) : ∀ᶠ y in nhds x, radialPlateau P y = 1 := by have h := (P.continuous.norm.continuousAt).eventually (Iio_mem_nhds hx) filter_upwards [h] with y hy exact plateau_eq_one _ hy.le -
radialPlateau_base_hasCompactSupporttheorem — The norm plateau on the finite-dimensional codomain has compact support in the fixed inner-product space.Proof (Lean source)
theorem radialPlateau_base_hasCompactSupport : HasCompactSupport (fun x : F => plateau ‖x‖) := by apply HasCompactSupport.intro (K := closedBall (0 : F) 2) (isCompact_closedBall _ _) intro x hx apply plateau_eq_zero have hr : ¬ ‖x‖ ≤ 2 := by simpa using hx exact (lt_of_not_ge hr).le -
radialPlateau_jets_zerotheorem — At a point whose projected radius is at least two under the projection, the value and both ambient jets vanish.hypothesesE :sharedType u_1F :sharedType u_2P :E →L[ℝ] Fx :Ehx :2 ≤ ‖P x‖conclusionconclusion 1radialPlateau P x = 0conclusion 2fderiv ℝ (radialPlateau P) x = 0conclusion 3Proof (Lean source)
theorem radialPlateau_jets_zero (P : E →L[ℝ] F) (x : E) (hx : 2 ≤ ‖P x‖) : radialPlateau P x = 0 ∧ fderiv ℝ (radialPlateau P) x = 0 ∧ fderiv ℝ (fderiv ℝ (radialPlateau P)) x = 0 := by have hext (y : E) (hy : 2 < ‖P y‖) : radialPlateau P y = 0 ∧ fderiv ℝ (radialPlateau P) y = 0 ∧ fderiv ℝ (fderiv ℝ (radialPlateau P)) y = 0 := by apply jets_zero_of_eventually_zero have h := P.continuous.norm.continuousAt.eventually (Ioi_mem_nhds hy) filter_upwards [h] with z hz exact plateau_eq_zero _ hz.le have hd : ContDiff ℝ 1 (fderiv ℝ (radialPlateau P)) := (contDiff_succ_iff_fderiv.mp (radialPlateau_contDiff P)).2.2 have hc : Continuous (fun t : ℝ => t • x) := by fun_prop have hs : IsClosed {t : ℝ | fderiv ℝ (radialPlateau P) (t • x) = 0 ∧ fderiv ℝ (fderiv ℝ (radialPlateau P)) (t • x) = 0} := (isClosed_eq (hd.continuous.comp hc) continuous_const).inter (isClosed_eq ((hd.continuous_fderiv (by norm_num)).comp hc) continuous_const) have hsub : Ioi (1 : ℝ) ⊆ {t : ℝ | fderiv ℝ (radialPlateau P) (t • x) = 0 ∧ fderiv ℝ (fderiv ℝ (radialPlateau P)) (t • x) = 0} := by intro t ht change 1 < t at ht apply (hext (t • x) ?_).2 rw [map_smul, norm_smul, Real.norm_eq_abs, abs_of_pos (by linarith : 0 < t)] nlinarith have hmem : (1 : ℝ) ∈ closure (Ioi (1 : ℝ)) := by rw [closure_Ioi] change (1 : ℝ) ≤ 1 exact le_rfl have hj := (closure_minimal hsub hs) hmem change fderiv ℝ (radialPlateau P) ((1 : ℝ) • x) = 0 ∧ fderiv ℝ (fderiv ℝ (radialPlateau P)) ((1 : ℝ) • x) = 0 at hj refine ⟨plateau_eq_zero ‖P x‖ hx, ?_⟩ simpa only [one_smul] using hj -
radialPlateau_uniform_jetBoundstheorem — A finite constant bounds the radial first and second jets by the first and second powers of the projection norm, and values by one, uniformly over all coordinate maps between the fixed spaces.hypothesesE :sharedType u_1F :sharedType u_2conclusion∃ C : ℝ,1 ≤ Cconclusion 1P :E →L[ℝ] Fx :E|radialPlateau P x| ≤ 1‖fderiv ℝ (radialPlateau P) x‖ ≤ C * ‖P‖‖fderiv ℝ (fderiv ℝ (radialPlateau P)) x‖ ≤ C * ‖P‖ ^ 2Proof (Lean source)
-- `ContinuousLinearMap.iteratedFDeriv_comp_right` and the norm bound for -- `ContinuousMultilinearMap.compContinuousLinearMap` give the codomain jet -- bound multiplied by ‖P‖^j. Relate j=1,2 to nested ambient fderiv via -- `norm_iteratedFDeriv_fderiv` and the order-one norm identity. theorem radialPlateau_uniform_jetBounds : ∃ C : ℝ, 1 ≤ C ∧ ∀ (P : E →L[ℝ] F) (x : E), |radialPlateau P x| ≤ 1 ∧ ‖fderiv ℝ (radialPlateau P) x‖ ≤ C * ‖P‖ ∧ ‖fderiv ℝ (fderiv ℝ (radialPlateau P)) x‖ ≤ C * ‖P‖ ^ 2 := by let b : F → ℝ := fun y => plateau ‖y‖ have hb : ContDiff ℝ 2 b := by exact radialPlateau_contDiff (id ℝ F) obtain ⟨C, hC, hB⟩ := exists_jetBounds_of_compactSupport hb radialPlateau_base_hasCompactSupport refine ⟨C, hC, ?_⟩ intro P x have hbound (j : ℕ) (hj : j ≤ 2) (hjet : ‖iteratedFDeriv ℝ j b (P x)‖ ≤ C) : ‖iteratedFDeriv ℝ j (radialPlateau P) x‖ ≤ C * ‖P‖ ^ j := by change ‖iteratedFDeriv ℝ j (b ∘ P) x‖ ≤ _ rw [P.iteratedFDeriv_comp_right hb x (by exact_mod_cast hj)] calc _ ≤ ‖iteratedFDeriv ℝ j b (P x)‖ * ∏ _ : Fin j, ‖P‖ := ContinuousMultilinearMap.norm_compContinuousLinearMap_le _ _ _ = ‖iteratedFDeriv ℝ j b (P x)‖ * ‖P‖ ^ j := by simp _ ≤ C * ‖P‖ ^ j := mul_le_mul_of_nonneg_right hjet (by positivity) refine ⟨?_, ?_, ?_⟩ · rw [abs_of_nonneg (radialPlateau_bounds P x).1] exact (radialPlateau_bounds P x).2 · simpa only [norm_iteratedFDeriv_one, pow_one] using hbound 1 (by norm_num) (by simpa only [norm_iteratedFDeriv_one] using hB.first (P x)) · have hn (f : E → ℝ) : ‖iteratedFDeriv ℝ 2 f x‖ = ‖fderiv ℝ (fderiv ℝ f) x‖ := by rw [← norm_iteratedFDeriv_fderiv (n := 1), norm_iteratedFDeriv_one] have hnF : ‖iteratedFDeriv ℝ 2 b (P x)‖ ≤ C := by rw [← norm_iteratedFDeriv_fderiv (n := 1), norm_iteratedFDeriv_one] exact hB.second (P x) simpa only [hn] using hbound 2 le_rfl hnF
RectangularAffine 1 core · 0 supporting Coordinatewise affine changes of variables identify any two nondegenerate finite boxes. ★ exists_rectAffine_holder_constant
Quantitative affine transport between closed rectangular boxes
Coordinatewise affine changes of variables identify any two nondegenerate finite boxes. This module records the uniform intrinsic Hölder norm estimate needed to reuse a normalized one-face reflection on successive boxes.
If the source box and the target box both have positive side lengths, then for derivative order m and exponent s there is a positive constant C such that whenever a response u lies in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the target box, its pullback along the coordinatewise affine map lies in the intrinsic Hölder ball of radius C·L on the source box. The constant depends only on the boxes, m and s; all jets are taken within their own box, so the estimate does not depend on the ambient representative.
Formal statement
Proof (Lean source)
RectangularAffineJets 1 core · 2 supporting These identities isolate the chain rule needed to transport an intrinsic Hölder ball between fixed nondegenerate boxes. ★ coordJetOn_rectAffine
Intrinsic jets under a rectangular affine change of variables
These identities isolate the chain rule needed to transport an intrinsic Hölder ball between fixed nondegenerate boxes. The derivatives are taken within the corresponding boxes, including at their faces.
If the source box with corners lo, hi and the target box with corners lo', hi' both have positive side lengths, then at any point x of the source box, including boundary points, each order-j intrinsic coordinate jet on the source box of the pullback of a response u along the coordinatewise affine map, in directions f(0), …, f(j − 1), equals the product over k of the scale factors (hi'_{f(k)} − lo'_{f(k)})/(hi_{f(k)} − lo_{f(k)}) times the corresponding intrinsic jet of u on the target box at the image of x.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
exists_rectAffine_linearEquivtheorem — If the source box with corners lo, hi and the target box with corners lo', hi' both have positive side lengths, then there is a continuous linear equivalence e that multiplies coordinate i by (hi'_i − lo'_i)/(hi_i − lo_i), and the coordinatewise affine map between the boxes equals e followed by translation by the vector with i-th coordinate lo'_i − (hi'_i − lo'_i)/(hi_i − lo_i)·lo_i.hypothesesconclusionconclusion 1x i :e x i = (hi' i - lo' i) / (hi i - lo i) * x iconclusion 2x :rectAffine lo hi lo' hi' x= e x + (fun i => lo' i - (hi' i - lo' i) / (hi i - lo i) * lo i)Proof (Lean source)
theorem exists_rectAffine_linearEquiv {d : ℕ} (lo hi lo' hi' : Fin d → ℝ) (hsource : ∀ i, lo i < hi i) (htarget : ∀ i, lo' i < hi' i) : ∃ e : (Fin d → ℝ) ≃L[ℝ] (Fin d → ℝ), (∀ x i, e x i = (hi' i - lo' i) / (hi i - lo i) * x i) ∧ (∀ x, rectAffine lo hi lo' hi' x = e x + (fun i => lo' i - (hi' i - lo' i) / (hi i - lo i) * lo i)) := by /- Build the diagonal linear equivalence from the positive scalars and their inverses, with continuity from finite-dimensionality. The final identity follows by coordinate extensionality and `ring`. -/ let a : Fin d → ℝ := fun i => (hi' i - lo' i) / (hi i - lo i) have ha (i : Fin d) : a i ≠ 0 := ne_of_gt (div_pos (sub_pos.mpr (htarget i)) (sub_pos.mpr (hsource i))) let e : (Fin d → ℝ) ≃L[ℝ] (Fin d → ℝ) := ContinuousLinearEquiv.piCongrRight (fun i => (LinearEquiv.smulOfNeZero ℝ ℝ (a i) (ha i)).toContinuousLinearEquiv) refine ⟨e, ?_, ?_⟩ · intro x i simp [e, a] · intro x funext i simp only [Pi.add_apply, rectAffine, e, ContinuousLinearEquiv.piCongrRight_apply, LinearEquiv.coe_toContinuousLinearEquiv', LinearEquiv.smulOfNeZero_apply, smul_eq_mul] dsimp [a] ring -
contDiffOn_rectAffinetheorem — If the source box and the target box both have positive side lengths and a response u is m times continuously differentiable within the target box, then its pullback along the coordinatewise affine map is m times continuously differentiable within the source box.hypothesesd m :ℕlo hi lo' hi' :Fin d → ℝhsource :∀ i, lo i < hi ihtarget :∀ i, lo' i < hi' iu :(Fin d → ℝ) → ℝhu :ContDiffOn ℝ m u (rectBox lo' hi')conclusionProof (Lean source)
theorem contDiffOn_rectAffine {d m : ℕ} (lo hi lo' hi' : Fin d → ℝ) (hsource : ∀ i, lo i < hi i) (htarget : ∀ i, lo' i < hi' i) {u : (Fin d → ℝ) → ℝ} (hu : ContDiffOn ℝ m u (rectBox lo' hi')) : ContDiffOn ℝ m (fun x => u (rectAffine lo hi lo' hi' x)) (rectBox lo hi) := by obtain ⟨e, _, he⟩ := exists_rectAffine_linearEquiv lo hi lo' hi' hsource htarget let c : Fin d → ℝ := fun i => lo' i - (hi' i - lo' i) / (hi i - lo i) * lo i have hmap : ContDiff ℝ m (fun x : Fin d → ℝ => e x + c) := e.contDiff.add contDiff_const have hcomp : ContDiffOn ℝ m (u ∘ fun x : Fin d → ℝ => e x + c) (rectBox lo hi) := hu.comp hmap.contDiffOn (by intro x hx change e x + c ∈ rectBox lo' hi' have hx' : rectAffine lo hi lo' hi' x ∈ rectBox lo' hi' := by exact (Set.ext_iff.mp (rectAffine_preimage_rectBox lo hi lo' hi' hsource htarget) x).2 hx simpa only [he] using hx') convert hcomp using 1 funext x simp only [Function.comp_def, he] rfl
RectangularCutoff 1 core · 0 supporting An intrinsic Hölder ball on a closed box containing the normalized cube in its interior admits a globally controlled representative agreeing on the cube. ★ exists_global_holder_cutoff_of_rectBox
Controlled cutoff from a rectangular neighborhood
An intrinsic Hölder ball on a closed box containing the normalized cube in its interior admits a globally controlled representative agreeing on the cube.
In dimension d, for derivative order m and a Hölder exponent s with 0 < s and s ≤ 1, if the box with corners lo, hi strictly contains the normalized cube in every coordinate, then there is a positive constant C such that every response v in the intrinsic Hölder ball of radius R ≥ 0 on the box has a global representative U that agrees with v on the cube, is m times continuously differentiable, has ambient derivatives of every order at most m bounded in operator norm by C·R everywhere, and whose order-m derivative is globally s-Hölder with coefficient C·R.
Formal statement
Proof (Lean source)
RectangularCutoffBoundaryPoint 1 core · 0 supporting For a point in a closed box and a point outside it, moving one coordinate of the first point to the intervening face reaches the boundary without traveling farther than the original pair's distance. ★ exists_rectBox_boundary_point_le
A nearby rectangular boundary point
For a point in a closed box and a point outside it, moving one coordinate of the first point to the intervening face reaches the boundary without traveling farther than the original pair's distance.
If x lies in a closed coordinate box and y lies outside it, then there is a boundary point z of the box (in the closed box but not in the open box) whose distance to x is at most the distance from x to y.
Formal statement
Proof (Lean source)
RectangularCutoffBoundaryTransfer 1 core · 0 supporting A continuous map satisfying a Hölder estimate on the open rectangular box satisfies the same estimate on its closed box. ★ holder_modulus_on_rectBox_of_openBox
Hölder bounds up to rectangular faces
A continuous map satisfying a Hölder estimate on the open rectangular box satisfies the same estimate on its closed box.
If a box has positive side lengths, a map J into a normed group is continuous, s > 0, and ‖J(x) − J(y)‖ ≤ C·‖x − y‖^s for all points x, y of the open box, then the same bound holds for all points x, y of the closed box.
Formal statement
Proof (Lean source)
RectangularCutoffExteriorJets 1 core · 0 supporting When the cutoff support lies strictly inside the open box, the zero extension vanishes near every point outside that open box. ★ rectCutoffExtension_iteratedFDeriv_eq_zero_of_not_mem
Cutoff jets outside a rectangular box
When the cutoff support lies strictly inside the open box, the zero extension vanishes near every point outside that open box. All ambient jets vanish there.
If the closed support of a cutoff χ lies inside the open box and a point x lies outside the open box, then for every order j the ambient order-j derivative at x of the zero extension of χ·v from the closed box vanishes.
Formal statement
Proof (Lean source)
RectangularCutoffInteriorModulus 1 core · 0 supporting This module isolates the product estimate at pairs of points strictly inside the cutoff box. ★ exists_rectCutoffExtension_interior_modulus_constant
Interior top jet modulus for a cutoff response
This module isolates the product estimate at pairs of points strictly inside the cutoff box. A separate closure argument transfers it to the box faces.
If 0 < s and s ≤ 1, the box with corners lo, hi strictly contains the normalized cube, χ is smooth with closed support inside the open box, and its ambient derivatives of every order up to m + 1 are bounded in operator norm by B ≥ 0, then there is a positive constant C such that for every response v in the intrinsic Hölder ball of order m, exponent s and radius R ≥ 0 on the closed box, the order-m ambient derivatives of the zero extension of χ·v at any two points x, y of the open box differ in norm by at most C·R·‖x − y‖^s.
Formal statement
Proof (Lean source)
RectangularCutoffJetBounds 1 core · 0 supporting Coordinatewise intrinsic bounds on a closed box control all ambient jets of the zero extension obtained from a fixed smooth cutoff. ★ exists_rectCutoffExtension_jet_constant
Uniform jet bounds for a localized rectangular response
Coordinatewise intrinsic bounds on a closed box control all ambient jets of the zero extension obtained from a fixed smooth cutoff.
If the box with corners lo, hi strictly contains the normalized cube, χ is smooth with closed support inside the open box, and its ambient derivatives of every order up to m + 1 are bounded in operator norm by B ≥ 0, then there is a positive constant C such that for every response v in the intrinsic Hölder ball of order m, exponent s and radius R ≥ 0 on the closed box, every ambient derivative of order at most m of the zero extension of χ·v from the box has operator norm at most C·R everywhere.
Formal statement
Proof (Lean source)
RectangularCutoffLocalJets 1 core · 0 supporting Within-box derivative bounds for a response and ambient derivative bounds for a fixed smooth cutoff control the product jets at interior box points. ★ exists_rectCutoffExtension_local_jet_constant
Jet bounds inside the support box of a cutoff extension
Within-box derivative bounds for a response and ambient derivative bounds for a fixed smooth cutoff control the product jets at interior box points. This is the local estimate used before extending the bound by zero off the cutoff support.
If the box with corners lo, hi strictly contains the normalized cube, χ is smooth, and its ambient derivatives of every order up to m + 1 are bounded in operator norm by B ≥ 0, then there is a positive constant C such that for every response v in the intrinsic Hölder ball of order m, exponent s and radius R ≥ 0 on the closed box, every ambient derivative of order at most m of the zero extension of χ·v from the box has operator norm at most C·R at each point of the open box. The constant does not depend on the response or its radius.
Formal statement
Proof (Lean source)
RectangularCutoffLocalModulus 1 core · 0 supporting Inside a closed rectangular box, bounded jets of a smooth cutoff and the intrinsic Hölder jets of a response give a uniform top-order modulus for the localized response, including boundary traces. ★ exists_rectCutoffExtension_box_modulus_constant
Top jet modulus on the cutoff box
Inside a closed rectangular box, bounded jets of a smooth cutoff and the intrinsic Hölder jets of a response give a uniform top-order modulus for the localized response, including boundary traces.
If 0 < s and s ≤ 1, the box with corners lo, hi strictly contains the normalized cube, χ is smooth with closed support inside the open box, and its ambient derivatives of every order up to m + 1 are bounded in operator norm by B ≥ 0, then there is a positive constant C such that for every response v in the intrinsic Hölder ball of order m, exponent s and radius R ≥ 0 on the closed box, the order-m ambient derivatives of the zero extension of χ·v at any two points x, y of the closed box differ in norm by at most C·R·‖x − y‖^s.
Formal statement
Proof (Lean source)
RectangularCutoffModulus 1 core · 0 supporting The zero extension of a fixed smooth cutoff times an intrinsic box response retains the top-order Hölder modulus with a uniform multiplicative factor. ★ exists_rectCutoffExtension_modulus_constant
Top-order modulus for a localized rectangular response
The zero extension of a fixed smooth cutoff times an intrinsic box response retains the top-order Hölder modulus with a uniform multiplicative factor.
If 0 < s and s ≤ 1, the box with corners lo, hi strictly contains the normalized cube, χ is smooth with closed support inside the open box, and its ambient derivatives of every order up to m + 1 are bounded in operator norm by B ≥ 0, then there is a positive constant C such that for every response v in the intrinsic Hölder ball of order m, exponent s and radius R ≥ 0 on the closed box, the order-m ambient derivatives of the zero extension of χ·v at any two points x, y of the whole space differ in norm by at most C·R·‖x − y‖^s.
Formal statement
Proof (Lean source)
RectangularFaceReflection 1 core · 0 supporting Affine transport carries the normalized one-face reflection to any nondegenerate coordinate box. ★ exists_rectLeftFaceReflection_holder_constant
Controlled reflection across a face of a rectangular box
Affine transport carries the normalized one-face reflection to any nondegenerate coordinate box. The first step extends across a lower face; upper faces and repeated reflection can be built from this result.
If 0 < s and the box with corners lo, hi has positive side lengths, then for derivative order m and coordinate i there is a positive constant C such that every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the box agrees on the box with a response in the intrinsic Hölder ball of radius C·L on the box's left collar in coordinate i. The constant depends only on the box, m, s and i.
Formal statement
Proof (Lean source)
RectangularNegation 1 core · 2 supporting Negating every coordinate exchanges the lower and upper faces of a closed box. ★ holderBallOn_rectBox_neg
Intrinsic rectangular jets under coordinate negation
Negating every coordinate exchanges the lower and upper faces of a closed box. The within-box jets transform with the usual order-dependent sign, which lets the lower-face reflection theorem handle upper faces as well.
If the box with corners lo, hi has positive side lengths and a response u lies in the intrinsic Hölder ball of order m, exponent s and radius L on the box, then the response x ↦ u(−x) lies in the intrinsic Hölder ball with the same order, exponent and radius on the negated box. All bounds use within-box jets, so the claim applies to any ambient representative of the original response.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
mem_rectBox_neg_ifftheorem — A point x lies in the coordinatewise negated box, with corners −hi and −lo, exactly when −x lies in the original box with corners lo and hi.hypothesesProof (Lean source)
theorem mem_rectBox_neg_iff {d : ℕ} (lo hi : Fin d → ℝ) (x : Fin d → ℝ) : x ∈ rectBox (fun i => -hi i) (fun i => -lo i) ↔ -x ∈ rectBox lo hi := by constructor <;> intro hx i · have h := hx i change -hi i ≤ x i ∧ x i ≤ -lo i at h change lo i ≤ -x i ∧ -x i ≤ hi i constructor <;> linarith · have h := hx i change lo i ≤ -x i ∧ -x i ≤ hi i at h change -hi i ≤ x i ∧ x i ≤ -lo i constructor <;> linarith -
coordJetOn_rectBox_negtheorem — If the box with corners lo, hi has positive side lengths, then at every point x of the negated box the order-j intrinsic coordinate jet on the negated box of the response z ↦ u(−z) equals (−1)^j times the corresponding intrinsic jet of u on the original box at −x, including on the faces of the box.hypothesesd j :ℕlo hi :Fin d → ℝhbox :∀ i, lo i < hi iu :(Fin d → ℝ) → ℝx :Fin d → ℝhx :x ∈ rectBox (fun i => -hi i) (fun i => -lo i)conclusioncoordJetOn (rectBox (fun i => -hi i) (fun i => -lo i)) j (fun z => u (-z)) f x= (-1 : ℝ) ^ j * coordJetOn (rectBox lo hi) j u f (-x)Proof (Lean source)
theorem coordJetOn_rectBox_neg {d j : ℕ} (lo hi : Fin d → ℝ) (hbox : ∀ i, lo i < hi i) (u : (Fin d → ℝ) → ℝ) (f : Fin j → Fin d) {x : Fin d → ℝ} (hx : x ∈ rectBox (fun i => -hi i) (fun i => -lo i)) : coordJetOn (rectBox (fun i => -hi i) (fun i => -lo i)) j (fun z => u (-z)) f x = (-1 : ℝ) ^ j * coordJetOn (rectBox lo hi) j u f (-x) := by let e : (Fin d → ℝ) ≃L[ℝ] (Fin d → ℝ) := (LinearIsometryEquiv.neg ℝ).toContinuousLinearEquiv have he (z : Fin d → ℝ) : e z = -z := by simp [e] have hpre : e ⁻¹' rectBox lo hi = rectBox (fun i => -hi i) (fun i => -lo i) := by ext z change e z ∈ rectBox lo hi ↔ z ∈ rectBox (fun i => -hi i) (fun i => -lo i) rw [he] exact (mem_rectBox_neg_iff lo hi z).symm have hx' : e x ∈ rectBox lo hi := by rw [he] exact (mem_rectBox_neg_iff lo hi x).mp hx unfold coordJetOn rw [← hpre] change iteratedFDerivWithin ℝ j (u ∘ e) (e ⁻¹' rectBox lo hi) x (fun k => single (f k) 1) = _ rw [e.iteratedFDerivWithin_comp_right u (uniqueDiffOn_rectBox lo hi hbox) hx' j] simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousLinearEquiv.coe_coe] have hb (k : Fin j) : e (single (f k) (1 : ℝ)) = (-1 : ℝ) • single (f k) (1 : ℝ) := by rw [he] simp simp only [hb] rw [ContinuousMultilinearMap.map_smul_univ] simp [Finset.prod_const, smul_eq_mul, he]
RectangularTwoFaceReflection 1 core · 0 supporting Successive lower- and upper-face reflections extend an intrinsic Hölder ball to a larger rectangular box while preserving its values on the starting box. ★ exists_rectTwoFaceReflection_holder_constant
Controlled reflection across both faces of one coordinate
Successive lower- and upper-face reflections extend an intrinsic Hölder ball to a larger rectangular box while preserving its values on the starting box.
If 0 < s and the box with corners lo, hi has positive side lengths, then for derivative order m and coordinate i there is a positive constant C such that every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the box agrees on the box with a response in the intrinsic Hölder ball of radius C·L on the box enlarged by collars across both faces of coordinate i (first the left collar, then the right collar of the resulting box). The constant depends only on the box, m, s and i.
Formal statement
Proof (Lean source)
ReflectionCoefficients 1 core · 0 supporting The one-sided reflection construction combines finitely many inward samples. ★ exists_reflection_coefficients
Finite reflection coefficients for cube extension
The one-sided reflection construction combines finitely many inward samples. Its coefficients reproduce boundary derivatives through a prescribed order.
For every derivative order m there are real weights a_0, …, a_m such that, for every k ≤ m, the sum over i of a_i·(−(i + 1))^k equals one; that is, the negative integer dilation factors −1, …, −(m + 1) admit weights all of whose moments through order m equal one.
Formal statement
Proof (Lean source)
ReflectionCollarControl 1 core · 0 supporting This module packages the regularity and quantitative jet estimates of a single face reflection on the enlarged closed cube collar. ★ exists_leftFaceReflection_collar_holder_constant
Intrinsic Hölder control after one face reflection
This module packages the regularity and quantitative jet estimates of a single face reflection on the enlarged closed cube collar. It is the local input for iterating reflections over all faces.
If 0 < s and the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, then for the left face in coordinate i there is a positive constant C such that the one-face reflection of every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube lies in the intrinsic Hölder ball of radius C·L on the closed left collar. The constant depends only on the dimension, m, s, the face and the weights.
Formal statement
Proof (Lean source)
ReflectionCollarCrossing 1 core · 0 supporting A segment from the exterior slab to the original cube crosses their shared face. ★ exists_leftFaceReflection_crossing_point
A crossing point on a reflected cube face
A segment from the exterior slab to the original cube crosses their shared face. The crossing point gives a common comparison point for Hölder estimates.
If x lies in the closed exterior slab of the left collar in coordinate i and y lies in the normalized cube, then some point z of the segment from x to y lies both in the slab and in the cube (hence on the left face), and both ‖x − z‖ and ‖z − y‖ are at most ‖x − y‖.
Formal statement
Proof (Lean source)
ReflectionCollarCubeEstimates 1 core · 0 supporting The reflected function agrees with the input on the original cube. ★ exists_leftFaceReflection_cube_jet_control_constant
Quantitative reflected jets on the original cube
The reflected function agrees with the input on the original cube. Its within-collar jets there consequently inherit the full intrinsic cube bounds.
If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, then there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, the within-collar Fréchet derivatives of the one-face reflection of u of every order at most m have operator norm at most C·L at every cube point, and its order-m within-collar derivative is s-Hölder with coefficient C·L between any two cube points.
Formal statement
Proof (Lean source)
ReflectionCollarEstimates 1 core · 0 supporting The open exterior estimates extend to the closed exterior by continuity of intrinsic jets. ★ exists_leftFaceReflection_collar_derivBound_constant
Quantitative bounds on a closed one-face reflection collar
The open exterior estimates extend to the closed exterior by continuity of intrinsic jets. Bounds on the cube and exterior then combine on the collar.
If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, then there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, every intrinsic coordinate jet of order at most m of the one-face reflection of u is bounded in absolute value by C·L throughout the closed left collar.
Formal statement
Proof (Lean source)
ReflectionCollarGeometry 1 core · 6 supporting The cube and its closed exterior slab are the two closed pieces used to glue one-face reflection. ★ leftClosedExteriorCollar_inter_cube
Geometry of the closed one-face reflection collar
The cube and its closed exterior slab are the two closed pieces used to glue one-face reflection. Their union is the collar and their overlap is the face.
The closed exterior slab and the normalized cube overlap exactly in the selected left face, the set of cube points whose i-th coordinate equals −1, edges and corners included.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
closure_leftOpenCubeCollartheorem — The closure of the open exterior collar at the left face in coordinate i is the closed exterior slab, including the face itself and all remaining coordinate edges.Proof (Lean source)
theorem closure_leftOpenCubeCollar (d m : ℕ) (i : Fin d) : closure (leftOpenCubeCollar d m i) = leftClosedExteriorCollar d m i := by have hopen : leftOpenCubeCollar d m i = Set.univ.pi (fun j : Fin d => if j = i then Ioo (-1 - (1 : ℝ) / ((m : ℝ) + 1)) (-1) else Ioo (-1 : ℝ) 1) := by ext x simp only [leftOpenCubeCollar, Set.mem_ofPred_eq, Set.mem_univ_pi] constructor <;> intro hx j <;> by_cases hj : j = i <;> simpa [hj] using hx j rw [hopen, leftClosedExteriorCollar_eq_pi, closure_pi_set] congr 1 funext j by_cases h : j = i · subst j simp only [↓reduceIte] rw [closure_Ioo] have hpos : 0 < (1 : ℝ) / ((m : ℝ) + 1) := by positivity linarith · simp [h, closure_Ioo (by norm_num : (-1 : ℝ) ≠ 1)] -
isClosed_leftClosedExteriorCollartheorem — The closed exterior slab of a one-face cube collar is a closed set.Proof (Lean source)
theorem isClosed_leftClosedExteriorCollar (d m : ℕ) (i : Fin d) : IsClosed (leftClosedExteriorCollar d m i) := by rw [leftClosedExteriorCollar_eq_pi] apply isClosed_set_pi intro j hj split_ifs <;> exact isClosed_Icc -
isClosed_leftCubeCollartheorem — A one-face cube collar is a closed set.Proof (Lean source)
theorem isClosed_leftCubeCollar (d m : ℕ) (i : Fin d) : IsClosed (leftCubeCollar d m i) := by have hpi : leftCubeCollar d m i = Set.univ.pi (fun j : Fin d => if j = i then Icc (-1 - (1 : ℝ) / ((m : ℝ) + 1)) 1 else Icc (-1 : ℝ) 1) := by ext x simp only [leftCubeCollar, Set.mem_ofPred_eq, Set.mem_univ_pi] constructor <;> intro hx j <;> specialize hx j <;> split_ifs at hx ⊢ <;> exact hx rw [hpi] apply isClosed_set_pi intro j hj split_ifs <;> exact isClosed_Icc -
uniqueDiffOn_leftClosedExteriorCollartheorem — The closed exterior slab of a one-face cube collar has unique within-set derivatives at every point.Proof (Lean source)
theorem uniqueDiffOn_leftClosedExteriorCollar (d m : ℕ) (i : Fin d) : UniqueDiffOn ℝ (leftClosedExteriorCollar d m i) := by rw [leftClosedExteriorCollar_eq_pi] apply UniqueDiffOn.pi intro j hj split_ifs · apply uniqueDiffOn_Icc have hpos : 0 < (1 : ℝ) / ((m : ℝ) + 1) := by positivity linarith · exact uniqueDiffOn_Icc (by norm_num) -
uniqueDiffOn_leftCubeCollartheorem — The closed one-face cube collar has unique within-set derivatives at every point.Proof (Lean source)
theorem uniqueDiffOn_leftCubeCollar (d m : ℕ) (i : Fin d) : UniqueDiffOn ℝ (leftCubeCollar d m i) := by have hpi : leftCubeCollar d m i = Set.univ.pi (fun j : Fin d => if j = i then Icc (-1 - (1 : ℝ) / ((m : ℝ) + 1)) 1 else Icc (-1 : ℝ) 1) := by ext x simp only [leftCubeCollar, Set.mem_ofPred_eq, Set.mem_univ_pi] constructor <;> intro hx j <;> specialize hx j <;> split_ifs at hx ⊢ <;> exact hx rw [hpi] apply UniqueDiffOn.pi intro j hj split_ifs · apply uniqueDiffOn_Icc have hpos : 0 < (1 : ℝ) / ((m : ℝ) + 1) := by positivity linarith · exact uniqueDiffOn_Icc (by norm_num) -
leftClosedExteriorCollar_union_cubetheorem — The closed exterior slab and the normalized cube together make up the whole closed one-face collar.hypothesesd m :ℕi :Fin dconclusionleftClosedExteriorCollar d m i ∪ cube d = leftCubeCollar d m iProof (Lean source)
theorem leftClosedExteriorCollar_union_cube (d m : ℕ) (i : Fin d) : leftClosedExteriorCollar d m i ∪ cube d = leftCubeCollar d m i := by ext x constructor · rintro (hx | hx) · exact hx.1 · intro j by_cases h : j = i · subst j simp only [↓reduceIte, Set.mem_Icc] have hi := hx i have hnonneg : 0 ≤ (1 : ℝ) / ((m : ℝ) + 1) := by positivity exact ⟨by linarith [hi.1], hi.2⟩ · simpa [leftCubeCollar, h] using hx j · intro hx by_cases hxi : x i ≤ -1 · exact inl ⟨hx, hxi⟩ · right intro j by_cases h : j = i · subst j have hi := hx i simp only [↓reduceIte, Set.mem_Icc] at hi exact ⟨le_of_not_ge hxi, hi.2⟩ · simpa [leftCubeCollar, h] using hx j
ReflectionCollarModulus 1 core · 0 supporting The top-order derivative has a controlled modulus on each closed side of the face. ★ exists_leftFaceReflection_collar_modulus_constant
Hölder modulus across a reflected cube face
The top-order derivative has a controlled modulus on each closed side of the face. A segment crossing point combines those bounds for opposite-side pairs.
If 0 < s and the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, then there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, the top-order intrinsic coordinate jets of the one-face reflection of u have an s-Hölder modulus with coefficient C·L throughout the closed left collar.
Formal statement
Proof (Lean source)
ReflectionCollarRestriction 1 core · 0 supporting After face gluing, the within-collar jets of a reflected response coincide on the original cube with its intrinsic cube jets, including face edges. ★ leftFaceReflection_withinJet_eq_cube
Restricting reflected collar jets to the original cube
After face gluing, the within-collar jets of a reflected response coincide on the original cube with its intrinsic cube jets, including face edges.
If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, a response u is m times continuously differentiable within the closed cube, and j ≤ m, then at every point x of the cube the order-j within-collar Fréchet derivative of the one-face reflection of u equals the order-j within-cube derivative of u.
Formal statement
Proof (Lean source)
ReflectionCollarSideEstimates 1 core · 1 supporting The open exterior estimates pass to the face and the other coordinate edges through continuous within-collar jets. ★ exists_leftFaceReflection_closedExterior_top_modulus
Quantitative jets on the closed exterior side of a face collar
The open exterior estimates pass to the face and the other coordinate edges through continuous within-collar jets. Both conclusions concern derivatives within the full collar, so they can be used directly in collar bounds.
If s > 0 and the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, then there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, the order-m within-collar Fréchet derivative of the one-face reflection of u is s-Hölder with coefficient C·L between any two points of the closed exterior slab.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
exists_leftFaceReflection_closedExterior_jet_boundtheorem — If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, then there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, the within-collar Fréchet derivatives of the one-face reflection of u of every order at most m have operator norm at most C·L at every point of the closed exterior slab.hypothesesconclusion∃ C : ℝ,0 < Cconclusion 1u :(Fin d → ℝ) → ℝL :ℝ0 ≤ LCubeHolderBall d m s L uj ≤ m :x ∈ leftClosedExteriorCollar d m i :‖iteratedFDerivWithin ℝ j (leftFaceReflection d m i a u) (leftCubeCollar d m i) x‖ ≤ C * LProof (Lean source)
theorem exists_leftFaceReflection_closedExterior_jet_bound (d m : ℕ) (s : ℝ) (i : Fin d) (a : Fin (m + 1) → ℝ) (ha : ∀ k : Fin (m + 1), (∑ q : Fin (m + 1), a q * (-((q.val : ℝ) + 1)) ^ (k.val : ℕ)) = 1) : ∃ C : ℝ, 0 < C ∧ ∀ (u : (Fin d → ℝ) → ℝ) (L : ℝ), 0 ≤ L → CubeHolderBall d m s L u → ∀ j ≤ m, ∀ x ∈ leftClosedExteriorCollar d m i, ‖iteratedFDerivWithin ℝ j (leftFaceReflection d m i a u) (leftCubeCollar d m i) x‖ ≤ C * L := by obtain ⟨C, hC, hbound⟩ := exists_leftFaceReflection_jet_bound d m s i a refine ⟨C, hC, ?_⟩ intro u L hL hu j hj x hx have hreg := leftFaceReflection_contDiffOn_collar d m i a ha u hu.regularity have hcont : ContinuousOn (fun z => ‖iteratedFDerivWithin ℝ j (leftFaceReflection d m i a u) (leftCubeCollar d m i) z‖) (leftCubeCollar d m i) := ((hreg.continuousOn_iteratedFDerivWithin (by exact_mod_cast hj) (uniqueDiffOn_leftCubeCollar d m i)).norm) have hle := le_on_closure (s := leftOpenCubeCollar d m i) (f := fun z => ‖iteratedFDerivWithin ℝ j (leftFaceReflection d m i a u) (leftCubeCollar d m i) z‖) (g := fun _ => C * L) (by intro z hz rw [leftFaceReflection_withinJet_eq_ambient_on_open d m j i a u hu.regularity hj z hz] exact hbound u L hL hu j hj z hz) (by rw [closure_leftOpenCubeCollar] exact hcont.mono (fun z hz => hz.1)) continuousOn_const exact hle (by rwa [closure_leftOpenCubeCollar])
ReflectionFaceAlgebra 1 core · 0 supporting The reflection moment equations recover every coordinate evaluation of a multilinear jet through the prescribed order. ★ reflection_weighted_coordinate_jet
Algebraic matching of reflected face jets
The reflection moment equations recover every coordinate evaluation of a multilinear jet through the prescribed order. This is the algebraic input to matching the exterior jet trace to the intrinsic cube jet at a face.
If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m and j ≤ m, then for every continuous j-linear map T and coordinate directions f the weighted sum over q of a_q times T evaluated on the standard basis vectors e_{f(k)}, each scaled by −(q + 1) when f(k) = i and left unscaled otherwise, equals T evaluated on the unscaled basis vectors.
Proof (Lean source)
ReflectionFaceFirstDeriv 1 core · 0 supporting This module isolates the first differentiability step in gluing a finite reflection sum to the original response. ★ leftFaceReflection_hasFDerivWithinAt_face
First derivative at a reflected cube face
This module isolates the first differentiability step in gluing a finite reflection sum to the original response. The derivative is taken within the closed collar, so its value does not depend on the original response outside the normalized cube.
If m ≥ 1, the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, a response u is m times continuously differentiable within the closed cube, and x is a cube point on the left face in coordinate i, then the one-face reflection of u has, within the closed left collar at x, derivative equal to the within-cube derivative of u at x.
Formal statement
Proof (Lean source)
ReflectionFaceGluing 1 core · 0 supporting The reflected exterior branch and the original response have matching jets at their common face. ★ leftFaceReflection_contDiffOn_collar
Gluing a one-face reflection to the cube
The reflected exterior branch and the original response have matching jets at their common face. This module packages that match as regularity on the closed one-face collar, including its edges and corners.
If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m and a response u is m times continuously differentiable within the closed cube, then the one-face reflection of u across the left face in coordinate i is m times continuously differentiable within the closed left collar.
Formal statement
Proof (Lean source)
ReflectionFaceJets 1 core · 0 supporting The within-set jets of the closed exterior reflection agree with the original cube jets on their common face, including edges and corners. ★ leftFaceReflection_closedExterior_jet_eq_face
Intrinsic jets of the reflected exterior at a face
The within-set jets of the closed exterior reflection agree with the original cube jets on their common face, including edges and corners. This is the trace identity needed before gluing the two closed pieces.
If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, a response u is m times continuously differentiable within the closed cube, j ≤ m, and x is a cube point on the left face in coordinate i, then the order-j derivative of the one-face reflection of u within the closed exterior slab at x equals the order-j within-cube derivative of u at x. This holds at edges and corners of the face as well as in its relative interior.
Formal statement
Proof (Lean source)
ReflectionFaceLimit 1 core · 1 supporting The ambient jets of a one-face reflection on its open exterior collar tend to the intrinsic cube jets at the face. ★ leftFaceReflection_jet_tendsto_face
Boundary trace of reflected jets
The ambient jets of a one-face reflection on its open exterior collar tend to the intrinsic cube jets at the face. This statement is about a limit from the collar, so it does not use ambient boundary jets of the original response.
If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, a response u is m times continuously differentiable within the closed cube, j ≤ m, and x is a cube point on the left face in coordinate i, then as z approaches x from within the open exterior collar, the order-j ambient derivative of the one-face reflection of u at z converges to the order-j within-cube derivative of u at x.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
leftFaceReflection_coordinate_jet_tendsto_facetheorem — If the reflection weights a satisfy the moment conditions Σ_q a_q·(−(q + 1))^k = 1 for every k ≤ m, a response u is m times continuously differentiable within the closed cube, j ≤ m, and x is a cube point on the left face in coordinate i, then as z approaches x from within the open exterior collar, the order-j ambient derivative of the one-face reflection of u at z, evaluated on the standard basis vectors in directions f, converges to the order-j within-cube derivative of u at x evaluated on the same vectors. The moment equations cancel the inward sample factors.hypothesesd m :ℕi :Fin da :Fin (m + 1) → ℝu :(Fin d → ℝ) → ℝhu :ContDiffOn ℝ m u (cube d)j :ℕhj :j ≤ mx :Fin d → ℝhx :x ∈ cube dhxi :x i = -1conclusionTendsto (fun z => iteratedFDeriv ℝ j (leftFaceReflection d m i a u) z (fun k => single (f k) (1 : ℝ))) (nhdsWithin x (leftOpenCubeCollar d m i)) (nhds (iteratedFDerivWithin ℝ j u (cube d) x (fun k => single (f k) (1 : ℝ))))Proof (Lean source)
theorem leftFaceReflection_coordinate_jet_tendsto_face (d m : ℕ) (i : Fin d) (a : Fin (m + 1) → ℝ) (ha : ∀ k : Fin (m + 1), (∑ q : Fin (m + 1), a q * (-((q.val : ℝ) + 1)) ^ (k.val : ℕ)) = 1) (u : (Fin d → ℝ) → ℝ) (hu : ContDiffOn ℝ m u (cube d)) (j : ℕ) (hj : j ≤ m) (f : Fin j → Fin d) (x : Fin d → ℝ) (hx : x ∈ cube d) (hxi : x i = -1) : Tendsto (fun z => iteratedFDeriv ℝ j (leftFaceReflection d m i a u) z (fun k => single (f k) (1 : ℝ))) (nhdsWithin x (leftOpenCubeCollar d m i)) (nhds (iteratedFDerivWithin ℝ j u (cube d) x (fun k => single (f k) (1 : ℝ)))) := by classical have hsum : Tendsto (fun z => ∑ q : Fin (m + 1), a q * iteratedFDeriv ℝ j (fun y => u (leftFaceSample d i q y)) z (fun k => single (f k) (1 : ℝ))) (nhdsWithin x (leftOpenCubeCollar d m i)) (nhds (∑ q : Fin (m + 1), a q * iteratedFDerivWithin ℝ j u (cube d) x (fun k => (if f k = i then -((q.val : ℝ) + 1) else 1) • single (f k) (1 : ℝ)))) := by apply tendsto_finsetSum intro q hq exact tendsto_const_nhds.mul (leftFaceSample_coordinate_jet_tendsto_face d m i q u hu j hj f x hx hxi) rw [reflection_weighted_coordinate_jet d m i a ha j hj (iteratedFDerivWithin ℝ j u (cube d) x) f] at hsum apply hsum.congr' filter_upwards [self_mem_nhdsWithin] with z hz rw [leftFaceReflection_iteratedFDeriv_eq_sum d m i a u hu j hj z hz] simp [smul_eq_mul]
ReflectionInterior 1 core · 0 supporting Every inward sample of an open collar point lies in the open cube. ★ leftFaceReflection_contDiffOn_openCollar
Interior regularity of a one-face reflection
Every inward sample of an open collar point lies in the open cube. Thus the finite reflection sum inherits all available interior derivatives of the original response. This is the interior half of the face-gluing argument; matching the derivatives at the face is a separate obligation.
If a response u is m times continuously differentiable within the closed cube, then for any reflection weights a the one-face reflection of u across the left face in coordinate i is m times continuously differentiable on the open exterior collar.
Formal statement
Proof (Lean source)
ReflectionPolynomial 1 core · 0 supporting The reflection weights reproduce every Taylor polynomial through the chosen order. ★ reflection_taylor_polynomial
Polynomial reproduction by one-sided reflection
The reflection weights reproduce every Taylor polynomial through the chosen order. This algebraic identity is the jet-matching step at a cube face.
If the reflection weights a satisfy the moment conditions Σ_i a_i·(−(i + 1))^k = 1 for every k ≤ m, then for every polynomial with coefficients c_0, …, c_m and every real t, the weighted sum over i of a_i times the polynomial evaluated at −(i + 1)·t equals the polynomial evaluated at t; that is, moment-matched weights reproduce every polynomial of degree at most m.
Proof (Lean source)
ReflectionQuantitative 1 core · 1 supporting The affine samples used by one-face reflection have a uniform Lipschitz constant. ★ leftFaceReflection_abs_le_openCollar
Quantitative estimates for inward face samples
The affine samples used by one-face reflection have a uniform Lipschitz constant. On the exterior collar, their weighted sum inherits a value bound from the intrinsic cube ball. These estimates are inputs to the higher-jet reflection bounds.
If a response u lies in the intrinsic Hölder ball of order m, exponent s and radius L on the normalized cube, then at every point x of the open exterior collar the one-face reflection of u has absolute value at most (Σ_q |a_q|)·L.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
leftFaceSample_lipschitztheorem — The inward reflection sample with dilation index q is Lipschitz for the supremum norm with constant q + 1: it moves two points apart by at most q + 1 times their distance.hypothesesconclusion‖leftFaceSample d i q x - leftFaceSample d i q y‖ ≤ ((q : ℝ) + 1) * ‖x - y‖Proof (Lean source)
theorem leftFaceSample_lipschitz (d : ℕ) (i : Fin d) (q : ℕ) (x y : Fin d → ℝ) : ‖leftFaceSample d i q x - leftFaceSample d i q y‖ ≤ ((q : ℝ) + 1) * ‖x - y‖ := by apply (pi_norm_le_iff_of_nonneg (mul_nonneg (by positivity) (norm_nonneg (x - y)))).2 intro j by_cases hji : j = i · subst j have heq : (leftFaceSample d i q x - leftFaceSample d i q y) i = -((q : ℝ) + 1) * (x - y) i := by simp [leftFaceSample, Pi.sub_apply] ring rw [heq, norm_mul, norm_neg, Real.norm_eq_abs, abs_of_nonneg (show 0 ≤ (q : ℝ) + 1 by positivity)] exact mul_le_mul_of_nonneg_left (norm_le_pi_norm (x - y) i) (by positivity) · have heq : (leftFaceSample d i q x - leftFaceSample d i q y) j = (x - y) j := by simp [leftFaceSample_other i j q x hji, leftFaceSample_other i j q y hji, Pi.sub_apply] rw [heq] calc ‖(x - y) j‖ ≤ ‖x - y‖ := norm_le_pi_norm (x - y) j _ ≤ ((q : ℝ) + 1) * ‖x - y‖ := by nlinarith [norm_nonneg (x - y), Nat.cast_nonneg (α := ℝ) q]
ReflectionSampleJets 1 core · 4 supporting This module bounds ambient jets of each inward sample on the open exterior collar, then combines them into the corresponding finite one-face reflection. ★ exists_leftFaceReflection_top_modulus
Jets of inward samples and one-face reflections
This module bounds ambient jets of each inward sample on the open exterior collar, then combines them into the corresponding finite one-face reflection. Every sample point lies in the open cube, where ambient and intrinsic jets agree. The affine map's operator norm is bounded by its dilation factor.
If s > 0, then for the left face in coordinate i and fixed reflection weights a there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, the order-m ambient derivative of the one-face reflection of u is s-Hölder with coefficient C·L between any two points of the open exterior collar.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
exists_leftFaceSample_jet_boundtheorem — For the left face in coordinate i and a dilation index q, there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, every ambient derivative of order at most m of the composite y ↦ u(inward sample of y) has operator norm at most C·L on the open exterior collar. The constant does not depend on the response or the radius.hypothesesconclusion∃ C : ℝ,0 < Cconclusion 1‖iteratedFDeriv ℝ j (fun y => u (leftFaceSample d i q y)) x‖ ≤ C * LProof (Lean source)
theorem exists_leftFaceSample_jet_bound (d m : ℕ) (s : ℝ) (i : Fin d) (q : Fin (m + 1)) : ∃ C : ℝ, 0 < C ∧ ∀ (u : (Fin d → ℝ) → ℝ) (L : ℝ), 0 ≤ L → CubeHolderBall d m s L u → ∀ j ≤ m, ∀ x ∈ leftOpenCubeCollar d m i, ‖iteratedFDeriv ℝ j (fun y => u (leftFaceSample d i q y)) x‖ ≤ C * L := by classical obtain ⟨K, hK, hKbound⟩ := exists_full_intrinsic_jet_bounds d m s let a : Fin d → ℝ := leftFaceSample d i q 0 let g : (Fin d → ℝ) →L[ℝ] (Fin d → ℝ) := { toFun := fun x j => if j = i then -((q : ℝ) + 1) * x j else x j map_add' := by intro x y ext j by_cases hj : j = i <;> simp [hj, mul_add] map_smul' := by intro c x ext j by_cases hj : j = i <;> simp [hj] ring cont := by apply continuous_pi intro j by_cases hj : j = i · subst j simp only exact (continuous_const.mul (continuous_apply i) : Continuous (fun x : Fin d → ℝ => -((q : ℝ) + 1) * x i)) · simpa [hj] using (continuous_apply j) } have hsamp (y : Fin d → ℝ) : leftFaceSample d i q y = g y + a := by ext j by_cases hj : j = i · subst j simp [g, a, leftFaceSample] ring · simp [g, a, leftFaceSample, hj] have hg : ‖g‖ ≤ (q : ℝ) + 1 := by apply g.opNorm_le_bound (by positivity) intro y have heq : g y = leftFaceSample d i q y - leftFaceSample d i q 0 := by rw [hsamp] simp [a] rw [heq] simpa using leftFaceSample_lipschitz d i q y 0 refine ⟨K * ((q : ℝ) + 1) ^ m, mul_pos hK (pow_pos (by positivity) _), ?_⟩ intro u L hL hu j hj x hx let S : Set (Fin d → ℝ) := {z | z + a ∈ openCube d} let f : (Fin d → ℝ) → ℝ := fun z => u (z + a) have hopen : IsOpen (openCube d) := isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo) have hsub : openCube d ⊆ cube d := by intro z hz k exact ⟨(hz k trivial).1.le, (hz k trivial).2.le⟩ have hSopen : IsOpen S := hopen.preimage (continuous_id.add continuous_const) have hSf : ContDiffOn ℝ m f S := by have htrans : ContDiff ℝ m (fun z : Fin d → ℝ => z + a) := contDiff_id.add contDiff_const exact (hu.regularity.mono hsub).comp htrans.contDiffOn (fun z hz => hz) have hsrc : g x ∈ S := by change g x + a ∈ openCube d rw [← hsamp] exact leftFaceSample_mem_openCube i q x hx have htarget : ContDiffAt ℝ j (f ∘ g) x := (hSf.comp_continuousLinearMap g).contDiffAt ((hSopen.preimage g.continuous).mem_nhds hsrc) |>.of_le (by exact_mod_cast hj) have hsource : ContDiffAt ℝ j f (g x) := hSf.contDiffAt (hSopen.mem_nhds hsrc) |>.of_le (by exact_mod_cast hj) have hchain := g.iteratedFDerivWithin_comp_right hSf hSopen.uniqueDiffOn (hSopen.preimage g.continuous).uniqueDiffOn hsrc (show j ≤ (m : WithTop ℕ∞) by exact_mod_cast hj) have hjet : iteratedFDeriv ℝ j (fun y => u (leftFaceSample d i q y)) x = (iteratedFDeriv ℝ j u (leftFaceSample d i q x)).compContinuousLinearMap (fun _ => g) := by have hfun : (fun y => u (leftFaceSample d i q y)) = f ∘ g := by funext y simp [f, hsamp] rw [hfun, ← iteratedFDerivWithin_eq_iteratedFDeriv (hSopen.preimage g.continuous).uniqueDiffOn htarget hsrc] rw [hchain] rw [iteratedFDerivWithin_eq_iteratedFDeriv hSopen.uniqueDiffOn hsource hsrc] rw [iteratedFDeriv_comp_add_right j a (g x)] rw [hsamp] rw [hjet] have hs : leftFaceSample d i q x ∈ cube d := hsub (leftFaceSample_mem_openCube i q x hx) have hfull : ‖iteratedFDeriv ℝ j u (leftFaceSample d i q x)‖ ≤ K * L := by have hreg : ContDiffAt ℝ j u (leftFaceSample d i q x) := (hu.regularity.mono hsub).contDiffAt (hopen.mem_nhds (leftFaceSample_mem_openCube i q x hx)) |>.of_le (by exact_mod_cast hj) have hcube : UniqueDiffOn ℝ (cube d) := by have hc : cube d = Set.univ.pi (fun _ : Fin d => Icc (-1 : ℝ) 1) := by ext z simp [cube, normalizedCube, Pi.le_def, forall_and] rw [hc] exact UniqueDiffOn.pi (fun _ _ => uniqueDiffOn_Icc (by norm_num)) rw [← iteratedFDerivWithin_eq_iteratedFDeriv hcube hreg hs] exact (hKbound u L hL hu).1 j hj _ hs calc _ ≤ ‖iteratedFDeriv ℝ j u (leftFaceSample d i q x)‖ * ∏ _k : Fin j, ‖g‖ := ContinuousMultilinearMap.norm_compContinuousLinearMap_le _ _ _ = ‖iteratedFDeriv ℝ j u (leftFaceSample d i q x)‖ * ‖g‖ ^ j := by simp _ ≤ (K * L) * ((q : ℝ) + 1) ^ j := by gcongr _ ≤ (K * L) * ((q : ℝ) + 1) ^ m := by gcongr have hq : 0 ≤ ((q : ℕ) : ℝ) := Nat.cast_nonneg _ linarith _ = (K * ((q : ℝ) + 1) ^ m) * L := by ring -
exists_leftFaceSample_top_modulustheorem — If s > 0, then for the left face in coordinate i and a dilation index q there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, the order-m ambient derivative of the composite z ↦ u(inward sample of z) is s-Hölder with coefficient C·L between any two points of the open exterior collar.hypothesesconclusion∃ C : ℝ,0 < Cconclusion 1u :(Fin d → ℝ) → ℝL :ℝ0 ≤ LCubeHolderBall d m s L ux ∈ leftOpenCubeCollar d m i :y ∈ leftOpenCubeCollar d m i :‖iteratedFDeriv ℝ m (fun z => u (leftFaceSample d i q z)) x - iteratedFDeriv ℝ m (fun z => u (leftFaceSample d i q z)) y‖≤ C * L * ‖x - y‖ ^ sProof (Lean source)
theorem exists_leftFaceSample_top_modulus (d m : ℕ) (s : ℝ) (hs : 0 < s) (i : Fin d) (q : Fin (m + 1)) : ∃ C : ℝ, 0 < C ∧ ∀ (u : (Fin d → ℝ) → ℝ) (L : ℝ), 0 ≤ L → CubeHolderBall d m s L u → ∀ x ∈ leftOpenCubeCollar d m i, ∀ y ∈ leftOpenCubeCollar d m i, ‖iteratedFDeriv ℝ m (fun z => u (leftFaceSample d i q z)) x - iteratedFDeriv ℝ m (fun z => u (leftFaceSample d i q z)) y‖ ≤ C * L * ‖x - y‖ ^ s := by classical obtain ⟨K, hK, hKbound⟩ := exists_full_intrinsic_jet_bounds d m s let a : Fin d → ℝ := leftFaceSample d i q 0 let g : (Fin d → ℝ) →L[ℝ] (Fin d → ℝ) := { toFun := fun x j => if j = i then -((q : ℝ) + 1) * x j else x j map_add' := by intro x y ext j by_cases hj : j = i <;> simp [hj, mul_add] map_smul' := by intro c x ext j by_cases hj : j = i <;> simp [hj] ring cont := by apply continuous_pi intro j by_cases hj : j = i · subst j simp only exact (continuous_const.mul (continuous_apply i) : Continuous (fun x : Fin d → ℝ => -((q : ℝ) + 1) * x i)) · simpa [hj] using (continuous_apply j) } have hsamp (z : Fin d → ℝ) : leftFaceSample d i q z = g z + a := by ext j by_cases hj : j = i · subst j simp [g, a, leftFaceSample] ring · simp [g, a, leftFaceSample, hj] have hg : ‖g‖ ≤ (q : ℝ) + 1 := by apply g.opNorm_le_bound (by positivity) intro z have heq : g z = leftFaceSample d i q z - leftFaceSample d i q 0 := by rw [hsamp] simp [a] rw [heq] simpa using leftFaceSample_lipschitz d i q z 0 let S : Set (Fin d → ℝ) := {z | z + a ∈ openCube d} have hopen : IsOpen (openCube d) := isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo) have hsub : openCube d ⊆ cube d := by intro z hz k exact ⟨(hz k trivial).1.le, (hz k trivial).2.le⟩ have hSopen : IsOpen S := hopen.preimage (continuous_id.add continuous_const) have hcube : UniqueDiffOn ℝ (cube d) := by have hc : cube d = Set.univ.pi (fun _ : Fin d => Icc (-1 : ℝ) 1) := by ext z simp [cube, normalizedCube, Pi.le_def, forall_and] rw [hc] exact UniqueDiffOn.pi (fun _ _ => uniqueDiffOn_Icc (by norm_num)) refine ⟨K * ((q : ℝ) + 1) ^ m * ((q : ℝ) + 1) ^ s, mul_pos (mul_pos hK (pow_pos (by positivity) _)) (Real.rpow_pos_of_pos (by positivity) _), ?_⟩ intro u L hL hu x hx y hy let f : (Fin d → ℝ) → ℝ := fun z => u (z + a) have hSf : ContDiffOn ℝ m f S := by have htrans : ContDiff ℝ m (fun z : Fin d → ℝ => z + a) := contDiff_id.add contDiff_const exact (hu.regularity.mono hsub).comp htrans.contDiffOn (fun z hz => hz) have hjet (z : Fin d → ℝ) (hz : z ∈ leftOpenCubeCollar d m i) : iteratedFDeriv ℝ m (fun w => u (leftFaceSample d i q w)) z = (iteratedFDeriv ℝ m u (leftFaceSample d i q z)).compContinuousLinearMap (fun _ => g) := by have hsrc : g z ∈ S := by change g z + a ∈ openCube d rw [← hsamp] exact leftFaceSample_mem_openCube i q z hz have htarget : ContDiffAt ℝ m (f ∘ g) z := (hSf.comp_continuousLinearMap g).contDiffAt ((hSopen.preimage g.continuous).mem_nhds hsrc) have hsource : ContDiffAt ℝ m f (g z) := hSf.contDiffAt (hSopen.mem_nhds hsrc) have hchain := g.iteratedFDerivWithin_comp_right hSf hSopen.uniqueDiffOn (hSopen.preimage g.continuous).uniqueDiffOn hsrc (show m ≤ (m : WithTop ℕ∞) by exact_mod_cast le_rfl) have hfun : (fun w => u (leftFaceSample d i q w)) = f ∘ g := by funext w simp [f, hsamp] rw [hfun, ← iteratedFDerivWithin_eq_iteratedFDeriv (hSopen.preimage g.continuous).uniqueDiffOn htarget hsrc] rw [hchain] rw [iteratedFDerivWithin_eq_iteratedFDeriv hSopen.uniqueDiffOn hsource hsrc] rw [iteratedFDeriv_comp_add_right m a (g z)] rw [hsamp] have hxy : ‖iteratedFDeriv ℝ m u (leftFaceSample d i q x) - iteratedFDeriv ℝ m u (leftFaceSample d i q y)‖ ≤ K * L * ‖leftFaceSample d i q x - leftFaceSample d i q y‖ ^ s := by have hreg (z : Fin d → ℝ) (hz : z ∈ leftOpenCubeCollar d m i) : ContDiffAt ℝ m u (leftFaceSample d i q z) := (hu.regularity.mono hsub).contDiffAt (hopen.mem_nhds (leftFaceSample_mem_openCube i q z hz)) rw [← iteratedFDerivWithin_eq_iteratedFDeriv hcube (hreg x hx) (hsub (leftFaceSample_mem_openCube i q x hx))] rw [← iteratedFDerivWithin_eq_iteratedFDeriv hcube (hreg y hy) (hsub (leftFaceSample_mem_openCube i q y hy))] exact (hKbound u L hL hu).2 _ (hsub (leftFaceSample_mem_openCube i q x hx)) _ (hsub (leftFaceSample_mem_openCube i q y hy)) rw [hjet x hx, hjet y hy] have hcomp : (iteratedFDeriv ℝ m u (leftFaceSample d i q x)).compContinuousLinearMap (fun _ => g) - (iteratedFDeriv ℝ m u (leftFaceSample d i q y)).compContinuousLinearMap (fun _ => g) = (iteratedFDeriv ℝ m u (leftFaceSample d i q x) - iteratedFDeriv ℝ m u (leftFaceSample d i q y)).compContinuousLinearMap (fun _ => g) := by ext v simp rw [hcomp] calc _ ≤ ‖iteratedFDeriv ℝ m u (leftFaceSample d i q x) - iteratedFDeriv ℝ m u (leftFaceSample d i q y)‖ * ∏ _k : Fin m, ‖g‖ := ContinuousMultilinearMap.norm_compContinuousLinearMap_le _ _ _ = ‖iteratedFDeriv ℝ m u (leftFaceSample d i q x) - iteratedFDeriv ℝ m u (leftFaceSample d i q y)‖ * ‖g‖ ^ m := by simp _ ≤ (K * L * ‖leftFaceSample d i q x - leftFaceSample d i q y‖ ^ s) * ((q : ℝ) + 1) ^ m := by gcongr _ ≤ (K * L * (((q : ℝ) + 1) * ‖x - y‖) ^ s) * ((q : ℝ) + 1) ^ m := by gcongr exact leftFaceSample_lipschitz d i q x y _ = (K * ((q : ℝ) + 1) ^ m * ((q : ℝ) + 1) ^ s) * L * ‖x - y‖ ^ s := by rw [Real.mul_rpow (by positivity) (norm_nonneg _)] ring -
leftFaceReflection_iteratedFDeriv_eq_sumtheorem — If a response u is m times continuously differentiable within the closed cube, j ≤ m, and x lies in the open exterior collar, then the order-j ambient derivative of the one-face reflection of u at x equals the weighted sum over q of a_q times the order-j ambient derivative at x of the composite z ↦ u(inward sample of z with dilation index q).hypothesesd m :ℕi :Fin da :Fin (m + 1) → ℝu :(Fin d → ℝ) → ℝhu :ContDiffOn ℝ m u (cube d)j :ℕhj :j ≤ mx :Fin d → ℝhx :x ∈ leftOpenCubeCollar d m iconclusioniteratedFDeriv ℝ j (leftFaceReflection d m i a u) xProof (Lean source)
theorem leftFaceReflection_iteratedFDeriv_eq_sum (d m : ℕ) (i : Fin d) (a : Fin (m + 1) → ℝ) (u : (Fin d → ℝ) → ℝ) (hu : ContDiffOn ℝ m u (cube d)) (j : ℕ) (hj : j ≤ m) (x : Fin d → ℝ) (hx : x ∈ leftOpenCubeCollar d m i) : iteratedFDeriv ℝ j (leftFaceReflection d m i a u) x = ∑ q : Fin (m + 1), a q • iteratedFDeriv ℝ j (fun z => u (leftFaceSample d i q z)) x := by classical have hcollar : IsOpen (leftOpenCubeCollar d m i) := by have hc : leftOpenCubeCollar d m i = Set.univ.pi (fun k : Fin d => if k = i then Ioo (-1 - (1 : ℝ) / ((m : ℝ) + 1)) (-1) else Ioo (-1 : ℝ) 1) := by ext z simp [leftOpenCubeCollar] constructor <;> intro h k <;> by_cases hk : k = i <;> simpa [hk] using h k rw [hc] apply isOpen_set_pi Set.finite_univ intro k hk split_ifs <;> exact isOpen_Ioo have hsub : openCube d ⊆ cube d := by intro z hz k exact ⟨(hz k trivial).1.le, (hz k trivial).2.le⟩ have hsample (q : Fin (m + 1)) : ContDiffOn ℝ m (fun z => u (leftFaceSample d i q z)) (leftOpenCubeCollar d m i) := by have hmap : ContDiff ℝ m (leftFaceSample d i q) := by rw [contDiff_pi] intro k by_cases h : k = i · subst k simpa [leftFaceSample] using (show ContDiff ℝ m (fun z : Fin d → ℝ => -1 + ((q : ℝ) + 1) * (-1 - z i)) by fun_prop) · simpa [leftFaceSample, h] using (show ContDiff ℝ m (fun z : Fin d → ℝ => z k) by fun_prop) exact (hu.mono hsub).comp hmap.contDiffOn (fun z hz => leftFaceSample_mem_openCube i q z hz) have hxi : x i < -1 := by have hmem : x i ∈ Ioo (-1 - (1 : ℝ) / ((m : ℝ) + 1)) (-1) := by simpa [leftOpenCubeCollar] using hx i exact hmem.2 have heq : leftFaceReflection d m i a u =ᶠ[nhds x] (fun z => ∑ q : Fin (m + 1), a q * u (leftFaceSample d i q z)) := by filter_upwards [(isOpen_lt (continuous_apply i) continuous_const).mem_nhds hxi] with z hz simp [leftFaceReflection, hz] rw [(heq.iteratedFDeriv ℝ j).eq_of_nhds] rw [iteratedFDeriv_fun_sum_apply] · apply Finset.sum_congr rfl intro q hq have hreg : ContDiffAt ℝ j (fun z => u (leftFaceSample d i q z)) x := ((hsample q).contDiffAt (hcollar.mem_nhds hx)).of_le (by exact_mod_cast hj) simpa only [smul_eq_mul] using (iteratedFDeriv_const_smul_apply' (a := a q) hreg) · intro q hq have hreg : ContDiffAt ℝ j (fun z => u (leftFaceSample d i q z)) x := ((hsample q).contDiffAt (hcollar.mem_nhds hx)).of_le (by exact_mod_cast hj) simpa only [smul_eq_mul] using (hreg.const_smul (a q)) -
exists_leftFaceReflection_jet_boundtheorem — For the left face in coordinate i and fixed reflection weights a, there is a positive constant C such that, for every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the normalized cube, every ambient derivative of order at most m of the one-face reflection of u has operator norm at most C·L on the open exterior collar. The constant may depend on the weights.hypothesesProof (Lean source)
theorem exists_leftFaceReflection_jet_bound (d m : ℕ) (s : ℝ) (i : Fin d) (a : Fin (m + 1) → ℝ) : ∃ C : ℝ, 0 < C ∧ ∀ (u : (Fin d → ℝ) → ℝ) (L : ℝ), 0 ≤ L → CubeHolderBall d m s L u → ∀ j ≤ m, ∀ x ∈ leftOpenCubeCollar d m i, ‖iteratedFDeriv ℝ j (leftFaceReflection d m i a u) x‖ ≤ C * L := by classical choose C hC hbound using (fun q : Fin (m + 1) => exists_leftFaceSample_jet_bound d m s i q) refine ⟨1 + ∑ q : Fin (m + 1), |a q| * C q, ?_, ?_⟩ · have hsum : 0 ≤ ∑ q : Fin (m + 1), |a q| * C q := by apply Finset.sum_nonneg intro q hq exact mul_nonneg (abs_nonneg _) (le_of_lt (hC q)) linarith intro u L hL hu j hj x hx calc ‖iteratedFDeriv ℝ j (leftFaceReflection d m i a u) x‖ = ‖∑ q : Fin (m + 1), a q • iteratedFDeriv ℝ j (fun z => u (leftFaceSample d i q z)) x‖ := by rw [leftFaceReflection_iteratedFDeriv_eq_sum d m i a u hu.regularity j hj x hx] _ ≤ ∑ q : Fin (m + 1), ‖a q • iteratedFDeriv ℝ j (fun z => u (leftFaceSample d i q z)) x‖ := norm_sum_le _ _ _ ≤ ∑ q : Fin (m + 1), |a q| * (C q * L) := by apply Finset.sum_le_sum intro q hq rw [norm_smul, Real.norm_eq_abs] exact mul_le_mul_of_nonneg_left (hbound q u L hL hu j hj x hx) (abs_nonneg _) _ = (∑ q : Fin (m + 1), |a q| * C q) * L := by rw [Finset.sum_mul] apply Finset.sum_congr rfl intro q hq ring _ ≤ (1 + ∑ q : Fin (m + 1), |a q| * C q) * L := by nlinarith
ReflectionSampleLimit 1 core · 0 supporting At a cube face, an affine inward sample has a boundary jet determined by the intrinsic jet of the original response and the sample's diagonal linear part. ★ leftFaceSample_coordinate_jet_tendsto_face
Boundary limits of inward sample jets
At a cube face, an affine inward sample has a boundary jet determined by the intrinsic jet of the original response and the sample's diagonal linear part. This isolates the chain-rule and continuity step used to glue reflections.
If a response u is m times continuously differentiable within the closed cube, j ≤ m, and x is a cube point on the left face in coordinate i, then as z approaches x from within the open exterior collar, the order-j ambient derivative at z of the composite y ↦ u(inward sample of y with dilation index q), evaluated on the standard basis vectors in directions f, converges to the order-j within-cube derivative of u at x evaluated on the same basis vectors, those in direction i scaled by −(q + 1).
Formal statement
Proof (Lean source)
ScaledProductBump 4 core · 18 supporting This module defines a normalized smooth product bump and proves bandwidth-uniform intrinsic Hölder-ball bounds for its translated, rescaled copies on the unit cube. ★ exists_scaledProductBump_holderBallOn
Smooth compactly supported product bumps on cubes
This module defines a normalized smooth product bump and proves bandwidth-uniform intrinsic Hölder-ball bounds for its translated, rescaled copies on the unit cube.
At a real input x, the normalized bump profile is e·exp(−1/(1 − x²)) for |x| < 1 and zero for |x| ≥ 1; it is smooth, supported in the interval from −1 to 1, and equals one at x = 0.
Definition (Lean source)
In dimension d, the product bump at a point x is the product over all coordinates i of the normalized bump profile evaluated at x_i.
Definition (Lean source)
In dimension d, with smoothness exponent β and bandwidth h and a center x₀, the scaled product bump at a point x is h^β times the product bump evaluated at (x − x₀)/h.
Definition (Lean source)
In dimension d, for a smoothness exponent β > 0, write m for the largest integer strictly below β and s = β − m, so 0 < s ≤ 1. Then there is a constant A > 0 such that for every baseline b, amplitude amp, bandwidth h with 0 < h ≤ 1 and center x₀, the function x ↦ b + amp·h^β·(product bump at (x − x₀)/h) lies in the intrinsic Hölder ball of order m, exponent s and radius |b| + |amp|·A on the unit cube of points with all coordinates between 0 and 1. The constant A does not depend on the baseline, amplitude, bandwidth or center.
Formal statement
Proof (Lean source)
18 supporting declarations (lemmas, instances)
-
bumpProfile_contDifftheorem — The normalized bump profile is smooth to every finite order.conclusion -
bumpProfile_zerotheorem — The normalized bump profile takes value one at zero.conclusionbumpProfile 0 = 1Proof (Lean source)
theorem bumpProfile_zero : bumpProfile 0 = 1 := by simp [bumpProfile, expNegInvGlue, Real.exp_neg, Real.exp_ne_zero] -
bumpProfile_eq_zero_of_one_le_abstheorem — When the real input has absolute value at least one, the normalized bump profile vanishes.Proof (Lean source)
theorem bumpProfile_eq_zero_of_one_le_abs {x : ℝ} (hx : 1 ≤ |x|) : bumpProfile x = 0 := by have hx2 : 1 ≤ x ^ 2 := by nlinarith [sq_nonneg (|x|), sq_abs x] simp [bumpProfile, expNegInvGlue.zero_of_nonpos (show 1 - x ^ 2 ≤ 0 by linarith)] -
productBump_contDifftheorem — In a finite dimension, the product bump is smooth to every finite order.Proof (Lean source)
theorem productBump_contDiff {d : ℕ} : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (productBump (d := d)) := by change ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : Fin d → ℝ => ∏ i : Fin d, bumpProfile (x i)) apply contDiff_prod intro i _ have hcoord : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : Fin d → ℝ => x i) := by fun_prop exact bumpProfile_contDiff.comp hcoord -
productBump_zerotheorem — In a finite dimension, the product bump takes value one at the origin.Proof (Lean source)
theorem productBump_zero {d : ℕ} : productBump (d := d) 0 = 1 := by simp [productBump, bumpProfile_zero] -
productBump_eq_zero_of_coordinatetheorem — In a finite dimension, when a point has a coordinate whose absolute value is at least one, the product bump vanishes.Proof (Lean source)
theorem productBump_eq_zero_of_coordinate {d : ℕ} (x : Fin d → ℝ) {i : Fin d} (hi : 1 ≤ |x i|) : productBump x = 0 := by exact Finset.prod_eq_zero (Finset.mem_univ i) (bumpProfile_eq_zero_of_one_le_abs hi) -
productBump_hasCompactSupporttheorem — In a finite dimension, the product bump has compact support.Proof (Lean source)
theorem productBump_hasCompactSupport {d : ℕ} : HasCompactSupport (productBump (d := d)) := by apply HasCompactSupport.intro (K := {x : Fin d → ℝ | ∀ i, x i ∈ Icc (-1) 1}) (isCompact_pi_infinite (fun _ => isCompact_Icc)) intro x hx have hcoord : ∃ i : Fin d, 1 ≤ |x i| := by simp only [Set.mem_ofPred_eq, Set.mem_Icc, not_forall] at hx obtain ⟨i, hi⟩ := hx refine ⟨i, ?_⟩ rcases not_and_or.mp hi with hi | hi · have h : x i ≤ -1 := le_of_lt (lt_of_not_ge hi) simpa [abs_of_nonpos (by linarith : x i ≤ 0)] using (neg_le_neg h) · have h : 1 ≤ x i := le_of_lt (lt_of_not_ge hi) simpa [abs_of_nonneg (by linarith : 0 ≤ x i)] using h obtain ⟨i, hi⟩ := hcoord exact productBump_eq_zero_of_coordinate x hi -
productBump_iteratedFDeriv_boundedtheorem — In a finite dimension, at a derivative order, the product bump has a finite global derivative bound.hypothesesd :ℕj :ℕconclusion∃ C : ℝ,0 ≤ CProof (Lean source)
theorem productBump_iteratedFDeriv_bounded {d : ℕ} (j : ℕ) : ∃ C : ℝ, 0 ≤ C ∧ ∀ x : Fin d → ℝ, ‖iteratedFDeriv ℝ j (productBump (d := d)) x‖ ≤ C := by have hprofile : ContDiff ℝ (j + 1 : ℕ) bumpProfile := by unfold bumpProfile have hinner : ContDiff ℝ (j + 1 : ℕ) (fun x : ℝ => 1 - x ^ 2) := by fun_prop exact contDiff_const.mul (expNegInvGlue.contDiff.comp hinner) have hproduct : ContDiff ℝ (j + 1 : ℕ) (productBump (d := d)) := by change ContDiff ℝ (j + 1 : ℕ) (fun x : Fin d → ℝ => ∏ i : Fin d, bumpProfile (x i)) apply contDiff_prod intro i _ have hcoord : ContDiff ℝ (j + 1 : ℕ) (fun x : Fin d → ℝ => x i) := by fun_prop exact hprofile.comp hcoord have hcontinuous : Continuous (iteratedFDeriv ℝ j (productBump (d := d))) := hproduct.continuous_iteratedFDeriv (by exact_mod_cast le_succ j) obtain ⟨C, hC⟩ := hcontinuous.bounded_above_of_compact_support (productBump_hasCompactSupport.iteratedFDeriv j) refine ⟨max C 0, le_max_right _ _, ?_⟩ intro x exact (hC x).trans (le_max_left _ _) -
scaledProductBump_eq_coordinate_divtheorem — In a finite dimension, with a smoothness exponent, a nonzero bandwidth, a center, and an evaluation point, the scaled bump has the coordinatewise-division representation.hypothesesconclusionscaledProductBump β h x₀ x = h ^ β * productBump (fun i => (x i - x₀ i) / h)Proof (Lean source)
theorem scaledProductBump_eq_coordinate_div {d : ℕ} (β : ℝ) {h : ℝ} (_hh : h ≠ 0) (x₀ x : Fin d → ℝ) : scaledProductBump β h x₀ x = h ^ β * productBump (fun i => (x i - x₀ i) / h) := by simp only [scaledProductBump] have harg : h⁻¹ • (x - x₀) = (fun i => (x i - x₀ i) / h) := by funext i simp [Pi.smul_apply, Pi.sub_apply, div_eq_mul_inv, mul_comm] rw [harg] -
scaledProductBump_contDifftheorem — In a finite dimension, for a smoothness exponent and bandwidth and a center, the scaled product bump is smooth to every finite order.hypothesesconclusionProof (Lean source)
theorem scaledProductBump_contDiff {d : ℕ} (β h : ℝ) (x₀ : Fin d → ℝ) : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (scaledProductBump β h x₀) := by unfold scaledProductBump have hinner : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : Fin d → ℝ => h⁻¹ • (x - x₀)) := by fun_prop exact contDiff_const.mul (productBump_contDiff.comp hinner) -
scaledProductBump_iteratedFDerivtheorem — In a finite dimension, at a derivative order, with a smoothness exponent and bandwidth, a center, and an evaluation point, the scaled bump derivative has the exact dilation formula.hypothesesconclusioniteratedFDeriv ℝ j (scaledProductBump β h x₀) x= (h ^ β) • ((h⁻¹) ^ j • iteratedFDeriv ℝ j (productBump (d := d)) (h⁻¹ • (x - x₀)))Proof (Lean source)
theorem scaledProductBump_iteratedFDeriv {d : ℕ} (j : ℕ) (β h : ℝ) (x₀ x : Fin d → ℝ) : iteratedFDeriv ℝ j (scaledProductBump β h x₀) x = (h ^ β) • ((h⁻¹) ^ j • iteratedFDeriv ℝ j (productBump (d := d)) (h⁻¹ • (x - x₀))) := by have hg : ContDiff ℝ (j : WithTop ℕ∞) (fun z : Fin d → ℝ => productBump (h⁻¹ • z)) := ((productBump_contDiff (d := d)).of_le (WithTop.coe_le_coe.mpr le_top)).comp (by fun_prop) have htrans : ContDiff ℝ (j : WithTop ℕ∞) (fun z : Fin d → ℝ => productBump (h⁻¹ • (z - x₀))) := hg.comp (by fun_prop) change iteratedFDeriv ℝ j (fun z : Fin d → ℝ => (h ^ β) • productBump (h⁻¹ • (z - x₀))) x = _ rw [iteratedFDeriv_const_smul_apply' htrans.contDiffAt] have ht := iteratedFDeriv_comp_sub (𝕜 := ℝ) (f := fun z : Fin d → ℝ => productBump (h⁻¹ • z)) j x₀ x rw [ht] rw [show iteratedFDeriv ℝ j (fun z : Fin d → ℝ => productBump (h⁻¹ • z)) = fun z => (h⁻¹) ^ j • iteratedFDeriv ℝ j (productBump (d := d)) (h⁻¹ • z) from iteratedFDeriv_comp_const_smul h⁻¹ ((productBump_contDiff (d := d)).of_le (WithTop.coe_le_coe.mpr le_top))] -
exists_productBump_top_modulustheorem — In a finite dimension, for a positive smoothness exponent, a nonnegative global Hölder coefficient for the normalized top derivative exists.hypothesesd :ℕβ :ℝhβ :0 < βProof (Lean source)
theorem exists_productBump_top_modulus {d : ℕ} (β : ℝ) (hβ : 0 < β) : let m := ⌈β⌉₊ - 1 let s := β - (m : ℝ) ∃ C : ℝ, 0 ≤ C ∧ ∀ x y : Fin d → ℝ, ‖iteratedFDeriv ℝ m (productBump (d := d)) x - iteratedFDeriv ℝ m (productBump (d := d)) y‖ ≤ C * ‖x - y‖ ^ s := by let m := ⌈β⌉₊ - 1 let s := β - (m : ℝ) have hmpos : 0 < ⌈β⌉₊ := Nat.ceil_pos.mpr hβ have hmadd : m + 1 = ⌈β⌉₊ := Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr (by omega)) have hmlt : (m : ℝ) < β := Nat.lt_ceil.mp (by omega : m < ⌈β⌉₊) have hs : 0 < s := by dsimp [s]; linarith have hs1 : s ≤ 1 := by have hceil := Nat.le_ceil β have hcast : (m : ℝ) + 1 = (⌈β⌉₊ : ℝ) := by exact_mod_cast hmadd dsimp [s] linarith obtain ⟨B, hB0, hB⟩ := productBump_iteratedFDeriv_bounded (d := d) m obtain ⟨L, hL0, hL⟩ := productBump_iteratedFDeriv_bounded (d := d) (m + 1) let A := max B L have hA0 : 0 ≤ A := le_trans hB0 (le_max_left B L) refine ⟨2 * A, by positivity, ?_⟩ intro x y let f := iteratedFDeriv ℝ m (productBump (d := d)) have hdiff : ∀ z : Fin d → ℝ, DifferentiableAt ℝ f z := by intro z exact (productBump_contDiff (d := d)).contDiffAt.differentiableAt_iteratedFDeriv (by exact_mod_cast (show (m : ℕ∞) < ⊤ from by simp)) have hlip : ‖f x - f y‖ ≤ A * ‖x - y‖ := by have hmv := Convex.norm_image_sub_le_of_norm_fderiv_le (s := univ) (x := y) (y := x) (f := f) (C := A) (fun z _ => hdiff z) (by intro z _ rw [norm_fderiv_iteratedFDeriv] exact (hL z).trans (le_max_right B L)) convex_univ (Set.mem_univ _) (Set.mem_univ _) simpa using hmv by_cases hsmall : ‖x - y‖ ≤ 1 · have hpow : ‖x - y‖ ≤ ‖x - y‖ ^ s := Real.self_le_rpow_of_le_one (norm_nonneg _) hsmall hs1 calc ‖f x - f y‖ ≤ A * ‖x - y‖ := hlip _ ≤ A * ‖x - y‖ ^ s := mul_le_mul_of_nonneg_left hpow hA0 _ ≤ (2 * A) * ‖x - y‖ ^ s := by have := Real.rpow_nonneg (norm_nonneg (x - y)) s nlinarith · have hpow : 1 ≤ ‖x - y‖ ^ s := Real.one_le_rpow (le_of_lt (lt_of_not_ge hsmall)) hs.le calc ‖f x - f y‖ ≤ ‖f x‖ + ‖f y‖ := norm_sub_le _ _ _ ≤ 2 * A := by have hx := (hB x).trans (le_max_left B L) have hy := (hB y).trans (le_max_left B L) dsimp [f] at * linarith _ ≤ (2 * A) * ‖x - y‖ ^ s := by nlinarith -
exists_scaledProductBump_deriv_boundtheorem — In a finite dimension, for a positive smoothness exponent, a nonnegative derivative bound uniform over admissible scaled bumps exists.hypothesesd :ℕβ :ℝhβ :0 < βconclusionm :⌈β⌉₊ - 1∃ C : ℝ,0 ≤ Cconclusion 1‖iteratedFDeriv ℝ j (scaledProductBump β h x₀) x‖ ≤ CProof (Lean source)
theorem exists_scaledProductBump_deriv_bound {d : ℕ} (β : ℝ) (hβ : 0 < β) : let m := ⌈β⌉₊ - 1 ∃ C : ℝ, 0 ≤ C ∧ ∀ (h : ℝ), 0 < h → h ≤ 1 → ∀ (x₀ : Fin d → ℝ) (j : ℕ), j ≤ m → ∀ x : Fin d → ℝ, ‖iteratedFDeriv ℝ j (scaledProductBump β h x₀) x‖ ≤ C := by let m := ⌈β⌉₊ - 1 have hmpos : 0 < ⌈β⌉₊ := Nat.ceil_pos.mpr hβ have hmlt : (m : ℝ) < β := Nat.lt_ceil.mp (by omega : m < ⌈β⌉₊) let D : ℕ → ℝ := fun j => (productBump_iteratedFDeriv_bounded (d := d) j).choose have hD0 : ∀ j, 0 ≤ D j := fun j => (productBump_iteratedFDeriv_bounded (d := d) j).choose_spec.1 have hD : ∀ j x, ‖iteratedFDeriv ℝ j (productBump (d := d)) x‖ ≤ D j := fun j x => (productBump_iteratedFDeriv_bounded (d := d) j).choose_spec.2 x let C := ∑ j ∈ range (m + 1), D j have hC0 : 0 ≤ C := Finset.sum_nonneg (fun j _ => hD0 j) refine ⟨C, hC0, ?_⟩ intro h hh hh1 x₀ j hj x have hh0 : h ≠ 0 := ne_of_gt hh have hjβ : (j : ℝ) ≤ β := by have hjm : (j : ℝ) ≤ m := Nat.cast_le.mpr hj linarith have hscale : h ^ β * (h⁻¹) ^ j ≤ 1 := by have hp : h ^ β ≤ h ^ (j : ℝ) := Real.rpow_le_rpow_of_exponent_ge' hh.le hh1 (Nat.cast_nonneg j) hjβ calc h ^ β * (h⁻¹) ^ j ≤ h ^ (j : ℝ) * (h⁻¹) ^ j := mul_le_mul_of_nonneg_right hp (pow_nonneg (inv_nonneg.mpr hh.le) j) _ = 1 := by rw [Real.rpow_natCast, ← mul_pow, mul_inv_cancel₀ hh0, one_pow] have hjC : D j ≤ C := Finset.single_le_sum (fun i _ => hD0 i) (by simpa only [Finset.mem_range] using (Nat.lt_succ_of_le (show j ≤ m from hj))) rw [scaledProductBump_iteratedFDeriv] rw [norm_smul, norm_smul, Real.norm_eq_abs, Real.norm_eq_abs, abs_pow, abs_inv, abs_of_pos hh, abs_of_nonneg (Real.rpow_nonneg hh.le β)] calc h ^ β * ((h⁻¹) ^ j * ‖iteratedFDeriv ℝ j (productBump (d := d)) _‖) ≤ (h ^ β * (h⁻¹) ^ j) * D j := by calc _ ≤ h ^ β * ((h⁻¹) ^ j * D j) := by gcongr exact hD j _ _ = _ := by ring _ ≤ D j := by nlinarith [hD0 j] _ ≤ C := hjC -
exists_scaledProductBump_top_modulustheorem — In a finite dimension, for a positive smoothness exponent, a nonnegative global Hölder coefficient uniform over admissible scaled bumps exists.hypothesesd :ℕβ :ℝhβ :0 < βconclusionm :⌈β⌉₊ - 1s :β - (m : ℝ)∃ C : ℝ,0 ≤ Cconclusion 1≤ C * ‖x - y‖ ^ sProof (Lean source)
theorem exists_scaledProductBump_top_modulus {d : ℕ} (β : ℝ) (hβ : 0 < β) : let m := ⌈β⌉₊ - 1 let s := β - (m : ℝ) ∃ C : ℝ, 0 ≤ C ∧ ∀ (h : ℝ), 0 < h → h ≤ 1 → ∀ (x₀ x y : Fin d → ℝ), ‖iteratedFDeriv ℝ m (scaledProductBump β h x₀) x - iteratedFDeriv ℝ m (scaledProductBump β h x₀) y‖ ≤ C * ‖x - y‖ ^ s := by let m := ⌈β⌉₊ - 1 let s := β - (m : ℝ) obtain ⟨C, hC0, hC⟩ := exists_productBump_top_modulus (d := d) β hβ refine ⟨C, hC0, ?_⟩ intro h hh hh1 x₀ x y have hh0 : h ≠ 0 := ne_of_gt hh let u : Fin d → ℝ := h⁻¹ • (x - x₀) let v : Fin d → ℝ := h⁻¹ • (y - x₀) have hdist : ‖u - v‖ = ‖x - y‖ / h := by have heq : u - v = h⁻¹ • (x - y) := by dsimp [u, v] rw [← smul_sub] congr 1 abel rw [heq, norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hh] exact inv_mul_eq_div _ _ have hcancel : h ^ β * (h⁻¹) ^ m * (‖x - y‖ / h) ^ s = ‖x - y‖ ^ s := by rw [Real.div_rpow (norm_nonneg _) hh.le, div_eq_mul_inv] have hp : h ^ β * (h⁻¹) ^ m * (h ^ s)⁻¹ = 1 := by rw [inv_pow, ← Real.rpow_natCast, ← Real.rpow_neg hh.le, ← Real.rpow_neg hh.le, ← Real.rpow_add hh, ← Real.rpow_add hh] have hexp : β + -(m : ℝ) + -s = 0 := by dsimp [s]; ring rw [hexp, Real.rpow_zero] calc h ^ β * (h⁻¹) ^ m * (‖x - y‖ ^ s * (h ^ s)⁻¹) = (h ^ β * (h⁻¹) ^ m * (h ^ s)⁻¹) * ‖x - y‖ ^ s := by ring _ = ‖x - y‖ ^ s := by rw [hp, one_mul] rw [scaledProductBump_iteratedFDeriv, scaledProductBump_iteratedFDeriv] rw [← smul_sub, ← smul_sub, norm_smul, norm_smul, Real.norm_eq_abs, Real.norm_eq_abs, abs_pow, abs_inv, abs_of_pos hh, abs_of_nonneg (Real.rpow_nonneg hh.le β)] have htop := hC u v change ‖iteratedFDeriv ℝ m (productBump (d := d)) u - iteratedFDeriv ℝ m (productBump (d := d)) v‖ ≤ C * ‖u - v‖ ^ s at htop change h ^ β * ((h⁻¹) ^ m * ‖iteratedFDeriv ℝ m (productBump (d := d)) u - iteratedFDeriv ℝ m (productBump (d := d)) v‖) ≤ C * ‖x - y‖ ^ s calc _ ≤ h ^ β * ((h⁻¹) ^ m * (C * ‖u - v‖ ^ s)) := by gcongr _ = C * ‖x - y‖ ^ s := by rw [hdist]; rw [← hcancel]; ring -
coordJetOn_unitCube_eq_ambienttheorem — In a finite dimension and derivative order, when a response is globally smooth, a requested coordinate direction list at a point in the unit cube has an intrinsic coordinate jet equal to the ambient iterated derivative.hypothesesconclusioncoordJetOn (unitCube d) j u f x= iteratedFDeriv ℝ j u x (fun k => single (f k) (1 : ℝ))Proof (Lean source)
theorem coordJetOn_unitCube_eq_ambient {d j : ℕ} {u : (Fin d → ℝ) → ℝ} (hu : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) u) (f : Fin j → Fin d) (x : Fin d → ℝ) (hx : x ∈ unitCube d) : coordJetOn (unitCube d) j u f x = iteratedFDeriv ℝ j u x (fun k => single (f k) (1 : ℝ)) := by have huniq : UniqueDiffOn ℝ (unitCube d) := by unfold unitCube exact UniqueDiffOn.pi (fun _ _ => uniqueDiffOn_Icc (by norm_num)) unfold coordJetOn rw [iteratedFDerivWithin_eq_iteratedFDeriv huniq (hu.contDiffAt.of_le (by exact_mod_cast le_top)) hx] -
holderBallOn_unitCube_of_ambient_boundstheorem — In a finite dimension, derivative order, exponent, and radius, when a response is globally smooth, has uniform derivative bounds, and has a top-derivative Hölder modulus, it belongs to the same-radius intrinsic Hölder ball on the unit cube.hypothesesd m :ℕs R :ℝu :(Fin d → ℝ) → ℝhbound :∀ j ≤ m, ∀ x : Fin d → ℝ, ‖iteratedFDeriv ℝ j u x‖ ≤ Rhmod :∀ x y : Fin d → ℝ, ‖iteratedFDeriv ℝ m u x - iteratedFDeriv ℝ m u y‖ ≤ R * ‖x - y‖ ^ sconclusionHolderBallOn (unitCube d) m s R uProof (Lean source)
theorem holderBallOn_unitCube_of_ambient_bounds {d m : ℕ} {s R : ℝ} {u : (Fin d → ℝ) → ℝ} (hu : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) u) (hbound : ∀ j ≤ m, ∀ x : Fin d → ℝ, ‖iteratedFDeriv ℝ j u x‖ ≤ R) (hmod : ∀ x y : Fin d → ℝ, ‖iteratedFDeriv ℝ m u x - iteratedFDeriv ℝ m u y‖ ≤ R * ‖x - y‖ ^ s) : HolderBallOn (unitCube d) m s R u := by have hcoord (j : ℕ) (f : Fin j → Fin d) : ‖(fun k => single (f k) (1 : ℝ) : Fin j → (Fin d → ℝ))‖ ≤ 1 := by apply (pi_norm_le_iff_of_nonneg (by norm_num)).2 intro k simp [Pi.norm_single] refine ⟨hu.contDiffOn.of_le (by exact_mod_cast le_top), ?_, ?_⟩ · intro j hj f x hx rw [coordJetOn_unitCube_eq_ambient hu f x hx, ← Real.norm_eq_abs] exact (ContinuousMultilinearMap.unit_le_opNorm _ (hcoord j f)).trans (hbound j hj x) · intro f x hx y hy rw [coordJetOn_unitCube_eq_ambient hu f x hx, coordJetOn_unitCube_eq_ambient hu f y hy, ← Real.norm_eq_abs] have heval : iteratedFDeriv ℝ m u x (fun k => single (f k) (1 : ℝ)) - iteratedFDeriv ℝ m u y (fun k => single (f k) (1 : ℝ)) = (iteratedFDeriv ℝ m u x - iteratedFDeriv ℝ m u y) (fun k => single (f k) (1 : ℝ)) := rfl rw [heval] exact (ContinuousMultilinearMap.unit_le_opNorm _ (hcoord m f)).trans (hmod x y) -
holderBallOn_unitCube_add_const_multheorem — In [a finite dimension, derivative order, exponent, and nonnegative radius] (hyp:d,m,s,R), the radius is nonnegative, and a response belongs to the intrinsic unit-cube Hölder ball with that radius and a baseline and amplitude are chosen, the affine response belongs to the stated enlarged Hölder ball.hypothesesconclusionHolderBallOn (unitCube d) m s (|b| + |amp| * R) (fun x => b + amp * u x)Proof (Lean source)
theorem holderBallOn_unitCube_add_const_mul {d m : ℕ} {s R : ℝ} {u : (Fin d → ℝ) → ℝ} (_hR : 0 ≤ R) (hu : HolderBallOn (unitCube d) m s R u) (b amp : ℝ) : HolderBallOn (unitCube d) m s (|b| + |amp| * R) (fun x => b + amp * u x) := by have huniq : UniqueDiffOn ℝ (unitCube d) := by unfold unitCube exact UniqueDiffOn.pi (fun _ _ => uniqueDiffOn_Icc (by norm_num)) have hjet (j : ℕ) (hj : j ≤ m) (f : Fin j → Fin d) (x : Fin d → ℝ) (hx : x ∈ unitCube d) : coordJetOn (unitCube d) j (fun z => b + amp * u z) f x = (if j = 0 then b else 0) + amp * coordJetOn (unitCube d) j u f x := by have hreg : ContDiffWithinAt ℝ j u (unitCube d) x := (hu.regularity x hx).of_le (by exact_mod_cast hj) unfold coordJetOn change iteratedFDerivWithin ℝ j ((fun _ : Fin d → ℝ => b) + (fun y => amp • u y)) (unitCube d) x _ = _ rw [iteratedFDerivWithin_add_apply contDiffWithinAt_const (hreg.const_smul amp) huniq hx] change ((iteratedFDerivWithin ℝ j (fun _ : Fin d → ℝ => b) (unitCube d) x + iteratedFDerivWithin ℝ j (amp • u) (unitCube d) x) _) = _ rw [iteratedFDerivWithin_const_smul_apply hreg huniq hx] simp only [add_apply, smul_apply, smul_eq_mul] by_cases hj0 : j = 0 · subst j simp [iteratedFDerivWithin_zero_apply] · rw [iteratedFDerivWithin_const_of_ne hj0] simp [hj0] have hregularity : ContDiffOn ℝ m (fun x => b + amp * u x) (unitCube d) := by have hc : ContDiffOn ℝ m (fun _ : Fin d → ℝ => b) (unitCube d) := contDiffOn_const simpa only [Pi.add_apply, Pi.smul_apply, smul_eq_mul] using hc.add (ContDiffOn.const_smul amp hu.regularity) refine ⟨hregularity, ?_, ?_⟩ · intro j hj f x hx rw [hjet j hj f x hx] have hc : |if j = 0 then b else 0| ≤ |b| := by split_ifs <;> simp calc |(if j = 0 then b else 0) + amp * coordJetOn (unitCube d) j u f x| ≤ |if j = 0 then b else 0| + |amp * coordJetOn (unitCube d) j u f x| := abs_add_le _ _ _ ≤ |b| + |amp| * R := by rw [abs_mul] gcongr exact hu.derivBound j hj f x hx · intro f x hx y hy rw [hjet m le_rfl f x hx, hjet m le_rfl f y hy] have heq : (if m = 0 then b else 0) + amp * coordJetOn (unitCube d) m u f x - ((if m = 0 then b else 0) + amp * coordJetOn (unitCube d) m u f y) = amp * (coordJetOn (unitCube d) m u f x - coordJetOn (unitCube d) m u f y) := by ring rw [heq, abs_mul] calc |amp| * |coordJetOn (unitCube d) m u f x - coordJetOn (unitCube d) m u f y| ≤ |amp| * (R * ‖x - y‖ ^ s) := mul_le_mul_of_nonneg_left (hu.modulus f x hx y hy) (abs_nonneg amp) _ = (|amp| * R) * ‖x - y‖ ^ s := by ring _ ≤ (|b| + |amp| * R) * ‖x - y‖ ^ s := mul_le_mul_of_nonneg_right (le_add_of_nonneg_left (abs_nonneg b)) (Real.rpow_nonneg (norm_nonneg _) _) -
exists_uniform_scaledProductBump_holderBallOntheorem — In a finite dimension, for a positive smoothness exponent, a positive Hölder radius independent of bandwidth and center controls every admissible scaled product bump on the unit cube.hypothesesd :ℕβ :ℝhβ :0 < βconclusionm :⌈β⌉₊ - 1s :β - (m : ℝ)∃ A : ℝ,0 < Aconclusion 1HolderBallOn (unitCube d) m s A (scaledProductBump β h x₀)Proof (Lean source)
theorem exists_uniform_scaledProductBump_holderBallOn {d : ℕ} (β : ℝ) (hβ : 0 < β) : let m := ⌈β⌉₊ - 1 let s := β - (m : ℝ) ∃ A : ℝ, 0 < A ∧ ∀ (h : ℝ), 0 < h → h ≤ 1 → ∀ x₀ : Fin d → ℝ, HolderBallOn (unitCube d) m s A (scaledProductBump β h x₀) := by obtain ⟨D, _hD0, hD⟩ := exists_scaledProductBump_deriv_bound (d := d) β hβ obtain ⟨M, _hM0, hM⟩ := exists_scaledProductBump_top_modulus (d := d) β hβ let A := max 1 (max D M) have hDA : D ≤ A := (le_max_left D M).trans (le_max_right 1 (max D M)) have hMA : M ≤ A := (le_max_right D M).trans (le_max_right 1 (max D M)) refine ⟨A, lt_of_lt_of_le (by norm_num) (le_max_left 1 (max D M)), ?_⟩ intro h hh hh1 x₀ apply holderBallOn_unitCube_of_ambient_bounds (scaledProductBump_contDiff β h x₀) · intro j hj x exact (hD h hh hh1 x₀ j hj x).trans hDA · intro x y exact (hM h hh hh1 x₀ x y).trans (mul_le_mul_of_nonneg_right hMA (Real.rpow_nonneg (norm_nonneg _) _))
Scaling 1 core · 2 supporting The generic amplitude and dilation calculus specializes to the odd coordinate product, its Euclidean version, and the tangent product with complementary radial plateau. ★ mixedProfile_uniform_scaled_bounds
Uniform bandwidth bounds for exact coordinate and mixed profiles
The generic amplitude and dilation calculus specializes to the odd coordinate product, its Euclidean version, and the tangent product with complementary radial plateau. Each constant is independent of bandwidth, exponent, and center.
For every tangent dimension t and complementary dimension c there is a constant C ≥ 1 such that for every exponent β with 0 < β ≤ 2, every bandwidth h with 0 < h ≤ 1 and every center z, the scaled copy x ↦ h^β·(mixed profile at (x − z)/h) is twice continuously differentiable on the whole space, with absolute value at most C·h^β, derivative of operator norm at most C·h^(β−1) and second derivative of operator norm at most C·h^(β−2) at every point. The constant does not depend on the exponent, bandwidth or center.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
oddProduct_uniform_scaled_boundstheorem — In dimension, one fixed constant bounds all scaled coordinate odd-product jets, uniformly over exponents in (0,2], bandwidths in (0,1], and centers.hypothesesd :ℕconclusion∃ C : ℝ,1 ≤ Cconclusion 1Proof (Lean source)
theorem oddProduct_uniform_scaled_bounds (d : ℕ) : ∃ C : ℝ, 1 ≤ C ∧ ∀ (β h : ℝ), 0 < β → β ≤ 2 → 0 < h → h ≤ 1 → ∀ z : Fin d → ℝ, ScaledJetBounds β h (scaledCopy β h z oddProduct) C := by obtain ⟨C, hC, hf⟩ := oddProduct_jetBounds d exact ⟨C, hC, fun β h _ _ hh _ z => scaledCopy_jetBounds β h z hf hh⟩ -
oddEuclidean_uniform_scaled_boundstheorem — In dimension, one fixed constant bounds all scaled Euclidean odd-product jets, uniformly over exponents in (0,2], bandwidths in (0,1], and centers.hypothesesd :ℕconclusion∃ C : ℝ,1 ≤ Cconclusion 1Proof (Lean source)
theorem oddEuclidean_uniform_scaled_bounds (d : ℕ) : ∃ C : ℝ, 1 ≤ C ∧ ∀ (β h : ℝ), 0 < β → β ≤ 2 → 0 < h → h ≤ 1 → ∀ z : EuclideanSpace ℝ (Fin d), ScaledJetBounds β h (scaledCopy β h z oddEuclidean) C := by obtain ⟨C, hC, hf⟩ := oddEuclidean_jetBounds d exact ⟨C, hC, fun β h _ _ hh _ z => scaledCopy_jetBounds β h z hf hh⟩
ZeroDimensional 1 core · 0 supporting The cube in a zero-dimensional space is a singleton, so its data already have a constant global representative with the required uniform bounds. ★ exists_global_holder_extension_zero
Intrinsic cube extension in dimension zero
The cube in a zero-dimensional space is a singleton, so its data already have a constant global representative with the required uniform bounds.
For any derivative order m and any exponent s, there is a positive constant A such that, in dimension zero, every response u in the intrinsic Hölder ball of order m, exponent s and radius L ≥ 0 on the cube has a global extension U that agrees with u on the cube, is m times continuously differentiable, has derivatives of every order at most m bounded in operator norm by A·L, and whose order-m derivative is s-Hölder with coefficient A·L.
Formal statement
Proof (Lean source)
ZeroOrder 1 core · 0 supporting A function on the cube [−1,1]^d that is bounded and s-Hölder with exponent s ∈ (0, 1] and radius L extends to a continuous function on all of ℝ^d that agrees with it on the cube, is bounded by A·L and is s-Hölder with co ★ exists_global_holder_extension_order_zero
Global Hölder extension from the cube at derivative order zero
A function on the cube [−1,1]^d that is bounded and s-Hölder with exponent s ∈ (0, 1] and radius L extends to a continuous function on all of ℝ^d that agrees with it on the cube, is bounded by A·L and is s-Hölder with constant A·L, where A depends only on d and s. The extension is the function composed with the coordinatewise clamping of a point to the cube.
Main results
* exists_global_holder_extension_order_zero — the order-zero extension with controlled sup norm
and Hölder constant.
In dimension d, for a Hölder exponent s with 0 < s, there is a positive constant A such that every response u in the intrinsic order-zero Hölder ball of exponent s and radius L ≥ 0 on the normalized cube has a continuous global representative U that agrees with u on the cube, is bounded in absolute value by A·L everywhere, and is s-Hölder with coefficient A·L on the whole space.