Lipschitz-parametrizable sets

A set is Lipschitz parametrizable in dimension d when finitely many Lipschitz images of the unit d-cube cover it. This is the boundary regularity condition used in lattice-point counting: a codimension-one parametrization gives quantitative control on how many lattice cells can meet a boundary.

This file supplies the elementary API needed to assemble parametrizations: the property is monotone in the set, is preserved by Lipschitz images, by locally Lipschitz images, by products and by finite unions, and holds for finite sets. It also supplies the way in from smoothness: a map that is C¹ on the compact cube is Lipschitz there, so the image of a cube of the right dimension is a single chart. It also records the basic dimension consequence. A Lipschitz-parametrizable subset of a finite-dimensional real normed space has additive Haar measure zero whenever the parameter dimension is strictly smaller than the ambient dimension. The proof compares additive Haar measure with Hausdorff measure and uses the fact that Lipschitz maps do not increase Hausdorff dimension.

It also records the quantitative form of a single chart: cutting the unit d-cube into m ^ d subcubes of side 1 / m covers a Lipschitz image of it by m ^ d pieces of diameter C / m. That is what turns a parametrization in a given dimension into a count.

Main declarations

• TauCeti.IsLipschitzParametrizable: finite Lipschitz parametrizability by a unit cube;
• TauCeti.isLipschitzParametrizable_iff: the finite-chart characterization of the predicate;
• TauCeti.IsLipschitzParametrizable.union: closure under binary unions;
• TauCeti.IsLipschitzParametrizable.image: closure under Lipschitz images;
• TauCeti.IsLipschitzParametrizable.image_of_locallyLipschitz: closure under locally Lipschitz images, which is what a chart-by-chart compactness argument buys over image;
• TauCeti.IsLipschitzParametrizable.iUnion: closure under unions over a finite index type;
• TauCeti.IsLipschitzParametrizable.prod: a product is parametrized in the sum of the dimensions;
• TauCeti.IsLipschitzParametrizable.image_unitCube_of_contDiffOn: a unit cube's image under a map that is C¹ on it is parametrized by that cube;
• TauCeti.IsLipschitzParametrizable.of_isBounded: a bounded subset of a finite-dimensional real normed space is parametrized in the ambient dimension;
• TauCeti.IsLipschitzParametrizable.of_isBounded_of_subset_ker: a bounded subset of a hyperplane is parametrized in codimension one;
• TauCeti.IsLipschitzParametrizable.measure_zero: a parametrized set has additive Haar measure zero below the ambient dimension;
• LipschitzOnWith.exists_cover_image_unitCube: a Lipschitz image of the unit d-cube is covered by m ^ d pieces of arbitrarily small diameter.

References

• S. Lang, Algebraic Number Theory, Chapter VI, Section 2, which the definition and its use in the lattice-point estimate follow.
• C. Birkbeck, AINTLIB at commit db14b34cc5e3d79603e67c205dfa86b7b989000c (Apache-2.0), projects/Chebotarev/CebotarevDensity/ForMathlib/IdealCongruenceCount.lean, whose exists_lipschitz_cube_cover_hyperplane_slab is the concrete precursor of of_isBounded and of_isBounded_of_subset_ker: it covers a bounded slab of a coordinate hyperplane of ι → ℝ by a single chart, through the same affine rescaling c ↦ 2 * M * c - M of the unit cube onto the box [-M, M]. The two lemmas here say the same thing without reference to coordinates, for any finite-dimensional real normed space and any hyperplane in it.

def TauCeti.IsLipschitzParametrizable {E : Type u_1} [PseudoEMetricSpace E] (d : ℕ) (S : Set E) : Prop

A set is Lipschitz parametrizable in dimension d if it is covered by finitely many Lipschitz images of the unit cube in Fin d → ℝ.

Equations

