Slicing is Lipschitz in the slice parameter

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #123, out of #121(i).

★★★ SchwartzMap.lipschitz_seminorm_slice — each Schwartz seminorm of slice K e − slice K e₀ is at most ‖e − e₀‖ times one seminorm of K, so ★★★ SchwartzMap.continuous_slice: the slice family e ↦ slice K e is continuous into 𝓢(F, G) for the Schwartz topology. #121(i) proved slicing continuous in the kernel (sliceCLM is a continuous linear map for each fixed e), which is what transfers theorems; this is the other direction, and the row recorded it as a genuinely different statement. It is.

The route the row recorded, and what it cost

• ★★ iteratedFDeriv_comp_inr — the derivatives of a slice are the kernel's derivatives precomposed with the inclusion w ↦ (e, w). This is the mirror of #126(ii)'s iteratedFDeriv_comp_inl and was the first of the two pieces the row named as needed;
• ★★ norm_fderiv_iteratedFDeriv_comp_inl_le — the second: e ↦ ∂ⁿK(e, w) is differentiable with derivative bounded by ‖∂ⁿ⁺¹K(e, w)‖, which is K's decay at one order higher, exactly as the row predicted;
• ★★★ lipschitz_seminorm_slice — the mean value inequality, with the weight handled by a case split on whether it vanishes. Weighting the map before the mean value step is the mathematically natural move — the derivative bound ‖w‖ᵏ‖∂ⁿ⁺¹K(u, w)‖ ≤ 𝒮_{k,n+1}(K) is then uniform in both variables — but it puts a scalar smul on a space of continuous multilinear maps, where the NormSMulClass instance the norm computation needs is absent at this pin. The case split costs two lines and needs no instances.

The row said "locally Lipschitz"; it is globally Lipschitz. The derivative bound is a seminorm of K, which does not depend on the base point, so no localisation is needed and the estimate holds between any two parameters.

Honest scope

⚠️ Nothing is gated on this. The row records it because #121(i) names it and because a symbol-valued calculus would want it; #121(ii) goes by #124 alone. It is here because it was unblocked, not because something waits on it.

⚠️ Not a curry. As #123 was corrected on 2026-10-07, 𝓢(E, 𝓢(F, G)) does not typecheck — SchwartzMap needs a normed target and Schwartz space is Fréchet — so this is a continuity statement about one map, with no larger object behind it. In particular the slice family is not claimed to be a Schwartz function of e, which would need every derivative in e and a weight, and is a different statement.

⚠️ Lipschitz in each seminorm, not for a norm. 𝓢(F, G) has no norm; the conclusion is the seminorm-wise estimate and the continuity it gives, not LipschitzWith.

References: SchwartzSlice.lean (#121(i), slice, sliceCLM), SchwartzPartialIntegral.lean (#126(ii), iteratedFDeriv_comp_inl, whose mirror this is); specs/BACKLOG.md #123, #121.

The derivatives of a slice

theorem SchwartzMap.iteratedFDeriv_comp_inr {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {K : E × F → G} (hK : ContDiff ℝ (↑⊤) K) (e : E) (k : ℕ) (w : F) : iteratedFDeriv ℝ k (fun (v : F) => K (e, v)) w = (iteratedFDeriv ℝ k K (e, w)).compContinuousLinearMap fun (x : Fin k) => ContinuousLinearMap.inr ℝ E F

★★ The iterated chain rule through the slice inclusion w ↦ (e, w) — the mirror of #126(ii)'s iteratedFDeriv_comp_inl, and the first piece #123 named.

theorem SchwartzMap.norm_inr_le_one {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖ContinuousLinearMap.inr ℝ E F‖ ≤ 1

The slice inclusion is short, so no power of it appears in any bound.

Differentiating in the parameter

theorem SchwartzMap.norm_inl_le_one' {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖ContinuousLinearMap.inl ℝ E F‖ ≤ 1

The inclusion of the first factor is short too.

theorem SchwartzMap.norm_fderiv_iteratedFDeriv_comp_inl_le {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {K : E × F → G} (hK : ContDiff ℝ (↑⊤) K) (n : ℕ) (e : E) (w : F) : ‖fderiv ℝ (fun (u : E) => iteratedFDeriv ℝ n K (u, w)) e‖ ≤ ‖iteratedFDeriv ℝ (n + 1) K (e, w)‖

★★ The second piece #123 named: the kernel's n-th derivative is differentiable in the parameter, with derivative bounded by its (n+1)-st — K's decay at one order higher.

The Lipschitz estimate

theorem SchwartzMap.norm_pow_mul_norm_iteratedFDeriv_slice_sub_le {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace ℂ G] [SMulCommClass ℝ ℂ G] (K : SchwartzMap (E × F) G) (k n : ℕ) (e₀ e : E) (w : F) : ‖w‖ ^ k * ‖iteratedFDeriv ℝ n (⇑(K.slice e - K.slice e₀)) w‖ ≤ (SchwartzMap.seminorm ℂ k (n + 1)) K * ‖e - e₀‖

★★★ Each seminorm of the slice difference is ‖e − e₀‖ times one seminorm of the kernel — the kernel's, at one order higher in the derivative. The mean value inequality is applied to the weighted map u ↦ ‖w‖ᵏ·∂ⁿK(u, w), whose derivative bound ‖w‖ᵏ‖∂ⁿ⁺¹K(u, w)‖ ≤ 𝒮_{k,n+1}(K) is uniform in both u and w; weighting afterwards would have forced a division by ‖w‖ᵏ.

theorem SchwartzMap.lipschitz_seminorm_slice {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace ℂ G] [SMulCommClass ℝ ℂ G] (K : SchwartzMap (E × F) G) (k n : ℕ) (e₀ e : E) : (SchwartzMap.seminorm ℂ k n) (K.slice e - K.slice e₀) ≤ (SchwartzMap.seminorm ℂ k (n + 1)) K * ‖e - e₀‖

★★★ The seminorm-wise Lipschitz estimate. Each Schwartz seminorm of the slice difference is at most ‖e − e₀‖ times one seminorm of the kernel, the same one at one order higher. The row said "locally Lipschitz"; the bound does not depend on the base point, so it is globally Lipschitz.

theorem SchwartzMap.continuous_slice {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace ℂ G] [SMulCommClass ℝ ℂ G] (K : SchwartzMap (E × F) G) : Continuous fun (e : E) => K.slice e

★★★ Slicing is continuous in the slice parameter for the Schwartz topology — #123's statement. It falls straight out of the Lipschitz estimate, since a seminorm of the difference is bounded by a constant times ‖e − e₀‖.