A Fubini decomposition of the quotient measure over a subspace

For a lattice Λ in a real vector space V with fundamental domain F, and a second space W, the slab F ×ˢ univ is a fundamental domain in V × W for the sublattice Λ × 0, so that for a Λ × 0-invariant set S the number (μV.prod μW) ((F ×ˢ univ) ∩ S) is the measure of the image of S in the quotient (V × W) ⧸ (Λ × 0). The main result decomposes that number as an integral over W of the quotient measures in V ⧸ Λ of the slices of S.

This is the identity (10) in Cassels' proof of his Chapter VIII, Theorem IV, which is the kernel of Weyl's proof of the upper bound in Minkowski's second theorem. Two further results carry the rest of that proof: the descent ZLattice.measure_inter_add_eq_of_separated, which says that for a set whose points are congruent modulo the big lattice L only when they are congruent modulo the small one Λ, the quotient measures over L and over Λ agree; and the scaling estimate ZLattice.measure_inter_add_prod_smul_le, which says that dilating a convex set by s ≥ 1 multiplies its quotient measure over Λ × 0 by at least s ^ dim W.

Main results

• ZLattice.measure_inter_add_prod_eq_lintegral: the Fubini decomposition, Cassels' (10).
• ZLattice.isAddFundamentalDomain_prod_univ: the slab F ×ˢ univ is a fundamental domain for Λ × 0, which is what makes the left-hand side of the decomposition a quotient measure.
• ZLattice.measure_inter_add_prod_smul_le: the scaling estimate, Cassels' (12) and (14).
• ZLattice.exists_isAddFundamentalDomain_measure_smul_le: the scaling estimate for a lattice of arbitrary rank in a single space, with the slab produced rather than assumed.
• ZLattice.measure_inter_add_eq_of_separated: the descent from L to Λ.
• ZLattice.pow_mul_measure_inter_add_le: the two combined — Cassels' Theorem IV in one step, the form Minkowski's second theorem chains over the successive minima.
• ZLattice.countable_of_discreteTopology: a discrete ℤ-submodule of a finite-dimensional real normed space is countable. Mathlib has this only for a lattice of full rank.

Implementation notes

⚠ The scaling estimate is not a statement about one set being a packing. Its proof translates each slice of the body by a different vector — (s - 1) • y₀ for some y₀ in that slice — and what makes that legitimate is exactly that the quotient measure of a slice is unchanged by translation. There is no single map of V × W doing this, which is why the Fubini decomposition, and not a change of variables, is the tool.

⚠ The descent needs the covolume to be finite, and that is the only place any finiteness enters. The proof exhibits (FΛ ∩ (A + Λ)) ∪ (FL \ (A + L)) as a fundamental domain for L, so it has the measure of FL; cancelling the second piece off both sides is what needs μ FL ≠ ⊤. No compactness, closedness or boundedness of the body is used anywhere in this file.

⚠ IsZLattice is not a hypothesis of the product results, and Countable is all they want. A fundamental domain is passed in as the hypothesis ∀ x, ∃! v : Λ, ↑v + x ∈ F rather than constructed, so the product statements are about an arbitrary countable ℤ-submodule. Only ZLattice.exists_isAddFundamentalDomain_measure_smul_le, which builds the slab, needs the submodule to be discrete — and there it is a ZLattice in its own span, not in the ambient space.

References

J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer (1959), Chapter VIII §4.2, Theorem IV, and the displays (10), (12) and (14) of its proof. Cassels normalizes the lattice to ℤ ^ n by a linear transformation first; the V × W form here is that normalization made coordinate-free, and ZLattice.exists_isAddFundamentalDomain_measure_smul_le performs it.

⚠ What is not here is the chaining of Theorem IV over the successive minima, which is Minkowski's second theorem itself. Beside the chain it wants three pieces of gauge bookkeeping, all specific to the body rather than to the quotient measure: that L ∩ span (v 0, …, v (J - 1)) has rank J, that Cassels' Lemma 2 (ZLattice.exists_basis_mem_span_int_of_gauge_lt) supplies the separation hypothesis for t • B when 2 t is below the J-th minimum, and that a dilate of the body has the expected measure.

