The origin is a lattice point
ProvedQFS.zero_mem_latticeanalysismeasure-theoryquadratic-forms-sobolev
Let denote the integer lattice lattice d, the set of points
of EuclideanSpace ℝ (Fin d) all of whose coordinates are integers. Then
Trivial as it is, this is the lemma that supplies a base point for the discrete constructions: the lattice is non-empty, so arguments that pick a lattice point of minimal distance to a given target, or that start a chain of jumps at a lattice site, always have somewhere to begin.
Formalization Note. The dimension is implicit and unconstrained; for the space is a single point and the statement is still true.
Preamble
-- Generated by skeleton subtraction from QuadraticFormsSobolev/Section5.lean
-- source: quadratic-forms-sobolev@7a1a680db212
/-
Section 5 of Bux–Kassmann–Schulze, "Chaining and renormalization", auxiliary
results: Lemmas 5.1, 5.2, 5.4 and 5.5, the quantitative discrete counterparts of
the Section 4 lemmas.
The point of the discrete setting is to keep track of how far an edge path may
wander, so connectivity is taken here inside a prescribed set of vertices.
-/
import Definitions.Def_QFS_Translate
import Definitions.Def_QFS_Defs
import Definitions.Def_QFS_ConeGap
import Definitions.Def_QFS_RefCones
import Definitions.Def_QFS_Section4
import Definitions.Def_QFS_Cubes
import Definitions.Def_QFS_Section3
import Definitions.Def_QFS_Section5
import Mathlib
set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3
open Real Set Metric
open QFS
variable {d : ℕ}
/-! ## Lattice points are `√d/2`-dense
"Any closed ball of radius `√d/2` contains a lattice point." -/
/-! ## Connectivity inside a prescribed set of vertices
Definition 5.3 speaks of edge paths "not leaving `B_R(x)`", so unlike `Conn` of
Section 4 — where intermediate vertices were unconstrained — every vertex of the
path is now required to lie in a given set. -/
variable {Γ : Configuration (EuclideanSpace ℝ (Fin d))}
{S S' : Set (EuclideanSpace ℝ (Fin d))}
/-! ## Lemma 5.1: producing lattice points inside cones -/
/-! ## Corollary 5.2, Definition 5.3, Lemmas 5.4 and 5.5 -/
variable {ϑ : ℝ}
/-! ## Lemma 5.6: bounded jumps toward the tip -/
/-! ## Descent by bounded jumps
Lemma 5.6 continues: "I.e., we can go from `x` within `V` to a lattice point of
minimum distance to the tip via a chain of jumps each bounded in length from
above by `δ`." That clause is a general consequence of the local statement, and
is what the induction of Lemma 5.7 consumes; we record it separately.
The descent terminates because squared distances between lattice points are
natural numbers. -/Formal statement
lemma QFS.zero_mem_lattice : (0 : EuclideanSpace ℝ (Fin d)) ∈ lattice d := by sorry
Source