Product Minkowski Covolume

Abstract

Finite product fundamental domains yield the discriminant covolume in every finite power.

Theorem 1.1 (Dependent finite products of basis fundamental domains).

$$\mathrm{finite}\left(I\right),\mathrm{realNormedSpaces}\left(E\right),\mathrm{bases}\left(b,J,E\right)\Rightarrow \mathrm{FD}\left(\mathrm{PiBasis}\left(b\right)\right)=\mathrm{SetPi}\left(I,\mathrm{FD}\left(b_i\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ProductMinkowskiCovolume.fundamentalDomain_pi (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite type I and families of types J(i) and E(i), assume each E(i) is a normed additive commutative group and a real normed space, and let b(i) be a J(i)-indexed real basis of E(i). No finiteness of J(i) is assumed. FD denotes ZSpan.fundamentalDomain. The sigma-indexed Pi basis has exactly the component coordinate inequalities.

Theorem 1.2 (Product volume for sigma-finite component measures).

$$\mathrm{finite}\left(I\right),\mathrm{realNormedSpaces}\left(E\right),\mathrm{bases}\left(b,J,E\right),\mathrm{sigmaFiniteVolumes}\left(E\right)\Rightarrow \mathrm{vol}\left(\mathrm{FD}\left(\mathrm{PiBasis}\left(b\right)\right)\right)=\prod _{i\in I}\mathrm{vol}\left(\mathrm{FD}\left(b_i\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ProductMinkowskiCovolume.volume_fundamentalDomain_pi (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume all the hypotheses of the factorization theorem. In addition, each E(i) has a MeasureSpace whose volume is sigma-finite. The volume on the dependent function space is the canonical product measure. The equality is in the extended nonnegative reals and requires no Haar or Borel hypothesis.

Theorem 1.3 (Discriminant covolume of the finite-power Minkowski lattice).

$$\mathrm{NumberField}\left(K\right),r\in \mathbb{N}\Rightarrow \mathrm{covol}\left(\mathrm{restrictedMinkowskiLattice}\left(K,r\right)\right)={{2^{-1}}^{c\left(K\right)}\times \sqrt{\mathrm{abs}\left(\mathrm{disc}\left(K\right)\right)}}^r$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ProductMinkowskiCovolume.restrictedMinkowskiLattice_covolume (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let K be a field with a NumberField instance and let r be any natural number, including zero. The lattice is the existing restrictedMinkowskiLattice K r, with canonical product volume on Fin(r) to mixedSpace(K). The symbol c(K) denotes NumberField.InfinitePlace.nrComplexPlaces K and disc(K) denotes NumberField.discr K cast to the reals. The formula follows by applying the new product factorization to Mathlib’s one-copy discriminant formula.

References

• Truth anchor: D5/S3/Arith/Lattices/ProductMinkowskiCovolume.fundamentalDomain_pi
• Truth anchor: D5/S3/Arith/Lattices/ProductMinkowskiCovolume.restrictedMinkowskiLattice_covolume
• Truth anchor: D5/S3/Arith/Lattices/ProductMinkowskiCovolume.volume_fundamentalDomain_pi
• Dependency: D5/S3/Arith/Lattices/RestrictedScalarFreeMinkowskiLattice