This is infrastructure for Layer 4.2 of the ArithmeticHeights roadmap.

theorem ZLattice.measure_inter_add_eq_of_separated {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddLeftInvariant] {Λ L : Submodule ℤ E} [Countable ↥Λ] [Countable ↥L] (hΛL : Λ ≤ L) {FΛ FL : Set E} (hΛ : ∀ (x : E), ∃! v : ↥Λ, ↑v + x ∈ FΛ) (hL : ∀ (x : E), ∃! v : ↥L, ↑v + x ∈ FL) (hmΛ : MeasurableSet FΛ) (hmL : MeasurableSet FL) (hfin : μ FL ≠ ⊤) {A : Set E} (hA : MeasurableSet A) (hsep : ∀ x ∈ A, ∀ y ∈ A, x - y ∈ L → x - y ∈ Λ) : μ (FΛ ∩ (A + ↑Λ)) = μ (FL ∩ (A + ↑L))

The descent from a lattice to a sublattice (the equivalence of (6) with (7) and (8) in Cassels' proof of his Chapter VIII, Theorem IV). If two points of A are congruent modulo L only when they are congruent modulo the sublattice Λ, then the measure of the image of A in E ⧸ L equals the measure of its image in E ⧸ Λ: the covering E ⧸ Λ → E ⧸ L is injective there.

Both measures are read off against fundamental domains — FΛ for Λ, FL for L, each given by its exact form ∀ x, ∃! v, ↑v + x ∈ · — and the proof exhibits (FΛ ∩ (A + Λ)) ∪ (FL \ (A + L)) as a third fundamental domain, for L. ⚠ This is where μ FL ≠ ⊤ is used, and it is the only finiteness hypothesis in the file.

theorem ZLattice.isAddFundamentalDomain_prod_univ {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [MeasurableSpace V] [NormedAddCommGroup W] [MeasurableSpace W] (μV : MeasureTheory.Measure V) (μW : MeasureTheory.Measure W) (Λ : Submodule ℤ V) {F : Set V} (hF : ∀ (x : V), ∃! v : ↥Λ, ↑v + x ∈ F) (hFm : MeasurableSet F) : MeasureTheory.IsAddFundamentalDomain (↥(Λ.prod ⊥)) (F ×ˢ Set.univ) (μV.prod μW)

The slab is a fundamental domain. If F is a fundamental domain for Λ in V, then F ×ˢ univ is one for Λ × 0 in V × W. This is what makes the left-hand side of ZLattice.measure_inter_add_prod_eq_lintegral the measure of an image in the quotient.

theorem ZLattice.measure_inter_add_prod_eq_lintegral {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W] (μV : MeasureTheory.Measure V) [μV.IsAddHaarMeasure] (μW : MeasureTheory.Measure W) [μW.IsAddHaarMeasure] (Λ : Submodule ℤ V) [Countable ↥Λ] {F : Set V} (hFm : MeasurableSet F) {X : Set (V × W)} (hX : MeasurableSet X) : (μV.prod μW) (F ×ˢ Set.univ ∩ (X + ↑(Λ.prod ⊥))) = ∫⁻ (z : W), μV (F ∩ ({y : V | (y, z) ∈ X} + ↑Λ)) ∂μW

The Fubini decomposition of the quotient measure (Cassels, Chapter VIII, §4.2, the display (10) in the proof of Theorem IV). The measure of the image of X in (V × W) ⧸ (Λ × 0) is the integral over W of the measures of the images of the slices of X in V ⧸ Λ.

Both sides are quotient measures read off against fundamental domains: the slab F ×ˢ univ on the left, by ZLattice.isAddFundamentalDomain_prod_univ, and F itself on the right.

theorem ZLattice.measure_inter_add_prod_smul_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W] (μV : MeasureTheory.Measure V) [μV.IsAddHaarMeasure] (μW : MeasureTheory.Measure W) [μW.IsAddHaarMeasure] (Λ : Submodule ℤ V) [Countable ↥Λ] {F : Set V} (hF : ∀ (x : V), ∃! v : ↥Λ, ↑v + x ∈ F) (hFm : MeasurableSet F) {A : Set (V × W)} (hAm : MeasurableSet A) (hAc : Convex ℝ A) {s : ℝ} (hs : 1 ≤ s) : ENNReal.ofReal (s ^ Module.finrank ℝ W) * (μV.prod μW) (F ×ˢ Set.univ ∩ (A + ↑(Λ.prod ⊥))) ≤ (μV.prod μW) (F ×ˢ Set.univ ∩ (s • A + ↑(Λ.prod ⊥)))

The scaling estimate (Cassels, Chapter VIII, §4.2, the displays (12) and (14) in the proof of Theorem IV). For a convex set A and s ≥ 1, the quotient measure of s • A over Λ × 0 is at least s ^ dim W times that of A.

The factor is s ^ dim W and not s ^ dim (V × W) because the Fubini decomposition scales only the W-direction: on each slice the dilation is replaced by a translation, which the quotient measure over Λ does not see. ⚠ The translating vector depends on the slice, so no map of V × W realizes this comparison; see the implementation notes.

theorem ZLattice.countable_of_discreteTopology {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Λ : Submodule ℤ E) [DiscreteTopology ↥Λ] : Countable ↥Λ

A discrete ℤ-submodule of a finite-dimensional real normed space is countable. Mathlib has this for a ZLattice; a discrete submodule of smaller rank is a ZLattice in its own span.

theorem ZLattice.exists_isAddFundamentalDomain_measure_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (Λ : Submodule ℤ E) [DiscreteTopology ↥Λ] : ∃ (F : Set E), MeasurableSet F ∧ (∀ (x : E), ∃! v : ↥Λ, ↑v + x ∈ F) ∧ ∀ (A : Set E), MeasurableSet A → Convex ℝ A → ∀ (s : ℝ), 1 ≤ s → ENNReal.ofReal (s ^ (Module.finrank ℝ E - Module.finrank ℤ ↥Λ)) * μ (F ∩ (A + ↑Λ)) ≤ μ (F ∩ (s • A + ↑Λ))

The scaling estimate for a lattice of arbitrary rank in a single space, with the slab produced rather than assumed: some measurable set F is a fundamental domain for Λ and, for every convex A and every s ≥ 1, the quotient measure of s • A modulo Λ is at least s ^ (n - rank Λ) times that of A.

This is Cassels' normalization of his Chapter VIII, Theorem IV made intrinsic: he transforms the lattice to ℤ ^ n linearly, and the transformation is here the choice of a complement W of the span of Λ, along which the fundamental parallelepiped of Λ in that span is extended to the slab F. The exponent is dim W.

theorem ZLattice.pow_mul_measure_inter_add_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {Λ L : Submodule ℤ E} [DiscreteTopology ↥Λ] [DiscreteTopology ↥L] (hΛL : Λ ≤ L) {FL : Set E} (hL : ∀ (x : E), ∃! v : ↥L, ↑v + x ∈ FL) (hmL : MeasurableSet FL) (hfin : μ FL ≠ ⊤) {A : Set E} (hAm : MeasurableSet A) (hAc : Convex ℝ A) {s : ℝ} (hs : 1 ≤ s) (hsepA : ∀ x ∈ A, ∀ y ∈ A, x - y ∈ L → x - y ∈ Λ) (hsepB : ∀ x ∈ s • A, ∀ y ∈ s • A, x - y ∈ L → x - y ∈ Λ) : ENNReal.ofReal (s ^ (Module.finrank ℝ E - Module.finrank ℤ ↥Λ)) * μ (FL ∩ (A + ↑L)) ≤ μ (FL ∩ (s • A + ↑L))

Cassels' Chapter VIII, Theorem IV, in one step (the display (14) of his proof). For a convex set A on which congruence modulo the lattice L is congruence modulo the sublattice Λ, dilating by s ≥ 1 multiplies the measure of the image in E ⧸ L by at least s ^ (n - rank Λ).

This is the inductive step of Weyl's proof of the upper bound in Minkowski's second theorem: the separation hypotheses are Cassels' Lemma 2 applied to A = t • B, and the exponent decreases by one each time t passes a successive minimum.