Theorems · Theorem · number theory

MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure

• #40 of the 100 theorems: Minkowski’s Fundamental Theorem
• 1000+ list: Minkowski's theorem

∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {L : AddSubgroup E}
  [Countable ↥L],
  MeasureTheory.IsAddFundamentalDomain (↥L) F μ →
    (∀ x ∈ s, -x ∈ s) → Convex ℝ s → μ F * 2 ^ Module.finrank ℝ E < μ s → ∃ x, x ≠ 0 ∧ ↑x ∈ s

The Minkowski Convex Body Theorem. If s is a convex symmetric domain of E whose volume is large enough compared to the covolume of a lattice L of E, then it contains a non-zero lattice point of L.

Defined in

Mathlib.MeasureTheory.Group.GeometryOfNumbers

Cited by

3 results in Mathlib

Foundations

Depth 261 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasureCountable