Theorems · Theorem · number theory

MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd

∀ {E : Type u_1} {L : Type u_2} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E}
  [inst_1 : AddGroup L] [Countable L] [inst_3 : AddAction L E] [inst_4 : MeasurableSpace L] [MeasurableVAdd L E]
  [MeasureTheory.VAddInvariantMeasure L E μ],
  MeasureTheory.IsAddFundamentalDomain L F μ →
    MeasureTheory.NullMeasurableSet s μ → μ F < μ s → ∃ x y, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)

Blichfeldt's Theorem. If the volume of the set s is larger than the covolume of the countable subgroup L of E, then there exist two distinct points x, y ∈ L such that (x + s) and (y + s) are not disjoint.

Defined in

Mathlib.MeasureTheory.Group.GeometryOfNumbers

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceAddGroupCountableAddActionMeasurableSpaceMeasurableVAddMeasureTheory.VAddInvariantMeasure