Fundamental domains of integer spans #
This file records geometric properties of the standard fundamental domain associated to a basis. Its convexity makes lattice cells preconnected, so cells crossing the boundary of a set can be detected by their intersection with the frontier in lattice-point counting arguments.
Main results #
ZSpan.convex_fundamentalDomain: the fundamental domain of a real basis is convex.ZSpan.eq_of_sub_mem_fundamentalDomain: two integer-span translates placing a point in the fundamental domain are equal.
theorem
ZSpan.convex_fundamentalDomain
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_2}
(β : Module.Basis ι ℝ E)
:
Convex ℝ (fundamentalDomain β)
The fundamental domain of a basis is convex: it is cut out by the conditions
b.repr x i ∈ [0, 1), one convex condition per coordinate.
theorem
ZSpan.eq_of_sub_mem_fundamentalDomain
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_2}
[Finite ι]
(β : Module.Basis ι ℝ E)
{x w₁ w₂ : E}
(hw₁ : w₁ ∈ Submodule.span ℤ (Set.range ⇑β))
(hw₂ : w₂ ∈ Submodule.span ℤ (Set.range ⇑β))
(h₁ : x - w₁ ∈ fundamentalDomain β)
(h₂ : x - w₂ ∈ fundamentalDomain β)
:
Two vectors in the integer span that translate the same point into the fundamental domain in subtraction form are equal.