ℤ-lattices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Let E be a finite dimensional vector space over a normed_linear_ordered_field K with a solid
norm and that is also a floor_ring, e.g. ℚ or ℝ. A (full) ℤ-lattice L of E is a discrete
subgroup of E such that L spans E over K.
The ℤ-lattice L can be defined in two ways:
- For
ba basis ofE, thensubmodule.span ℤ (set.range b)is a ℤ-lattice ofE. - As an
add_subgroup Ewith the additional properties:∀ r : ℝ, (L ∩ metric.closed_ball 0 r).finite, that isLis discretesubmodule.span ℝ (L : set E) = ⊤, that isLspansEoverK.
Main result #
zspan.is_add_fundamental_domain: for a ℤ-latticesubmodule.span ℤ (set.range b), proves that the set defined byzspan.fundamental_domainis a fundamental domain.
def
zspan.fundamental_domain
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E) :
set E
The fundamental domain of the ℤ-lattice spanned by b. See zspan.is_add_fundamental_domain
for the proof that it is the fundamental domain.
@[simp]
theorem
zspan.mem_fundamental_domain
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
{m : E} :
noncomputable
def
zspan.floor
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E) :
↥(submodule.span ℤ (set.range ⇑b))
The map that sends a vector of E to the element of the ℤ-lattice spanned by b obtained
by rounding down its coordinates on the basis b.
Equations
- zspan.floor b m = finset.univ.sum (λ (i : ι), ⌊⇑(⇑(b.repr) m) i⌋ • ⇑(basis.restrict_scalars ℤ b) i)
noncomputable
def
zspan.ceil
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E) :
↥(submodule.span ℤ (set.range ⇑b))
The map that sends a vector of E to the element of the ℤ-lattice spanned by b obtained
by rounding up its coordinates on the basis b.
Equations
- zspan.ceil b m = finset.univ.sum (λ (i : ι), ⌈⇑(⇑(b.repr) m) i⌉ • ⇑(basis.restrict_scalars ℤ b) i)
@[simp]
theorem
zspan.repr_floor_apply
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E)
(i : ι) :
@[simp]
theorem
zspan.repr_ceil_apply
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E)
(i : ι) :
@[simp]
theorem
zspan.floor_eq_self_of_mem
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E)
(h : m ∈ submodule.span ℤ (set.range ⇑b)) :
↑(zspan.floor b m) = m
@[simp]
theorem
zspan.ceil_eq_self_of_mem
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E)
(h : m ∈ submodule.span ℤ (set.range ⇑b)) :
↑(zspan.ceil b m) = m
noncomputable
def
zspan.fract
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E) :
E
The map that sends a vector E to the fundamental domain of the lattice,
see zspan.fract_mem_fundamental_domain.
Equations
- zspan.fract b m = m - ↑(zspan.floor b m)
theorem
zspan.fract_apply
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E) :
zspan.fract b m = m - ↑(zspan.floor b m)
@[simp]
theorem
zspan.repr_fract_apply
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E)
(i : ι) :
@[simp]
theorem
zspan.fract_fract
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E) :
zspan.fract b (zspan.fract b m) = zspan.fract b m
@[simp]
theorem
zspan.fract_zspan_add
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E)
{v : E}
(h : v ∈ submodule.span ℤ (set.range ⇑b)) :
zspan.fract b (v + m) = zspan.fract b m
@[simp]
theorem
zspan.fract_add_zspan
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m : E)
{v : E}
(h : v ∈ submodule.span ℤ (set.range ⇑b)) :
zspan.fract b (m + v) = zspan.fract b m
theorem
zspan.fract_eq_self
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
{b : basis ι K E}
[floor_ring K]
[fintype ι]
{x : E} :
zspan.fract b x = x ↔ x ∈ zspan.fundamental_domain b
theorem
zspan.fract_mem_fundamental_domain
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(x : E) :
theorem
zspan.fract_eq_fract
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(m n : E) :
zspan.fract b m = zspan.fract b n ↔ -m + n ∈ submodule.span ℤ (set.range ⇑b)
theorem
zspan.norm_fract_le
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
[has_solid_norm K]
(m : E) :
‖zspan.fract b m‖ ≤ finset.univ.sum (λ (i : ι), ‖⇑b i‖)
@[simp]
theorem
zspan.coe_floor_self
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[floor_ring K]
[fintype ι]
[unique ι]
(k : K) :
↑(zspan.floor (basis.singleton ι K) k) = ↑⌊k⌋
@[simp]
theorem
zspan.coe_fract_self
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[floor_ring K]
[fintype ι]
[unique ι]
(k : K) :
zspan.fract (basis.singleton ι K) k = int.fract k
theorem
zspan.fundamental_domain_bounded
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[finite ι]
[has_solid_norm K] :
theorem
zspan.vadd_mem_fundamental_domain
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[fintype ι]
(y : ↥(submodule.span ℤ (set.range ⇑b)))
(x : E) :
y +ᵥ x ∈ zspan.fundamental_domain b ↔ y = -zspan.floor b x
theorem
zspan.exist_unique_vadd_mem_fundamental_domain
{E : Type u_1}
{ι : Type u_2}
{K : Type u_3}
[normed_linear_ordered_field K]
[normed_add_comm_group E]
[normed_space K E]
(b : basis ι K E)
[floor_ring K]
[finite ι]
(x : E) :
∃! (v : ↥(submodule.span ℤ (set.range ⇑b))), v +ᵥ x ∈ zspan.fundamental_domain b
@[measurability]
theorem
zspan.fundamental_domain_measurable_set
{E : Type u_1}
{ι : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
(b : basis ι ℝ E)
[measurable_space E]
[opens_measurable_space E]
[finite ι] :
@[protected]
theorem
zspan.is_add_fundamental_domain
{E : Type u_1}
{ι : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
(b : basis ι ℝ E)
[finite ι]
[measurable_space E]
[opens_measurable_space E]
(μ : measure_theory.measure E) :
For a ℤ-lattice submodule.span ℤ (set.range b), proves that the set defined
by zspan.fundamental_domain is a fundamental domain.