• TauCeti.IsLipschitzParametrizable d S = ∃ (n : ℕ) (C : NNReal) (f : Fin n → (Fin d → ℝ) → E), (∀ (i : Fin n), LipschitzOnWith C (f i) (Set.Icc 0 1)) ∧ S ⊆ ⋃ (i : Fin n), f i '' Set.Icc 0 1

theorem TauCeti.isLipschitzParametrizable_iff {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} {S : Set E} : IsLipschitzParametrizable d S ↔ ∃ (n : ℕ) (C : NNReal) (f : Fin n → (Fin d → ℝ) → E), (∀ (i : Fin n), LipschitzOnWith C (f i) (Set.Icc 0 1)) ∧ S ⊆ ⋃ (i : Fin n), f i '' Set.Icc 0 1

A set is Lipschitz parametrizable in dimension d if and only if finitely many unit-cube charts, all Lipschitz with a common constant on the unit cube, cover it.

theorem TauCeti.IsLipschitzParametrizable.mono {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} {S T : Set E} (hT : IsLipschitzParametrizable d T) (hST : S ⊆ T) : IsLipschitzParametrizable d S

Every subset of a Lipschitz-parametrizable set is Lipschitz parametrizable with the same charts.

@[simp]

theorem TauCeti.IsLipschitzParametrizable.empty {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} : IsLipschitzParametrizable d ∅

The empty set is Lipschitz parametrizable in every dimension.

@[simp]

theorem TauCeti.IsLipschitzParametrizable.singleton {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} (x : E) : IsLipschitzParametrizable d {x}

A singleton is Lipschitz parametrizable in every dimension.

theorem TauCeti.IsLipschitzParametrizable.union {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} {S T : Set E} (hS : IsLipschitzParametrizable d S) (hT : IsLipschitzParametrizable d T) : IsLipschitzParametrizable d (S ∪ T)

The union of two Lipschitz-parametrizable sets in the same dimension is Lipschitz parametrizable.

theorem TauCeti.IsLipschitzParametrizable.biUnion_finset {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} {I : Type u_3} (s : Finset I) {A : I → Set E} (hA : ∀ i ∈ s, IsLipschitzParametrizable d (A i)) : IsLipschitzParametrizable d (⋃ i ∈ s, A i)

A finite union of sets parametrized in the same dimension is Lipschitz parametrizable.

theorem TauCeti.IsLipschitzParametrizable.iUnion {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} {I : Type u_3} [Finite I] {A : I → Set E} (hA : ∀ (i : I), IsLipschitzParametrizable d (A i)) : IsLipschitzParametrizable d (⋃ (i : I), A i)

A union over a finite index type of sets parametrized in dimension d is Lipschitz parametrizable in dimension d.

theorem TauCeti.IsLipschitzParametrizable.prod {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} {S : Set E} {G : Type u_3} [PseudoEMetricSpace G] {e : ℕ} {T : Set G} (hS : IsLipschitzParametrizable d S) (hT : IsLipschitzParametrizable e T) : IsLipschitzParametrizable (d + e) (S ×ˢ T)

A product of parametrized sets is Lipschitz parametrizable in the sum of the dimensions.

theorem TauCeti.IsLipschitzParametrizable.finite {E : Type u_1} [PseudoEMetricSpace E] {d : ℕ} {S : Set E} (hS : S.Finite) : IsLipschitzParametrizable d S

A finite set is Lipschitz parametrizable in every dimension.

theorem TauCeti.IsLipschitzParametrizable.image {E : Type u_1} {F : Type u_2} [PseudoEMetricSpace E] [PseudoEMetricSpace F] {d : ℕ} {S : Set E} {g : E → F} {K : NNReal} (hg : LipschitzWith K g) (hS : IsLipschitzParametrizable d S) : IsLipschitzParametrizable d (g '' S)

The image of a Lipschitz-parametrizable set under a Lipschitz map is Lipschitz parametrizable.

theorem TauCeti.IsLipschitzParametrizable.image_unitCube_of_contDiffOn {ι : Type u_3} {G : Type u_4} [Fintype ι] [NormedAddCommGroup G] [NormedSpace ℝ G] {d : ℕ} (hd : Fintype.card ι = d) {f : (ι → ℝ) → G} (hf : ContDiffOn ℝ 1 f (Set.Icc 0 1)) : IsLipschitzParametrizable d (f '' Set.Icc 0 1)

The image of the unit cube of ι → ℝ under a map that is C¹ on that cube is Lipschitz parametrizable in dimension #ι. The cube is indexed by an arbitrary finite type ι of cardinality d, not by Fin d itself.

theorem TauCeti.IsLipschitzParametrizable.of_isBounded {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} (hS : Bornology.IsBounded S) : IsLipschitzParametrizable (Module.finrank ℝ E) S

A bounded subset of a finite-dimensional real normed space is Lipschitz parametrizable in the ambient dimension. Linear coordinates carry the set into a box, and a box is the image of the unit cube under an affine — hence C¹ — map, so one chart suffices.

This is the trivial bound on the dimension: it is useful only for pieces of a set that are genuinely lower dimensional for another reason, such as a bounded piece of a hyperplane.

theorem TauCeti.IsLipschitzParametrizable.of_isBounded_of_subset_ker {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E →ₗ[ℝ] ℝ} (hf : f ≠ 0) {S : Set E} (hS : Bornology.IsBounded S) (hSf : S ⊆ ↑f.ker) : IsLipschitzParametrizable (Module.finrank ℝ E - 1) S

A bounded subset of a hyperplane is Lipschitz parametrizable in codimension one. The hyperplane is the kernel of a nonzero linear functional, a subspace of dimension finrank ℝ E - 1; inside it the set is still bounded, because the inclusion is an isometry.

theorem TauCeti.IsLipschitzParametrizable.image_of_locallyLipschitz {E : Type u_3} {F : Type u_4} [PseudoMetricSpace E] [PseudoMetricSpace F] {d : ℕ} {S : Set E} {g : E → F} (hg : LocallyLipschitz g) (hS : IsLipschitzParametrizable d S) : IsLipschitzParametrizable d (g '' S)

The image of a Lipschitz-parametrizable set under a locally Lipschitz map is Lipschitz parametrizable.

theorem TauCeti.IsLipschitzParametrizable.measure_zero {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {d : ℕ} {S : Set E} (hS : IsLipschitzParametrizable d S) (hd : d < Module.finrank ℝ E) : μ S = 0

A set Lipschitz parametrized in dimension d has zero additive Haar measure in a finite-dimensional real normed space of dimension strictly larger than d.

This statement is formulated for an arbitrary additive Haar measure, so it applies directly to the volume normalization used by a lattice and is invariant under later linear coordinate changes.

theorem LipschitzOnWith.exists_cover_image_unitCube {E : Type u_1} [PseudoMetricSpace E] {d : ℕ} {C : NNReal} {f : (Fin d → ℝ) → E} (hf : LipschitzOnWith C f (Set.Icc 0 1)) {m : ℕ} (hm : 0 < m) : ∃ (T : (Fin d → Fin m) → Set E), f '' Set.Icc 0 1 ⊆ ⋃ (k : Fin d → Fin m), T k ∧ ∀ (k : Fin d → Fin m), ∀ x ∈ T k, ∀ y ∈ T k, dist x y ≤ ↑C / ↑m

A map that is Lipschitz with constant C on the unit cube Icc 0 1 of Fin d → ℝ carries that cube into a union of m ^ d pieces — one for each subcube of side 1 / m — each of diameter at most C / m.

This is the quantitative content of a chart of a Lipschitz parametrization: cutting the cube finely enough covers the image by a prescribed number of arbitrarily small pieces, which is what bounds the number of lattice cells such an image can meet.