Exact lattice counts under an integral basis

The real basis extending an integral lattice basis maps lattice elements to integer coordinate vectors, preserving the count in every subset.

theorem NairTenenbaum.ofZLatticeBasis_equivFun_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℤ ↥L) (x : ↥L) : (Module.Basis.ofZLatticeBasis ℝ L b).equivFunL ↑x = integerLatticePoint (b.equivFun x)

theorem NairTenenbaum.integerLatticeCount_basis_image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℤ ↥L) (s : Set E) : integerLatticeCount (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFunL '' s) = Nat.card { x : ↥L // ↑x ∈ s }