Injective pieces of a differentiable map

A measurable set on which a map has injective derivative admits a countable measurable partition on which the map is bi-Lipschitz. This decomposition permits summation of injective change-of-variables and area formulas with multiplicity, without requiring the original map to be injective.

The construction uses Mathlib's exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, with an absolute error scaled to each candidate linear map, so that on every piece the map is within any prescribed relative error δ of an injective linear map (TauCeti.exists_partition_linear_approximation_of_hasFDerivWithinAt). For δ < 1 such a piece has a Lipschitz inverse (TauCeti.exists_antilipschitzWith_domRestrict_of_approx), which gives the bi-Lipschitz partition TauCeti.exists_partition_lipschitz_antilipschitz_of_hasFDerivWithinAt.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §3.3 (decomposition into injective pieces in the area formula).

theorem TauCeti.one_sub_mul_norm_sub_le_norm_sub {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : U → V} {p : Set U} {A : U →L[ℝ] V} {δ : ℝ} (happ : ∀ x ∈ p, ∀ y ∈ p, ‖f x - f y - A (x - y)‖ ≤ δ * ‖A (x - y)‖) {x y : U} (hx : x ∈ p) (hy : y ∈ p) : (1 - δ) * ‖A x - A y‖ ≤ ‖f x - f y‖

A map within relative error δ of a linear map A on p satisfies (1 - δ) ‖A x - A y‖ ≤ ‖f x - f y‖ there.

theorem TauCeti.norm_sub_le_one_add_mul_norm_sub {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : U → V} {p : Set U} {A : U →L[ℝ] V} {δ : ℝ} (happ : ∀ x ∈ p, ∀ y ∈ p, ‖f x - f y - A (x - y)‖ ≤ δ * ‖A (x - y)‖) {x y : U} (hx : x ∈ p) (hy : y ∈ p) : ‖f x - f y‖ ≤ (1 + δ) * ‖A x - A y‖

A map within relative error δ of a linear map A on p satisfies ‖f x - f y‖ ≤ (1 + δ) ‖A x - A y‖ there.

theorem TauCeti.lipschitzOnWith_and_antilipschitzWith_of_approx {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : U → V} {p : Set U} {A : U →L[ℝ] V} {ε : NNReal} (hA : Function.Injective ⇑A) (hε : ε < 1) (happ : ∀ x ∈ p, ∀ y ∈ p, ‖f x - f y - A (x - y)‖ ≤ ↑ε * ‖A (x - y)‖) : LipschitzOnWith (1 + ε) (f ∘ Function.invFun ⇑A) (⇑A '' p) ∧ AntilipschitzWith (1 - ε)⁻¹ ((⇑A '' p).domRestrict (f ∘ Function.invFun ⇑A))

A map f within relative error ε < 1 of an injective linear map A on p, read through A, is (1 + ε)-Lipschitz on A '' p with (1 - ε)⁻¹-Lipschitz inverse.

theorem TauCeti.exists_antilipschitzWith_domRestrict_of_approx {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : U → V} {p : Set U} {A : U →L[ℝ] V} {δ : ℝ} [FiniteDimensional ℝ U] (hA : p.Nonempty → Function.Injective ⇑A) (hδ : δ < 1) (happ : ∀ x ∈ p, ∀ y ∈ p, ‖f x - f y - A (x - y)‖ ≤ δ * ‖A (x - y)‖) : ∃ (L : NNReal), AntilipschitzWith L (p.domRestrict f)

A map within relative error δ < 1 of an injective linear map on p has a Lipschitz inverse on p.

theorem TauCeti.exists_partition_linear_approximation_of_hasFDerivWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : U → V} {δ : ℝ} [FiniteDimensional ℝ U] [MeasurableSpace U] [BorelSpace U] [SecondCountableTopology V] {s : Set U} {f' : U → U →L[ℝ] V} (hs : MeasurableSet s) (hd : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hinj : ∀ x ∈ s, Function.Injective ⇑(f' x)) (hδ : 0 < δ) : ∃ (p : ℕ → Set U) (A : ℕ → U →L[ℝ] V), (∀ (n : ℕ), MeasurableSet (p n)) ∧ Pairwise (Function.onFun Disjoint p) ∧ ⋃ (n : ℕ), p n = s ∧ (∀ (n : ℕ), (p n).Nonempty → Function.Injective ⇑(A n)) ∧ ∀ (n : ℕ), ∀ x ∈ p n, ∀ y ∈ p n, ‖f x - f y - (A n) (x - y)‖ ≤ δ * ‖(A n) (x - y)‖

A measurable set on which the derivative is injective has, for every δ > 0, a countable measurable partition into pieces p n, each with a linear map A n that is injective whenever the piece is nonempty and satisfies ‖f x - f y - A n (x - y)‖ ≤ δ ‖A n (x - y)‖ on the piece. No global Lipschitz assumption is needed.

theorem TauCeti.exists_partition_lipschitz_antilipschitz_of_hasFDerivWithinAt {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [MeasurableSpace U] [BorelSpace U] [NormedAddCommGroup V] [NormedSpace ℝ V] [SecondCountableTopology V] {f : U → V} {s : Set U} {f' : U → U →L[ℝ] V} (hs : MeasurableSet s) (hd : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hinj : ∀ x ∈ s, Function.Injective ⇑(f' x)) : ∃ (p : ℕ → Set U) (L : ℕ → NNReal) (K : ℕ → NNReal), (∀ (n : ℕ), MeasurableSet (p n)) ∧ Pairwise (Function.onFun Disjoint p) ∧ ⋃ (n : ℕ), p n = s ∧ ∀ (n : ℕ), LipschitzWith (L n) ((p n).domRestrict f) ∧ AntilipschitzWith (K n) ((p n).domRestrict f)

A measurable set on which the derivative is injective has a countable measurable partition into bi-Lipschitz pieces. No global Lipschitz assumption is needed.