Splicing two maps with a cutoff along a linear functional

Let k l : X → Y be maps between real normed spaces, π : X →L[ℝ] ℝ a continuous linear functional and δ > 0 a scale. The splice TauCeti.spliceAlong π k l δ is the convex combination x ↦ k x + χ (δ⁻¹ π x) • (l x - k x), where χ = TauCeti.spliceCutoff is a fixed smooth cutoff which is 1 on [-1, 1], vanishes off (-2, 2) and takes values in [0, 1]. It is l where |π x| ≤ δ and k where 2 δ ≤ |π x|, it stays in every convex set containing the values of k and l, and it is as smooth as k and l.

The derivative of the splice is controlled uniformly in the scale. Suppose ‖π‖ ≤ 1. If the derivatives of k and l at x are within ε of a linear map A, and ‖l x - k x‖ ≤ 2 ε |π x|, then the splice has derivative within (3 + 4 B) ε of A at x, where B bounds the derivative of the cutoff (TauCeti.exists_hasFDerivAt_spliceAlong_sub_le). The hypothesis on l x - k x holds by the mean value inequality when the two maps agree at a point y with ‖x - y‖ = |π x| (Convex.norm_sub_le_of_norm_hasFDerivWithin_sub_le in TauCeti.Analysis.Calculus.MeanValue); the derivative δ⁻¹ χ' (δ⁻¹ π x) • π of the cutoff has norm at most δ⁻¹ B ‖π‖ ≤ δ⁻¹ B, but only meets l x - k x where |π x| ≤ 2 δ.

This is the device used to straighten an embedding near a point or a line: there the two maps are the embedding and a model agreeing with it to first order, read in a chart.

Main definitions

• TauCeti.spliceCutoff: the fixed smooth cutoff on the line.
• TauCeti.spliceAlong: the splice of two maps along a linear functional at a given scale.

Main results

• TauCeti.spliceAlong_of_abs_le, TauCeti.spliceAlong_of_le_abs: the splice is l near the kernel of π and k away from it.
• TauCeti.spliceAlong_mem, TauCeti.contDiffOn_spliceAlong: convexity and smoothness.
• TauCeti.exists_hasFDerivAt_spliceAlong_sub_le: the uniform derivative estimate.
• TauCeti.injOn_and_injective_fderiv_spliceAlong_fst: injectivity and injective derivative for splices across a strip whose derivatives stay close to a linear map with a left inverse.

The cutoff

noncomputable def TauCeti.spliceCutoff : ℝ → ℝ

A fixed smooth cutoff on the line: it is 1 on [-1, 1], vanishes off (-2, 2), and takes values in [0, 1].

@[simp]

theorem TauCeti.spliceCutoff_eq_one {x : ℝ} (hx : |x| ≤ 1) : spliceCutoff x = 1

The cutoff is 1 on [-1, 1].

@[simp]

theorem TauCeti.spliceCutoff_eq_zero {x : ℝ} (hx : 2 ≤ |x|) : spliceCutoff x = 0

The cutoff vanishes off (-2, 2).

theorem TauCeti.spliceCutoff_nonneg (x : ℝ) : 0 ≤ spliceCutoff x

The cutoff is nonnegative.

theorem TauCeti.spliceCutoff_le_one (x : ℝ) : spliceCutoff x ≤ 1

The cutoff is at most 1.

theorem TauCeti.contDiff_spliceCutoff {n : ℕ∞} : ContDiff ℝ (↑n) spliceCutoff

The cutoff is smooth.

@[simp]

theorem TauCeti.deriv_spliceCutoff_eq_zero {x : ℝ} (hx : 2 < |x|) : deriv spliceCutoff x = 0

The derivative of the cutoff vanishes off [-2, 2].

theorem TauCeti.exists_abs_deriv_spliceCutoff_le : ∃ (B : ℝ), ∀ (x : ℝ), |deriv spliceCutoff x| ≤ B

The derivative of the cutoff is bounded, since it is continuous with compact support.

The splice

