English
If the volume of a set s exceeds the covolume of a countable lattice L in E, then there exist two distinct lattice points x, y such that x+s and y+s have a nonempty intersection.
Русский
Если объём множества s больше ковольюма годного решётки L в E, то существуют два различных элемента x, y ∈ L такие, что (x+s) и (y+s) непусто пересекаются.
LaTeX
$$$\\exists x,y \\in L,\\ x \\neq y \\land \\neg\\operatorname{Disjoint}(x+s, y+s).$$$
Lean4
/-- **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. -/
theorem exists_pair_mem_lattice_not_disjoint_vadd [AddGroup L] [Countable L] [AddAction L E] [MeasurableSpace L]
[MeasurableVAdd L E] [VAddInvariantMeasure L E μ] (fund : IsAddFundamentalDomain L F μ) (hS : NullMeasurableSet s μ)
(h : μ F < μ s) : ∃ x y : L, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s) :=
by
contrapose! h
exact
((fund.measure_eq_tsum _).trans
(measure_iUnion₀ (Pairwise.mono h fun i j hij => (hij.mono inf_le_left inf_le_left).aedisjoint) fun _ =>
(hS.vadd _).inter fund.nullMeasurableSet).symm).trans_le
(measure_mono <| Set.iUnion_subset fun _ => Set.inter_subset_right)
