Volume of a weighted cross-polytope

A positive weighted sum of absolute basis coordinates defines a cross-polytope. Its canonical Euclidean volume is the volume of the coordinate ℓ¹ unit ball, multiplied by the absolute basis determinant and divided by the product of the weights. This is the volume calculation used in the lower bound of Minkowski's second theorem.

For an arbitrary additive Haar measure μ on a finite-dimensional real normed space, the same cross-polytope has measure 2 ^ n / n! / ∏ i, a i times the measure of the fundamental parallelepiped of b (Module.Basis.addHaar_weighted_crosspolytope). No inner product is needed: the coordinates of b carry μ to a multiple of Lebesgue measure on ι → ℝ, and the multiple is the measure of the fundamental parallelepiped.

The general formula transports μ to Lebesgue measure by Module.Basis.addHaar_eq_measure_fundamentalDomain_mul_volume_image, writes the cross-polytope as the preimage of the ℓ¹ ball under a diagonal map, and applies Mathlib's MeasureTheory.Measure.addHaar_preimage_linearMap and TauCeti.volume_l1Ball. The Euclidean formula is its special case μ = volume: by ZSpan.measure_fundamentalDomain and OrthonormalBasis.volume_parallelepiped, the fundamental domain of b has volume |det_o b|.

With nonnegative weights the weighted cross-polytope lies in the weighted box {x | ∀ i, a i * |c x i| ≤ 1}, for any choice c of coordinates (TauCeti.weighted_crosspolytope_subset_weighted_box).

References

• J.-H. Evertse, Geometry of Numbers, §2.3, lower-bound proof of Theorem 2.9, printed p.27: https://pub.math.leidenuniv.nl/~evertsejh/dio19-2.pdf.

theorem TauCeti.weighted_crosspolytope_subset_weighted_box {ι : Type u_1} {F : Type u_2} [Fintype ι] {a : ι → ℝ} (ha : ∀ (i : ι), 0 ≤ a i) (c : F → ι → ℝ) : {x : F | ∑ i : ι, a i * |c x i| ≤ 1} ⊆ {x : F | ∀ (i : ι), a i * |c x i| ≤ 1}

With nonnegative weights a, the weighted cross-polytope {x | ∑ i, a i * |c x i| ≤ 1} lies in the weighted box {x | ∀ i, a i * |c x i| ≤ 1}, for any choice c of coordinates.

theorem Module.Basis.addHaar_weighted_crosspolytope {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {a : ι → ℝ} (ha : ∀ (i : ι), 0 < a i) : μ {x : E | ∑ i : ι, a i * |(b.repr x) i| ≤ 1} = ENNReal.ofReal (2 ^ Fintype.card ι / ↑(Fintype.card ι).factorial / ∏ i : ι, a i) * μ (ZSpan.fundamentalDomain b)

The measure of a weighted cross-polytope for an arbitrary additive Haar measure μ: if b is a basis of E and the weights a i are positive, then {x | ∑ i, a i * |b.repr x i| ≤ 1} has measure 2 ^ n / n! / ∏ i, a i times the measure of the fundamental parallelepiped of b, where n is the number of basis vectors. In an inner product space with its canonical volume that measure is the absolute determinant of b in an orthonormal basis, as in OrthonormalBasis.volume_weighted_crosspolytope.

theorem OrthonormalBasis.volume_weighted_crosspolytope {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (o : OrthonormalBasis ι ℝ E) (b : Module.Basis ι ℝ E) (a : ι → ℝ) (ha : ∀ (i : ι), 0 < a i) : MeasureTheory.volume {x : E | ∑ i : ι, a i * |(b.repr x) i| ≤ 1} = ENNReal.ofReal (2 ^ Fintype.card ι / ↑(Fintype.card ι).factorial * |o.toBasis.det ⇑b| / ∏ i : ι, a i)

The canonical Euclidean volume of a weighted cross-polytope in an arbitrary real basis. The index type may be empty, in which case the volume and the empty products are one.