minkowskiBound — Mathlib

English

For any number field K and fractional ideal unit I, the Minkowski bound is strictly less than the top element of ENNReal.

Русский

Для любого числа поля K и единицы дробно-идеала MinkowskiBound(K,I) строго меньше верхнего элемента ENNReal.

LaTeX

$$minkowskiBound K I < ⊤$$

Lean4

/-- The bound that appears in **Minkowski Convex Body theorem**, see
`MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`. See
`NumberField.mixedEmbedding.volume_fundamentalDomain_idealLatticeBasis_eq` and
`NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis` for the computation of
`volume (fundamentalDomain (idealLatticeBasis K))`. -/
noncomputable def minkowskiBound : ℝ≥0∞ :=
  volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) * (2 : ℝ≥0∞) ^ (finrank ℝ (mixedSpace K))

Похожие утверждения