noncomputable def TauCeti.spliceAlong {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (π : X →L[ℝ] ℝ) (k l : X → Y) (δ : ℝ) (x : X) : Y

The map k with its values near the kernel of π replaced by those of l: the convex combination of k x and l x with weight the cutoff spliceCutoff at scale δ along π. It is l where |π x| ≤ δ and k where 2 δ ≤ |π x|.

theorem TauCeti.spliceAlong_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {π : X →L[ℝ] ℝ} {k l : X → Y} {δ : ℝ} {x : X} : spliceAlong π k l δ x = k x + spliceCutoff (δ⁻¹ * π x) • (l x - k x)

The value of the spliced map at a point.

@[simp]

theorem TauCeti.spliceAlong_of_le_abs {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {π : X →L[ℝ] ℝ} {k l : X → Y} {δ : ℝ} {x : X} (hδ : 0 < δ) (hx : 2 * δ ≤ |π x|) : spliceAlong π k l δ x = k x

Where 2 δ ≤ |π x|, the spliced map is k.

@[simp]

theorem TauCeti.spliceAlong_of_abs_le {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {π : X →L[ℝ] ℝ} {k l : X → Y} {δ : ℝ} {x : X} (hδ : 0 < δ) (hx : |π x| ≤ δ) : spliceAlong π k l δ x = l x

Where |π x| ≤ δ, the spliced map is l.

@[simp]

theorem TauCeti.spliceAlong_of_eq {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {π : X →L[ℝ] ℝ} {k l : X → Y} {δ : ℝ} {x : X} (hx : k x = l x) : spliceAlong π k l δ x = k x

Where k and l agree, the spliced map is their common value.

theorem TauCeti.spliceAlong_mem {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {π : X →L[ℝ] ℝ} {k l : X → Y} {δ : ℝ} {x : X} {S : Set Y} (hS : Convex ℝ S) (hk : k x ∈ S) (hl : l x ∈ S) : spliceAlong π k l δ x ∈ S

The spliced map is a convex combination of the two maps, so it stays in any convex set containing both values.

theorem TauCeti.contDiffOn_spliceAlong {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {k l : X → Y} {n : ℕ∞} {W : Set X} (hk : ContDiffOn ℝ (↑n) k W) (hl : ContDiffOn ℝ (↑n) l W) (π : X →L[ℝ] ℝ) (δ : ℝ) : ContDiffOn ℝ (↑n) (spliceAlong π k l δ) W

The spliced map is as smooth as the two maps.

theorem TauCeti.hasFDerivAt_spliceAlong {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {π : X →L[ℝ] ℝ} {k l : X → Y} {δ : ℝ} {x : X} {k' l' : X →L[ℝ] Y} (hk : HasFDerivAt k k' x) (hl : HasFDerivAt l l' x) : HasFDerivAt (spliceAlong π k l δ) (k' + (spliceCutoff (δ⁻¹ * π x) • (l' - k') + ((δ⁻¹ * deriv spliceCutoff (δ⁻¹ * π x)) • π).smulRight (l x - k x))) x

The derivative of the spliced map, by the product rule.

theorem TauCeti.exists_hasFDerivAt_spliceAlong_sub_le {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {π : X →L[ℝ] ℝ} {k l : X → Y} {δ : ℝ} {x : X} {k' l' A : X →L[ℝ] Y} {ε B : ℝ} (hδ : 0 < δ) (hπ : ‖π‖ ≤ 1) (hB : ∀ (x : ℝ), |deriv spliceCutoff x| ≤ B) (hk : HasFDerivAt k k' x) (hl : HasFDerivAt l l' x) (hk' : ‖k' - A‖ ≤ ε) (hl' : ‖l' - A‖ ≤ ε) (hlk : ‖l x - k x‖ ≤ 2 * ε * |π x|) : ∃ (h' : X →L[ℝ] Y), HasFDerivAt (spliceAlong π k l δ) h' x ∧ ‖h' - A‖ ≤ (3 + 4 * B) * ε

The derivative of a spliced map. If the derivatives of k and l at x are within ε of a linear map A, ‖l x - k x‖ ≤ 2 ε |π x| and B bounds the derivative of the cutoff, then at every scale δ > 0 the spliced map has derivative within (3 + 4 B) ε of A at x, for a functional π of norm at most 1. The derivative δ⁻¹ χ' (δ⁻¹ π x) • π of the cutoff only meets l x - k x where |π x| ≤ 2 δ.

theorem TauCeti.injOn_and_injective_fderiv_spliceAlong_fst {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {k l : ℝ × ℝ → Y} {ρ δ ε B : ℝ} {A : ℝ × ℝ →L[ℝ] Y} {P : Y →L[ℝ] ℝ × ℝ} (hρ : 0 < ρ) (hδ : 0 < δ) (hkC : ContDiffOn ℝ 1 k {u : ℝ × ℝ | |u.1| < ρ}) (hlC : ContDiffOn ℝ 1 l {u : ℝ × ℝ | |u.1| < ρ}) (hkl0 : ∀ (t : ℝ), k (0, t) = l (0, t)) (hbound : ∀ (u : ℝ × ℝ), |u.1| < ρ → ‖fderiv ℝ k u - A‖ < ε ∧ ‖fderiv ℝ l u - A‖ < ε) (hB : ∀ (x : ℝ), |deriv spliceCutoff x| ≤ B) (hP : Function.LeftInverse ⇑P ⇑A) (hPε : ‖P‖ * ((3 + 4 * B) * ε) ≤ 1 / 2) : Set.InjOn (spliceAlong (ContinuousLinearMap.fst ℝ ℝ ℝ) k l δ) {u : ℝ × ℝ | |u.1| < ρ} ∧ ∀ (u : ℝ × ℝ), |u.1| < ρ → Function.Injective ⇑(fderiv ℝ (spliceAlong (ContinuousLinearMap.fst ℝ ℝ ℝ) k l δ) u)

A splice across a strip is injective with injective derivative when both maps agree on the central line and their derivatives stay close to a linear map with a left inverse. The bound on ε makes the splice composed with that left inverse approximate the identity.