MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure
theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure :
∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E}
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : BorelSpace E]
[inst_4 : FiniteDimensional ℝ E] [inst_5 : Nontrivial E] [inst_6 : μ.IsAddHaarMeasure] {L : AddSubgroup E}
[inst_7 : Countable ↥L] [inst_8 : DiscreteTopology ↥L],
MeasureTheory.IsAddFundamentalDomain (↥L) F μ →
(∀ x ∈ s, -x ∈ s) →
Convex ℝ s → IsCompact s → ↑↑μ F * 2 ^ FiniteDimensional.finrank ℝ E ≤ ↑↑μ s → ∃ x, x ≠ 0 ∧ ↑x ∈ s
The **Minkowski Convex Body Theorem for compact domain** states that for a given measurable space `E` and a measure `μ` on `E`, if `s` is a convex compact symmetric domain of `E` and `F` is an add fundamental domain for a lattice `L` of `E`, with `L` being countable and discretely topological, then provided the measure of `F` times two to the power of the `E`'s finite dimension is less than or equal to the measure of `s`, there exists a non-zero lattice point of `L` within `s`. This theorem assumes that `E` is a normed add commutative group and a normed space over the real numbers, and that `μ` is an add Haar measure. Compared to `exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`, this version requires that `s` is compact and `L` is discrete but weakens the inequality constraint.
More concisely: Given a measurable space `E` with a convex compact symmetric domain `s`, a measurable space `F` as an add fundamental domain for a countable, discrete, and topologically separable lattice `L` in `E`, and a Haar measure `μ` on `E` such that the measure of `F` raised to the power of the dimension of `E` is less than or equal to the measure of `s`, then `s` contains a non-zero lattice point of `L`.
|
MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd
theorem 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 : AddCommGroup L] [inst_2 : Countable L] [inst_3 : AddAction L E] [inst_4 : MeasurableSpace L]
[inst_5 : MeasurableVAdd L E] [inst_6 : 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**: Consider a measure space `(E, μ)`, where `E` is a set and `μ` is a measure on `E`. Let `L` be a countable additive commutative group acting on `E`, and `F` be a fundamental domain of `L` under this action. Also, suppose `s` is a null measurable subset of `E`. If the measure of `F` is strictly less than the measure of `s`, then there exist two distinct elements `x` and `y` in `L` such that the sets `x + s` and `y + s` (i.e., `s` translated by `x` and `y`, respectively) are not disjoint. In other words, the sets `x + s` and `y + s` have a non-empty intersection.
More concisely: If `(E, μ)` is a measure space with a countable additive commutative group action `L`, and `F` is a fundamental domain of `L` with strictly smaller measure than a null measurable set `s`, then there exist distinct `x, y` in `L` such that `x + s` and `y + s` intersect.
|
MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure :
∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E}
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : BorelSpace E]
[inst_4 : FiniteDimensional ℝ E] [inst_5 : μ.IsAddHaarMeasure] {L : AddSubgroup E} [inst_6 : Countable ↥L],
MeasureTheory.IsAddFundamentalDomain (↥L) F μ →
(∀ x ∈ s, -x ∈ s) → Convex ℝ s → ↑↑μ F * 2 ^ FiniteDimensional.finrank ℝ E < ↑↑μ s → ∃ x, x ≠ 0 ∧ ↑x ∈ s
The **Minkowski Convex Body Theorem** states that for any measurable space `E`, given a measure `μ`, two sets `F` and `s` in `E`, norms, a Borel Space, a finite-dimensional real vector space, and a countable subgroup `L` of `E` such that `μ` is a Add Haar Measure, if `F` forms an Add Fundamental Domain with respect to the measure `μ` and `s` is a symmetric, real convex set (i.e., for any element `x` in `s`, `-x` is also in `s`), and the measure of `F` multiplied by 2 raised to the power of the rank of the real vector space `E` is less than the measure of `s`, then there exists a non-zero element `x` in `s` that belongs to the lattice formed by the subgroup `L`.
In simpler terms, it asserts that if a convex symmetric domain `s` in the vector space `E` is large enough compared to the covolume of a lattice `L` of `E`, then it contains a non-zero lattice point of `L`. This theorem is fundamental in the theory of lattices and has applications in number theory and geometry.
More concisely: If `μ` is a finite Add Haar Measure on a Borel space `E`, a normed vector space with a countable subgroup `L`, and a symmetric, convex set `s` satisfies `μ(F) ≤ μ(s)^(dim E)` for any fundamental domain `F` of `L`, then `s` contains a non-zero lattice point from `L`.
|