Zspan.isAddFundamentalDomain
theorem Zspan.isAddFundamentalDomain :
∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Basis ι ℝ E)
[inst_2 : Finite ι] [inst_3 : MeasurableSpace E] [inst_4 : OpensMeasurableSpace E] (μ : MeasureTheory.Measure E),
MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup)
(Zspan.fundamentalDomain b) μ
This theorem states that for a basis `b` of a normed space over the real numbers, the set defined by the function `Zspan.fundamentalDomain` is an additive fundamental domain for the ℤ-lattice generated by the basis `b`. An additive fundamental domain is a set that "tiles" the entire space under the action of addition by elements of the lattice, without overlaps or gaps. In the specific case, the lattice is the set of all integer linear combinations of the basis vectors, and the fundamental domain is constructed such that for every point `m` in it, the coefficients of its representation in terms of the basis `b` are in the interval [0, 1). The measure `μ` is assumed to be a measure on the normed space, and the space is assumed to have a finite basis and to be both measurable and open.
More concisely: The set defined by `Zspan.fundamentalDomain` for a real normed space's basis `b` is an additive fundamental domain for the lattice of integer linear combinations of `b`, where each point's representation in terms of `b` has coefficients in [0, 1).
|
Zspan.fract_eq_self
theorem Zspan.fract_eq_self :
∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedLinearOrderedField K] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace K E] {b : Basis ι K E} [inst_3 : FloorRing K] [inst_4 : Fintype ι] {x : E},
Zspan.fract b x = x ↔ x ∈ Zspan.fundamentalDomain b
The theorem `Zspan.fract_eq_self` states that for any type `E`, `ι`, and `K`, where `K` is a normed linear ordered field, `E` is a normed add commutative group, and `E` is a normed space over `K`, given a basis `b` of type `Basis ι K E` (i.e., a basis of `E` over `K` indexed by `ι`), a floor ring over `K`, and a `Fintype ι`, a vector `x` in `E` is in the fundamental domain of the lattice spanned by `b` if and only if applying the `Zspan.fract` operation to `x` results in `x` itself. Here, the `Zspan.fract` operation is defined as the vector `x` minus an integral vector obtained via the `Zspan.floor` function. The fundamental domain of a lattice is the set of all vectors `m` such that for all indices `i`, the `i`-th coordinate of the representation of `m` in the basis `b` lies in the half-open interval `[0, 1)`.
More concisely: Given a normed linear ordered field `K`, a normed add commutative group `E` that is a normed space over `K`, a basis `b` of `E` over `K`, and a vector `x` in `E`, `x` lies in the fundamental domain of the lattice spanned by `b` if and only if `x = Zspan.fract x`.
|