Restricting a weight to selected thin slabs

A finite union bound controls the mass removed by intersecting thin slabs. The stage errors form a geometric sum, leaving enough thickness outside the maximal space of selected directions. Retained points also have bounded integer coordinates in the selected directions.

noncomputable def EGZ.restrictWeight {α : Type u_1} (w : α → ℕ) (S : Set α) : α → ℕ

Delete all mass outside a set.

Equations

• EGZ.restrictWeight w S v = if v ∈ S then w v else 0

theorem EGZ.restrictWeight_le {α : Type u_1} (w : α → ℕ) (S : Set α) : restrictWeight w S ≤ w

@[simp]

theorem EGZ.restrictWeight_ne_zero_iff {α : Type u_1} (w : α → ℕ) (S : Set α) (v : α) : restrictWeight w S v ≠ 0 ↔ v ∈ S ∧ w v ≠ 0

@[simp]

theorem EGZ.natMass_restrictWeight {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) : natMass (restrictWeight w S) = natMassOn w S

theorem EGZ.restrictWeight_loss_eq_compl {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) : ↑(natMass w) - ↑(natMass (restrictWeight w S)) = ↑(natMassOn w Sᶜ)

theorem EGZ.natMassOn_compl_intersection_le {α : Type u_1} {I : Type u_2} [Fintype α] [Fintype I] (w : α → ℕ) (S : I → Set α) : natMassOn w {v : α | ∀ (i : I), v ∈ S i}ᶜ ≤ ∑ i : I, natMassOn w (S i)ᶜ

Finite union bound for the mass outside an intersection.

theorem EGZ.restrictWeight_intersection_loss_le {α : Type u_1} {I : Type u_2} [Fintype α] [Fintype I] (w : α → ℕ) (S : I → Set α) (ε : I → ℝ) (hS : ∀ (i : I), ↑(natMassOn w (S i)ᶜ) ≤ ε i * ↑(natMass w)) : ↑(natMass w) - ↑(natMass (restrictWeight w {v : α | ∀ (i : I), v ∈ S i})) ≤ (∑ i : I, ε i) * ↑(natMass w)

Relative complement bounds add when the retained sets are intersected.

theorem EGZ.restrictWeight_retainedMass_ge {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) (ε : ℝ) (hloss : ↑(natMass w) - ↑(natMass (restrictWeight w S)) ≤ ε * ↑(natMass w)) : (1 - ε) * ↑(natMass w) ≤ ↑(natMass (restrictWeight w S))

theorem EGZ.restrictWeight_nonzero_of_loss_lt_one {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) (ε : ℝ) (hw : ∃ (v : α), w v ≠ 0) (hε : ε < 1) (hloss : ↑(natMass w) - ↑(natMass (restrictWeight w S)) ≤ ε * ↑(natMass w)) : ∃ (v : α), restrictWeight w S v ≠ 0

theorem EGZ.IsThinAlong.compl_mass_le {p d : ℕ} [NeZero p] {w : FpCoord p d → ℕ} {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} {t : ℕ} {ε : ℝ} (h : IsThinAlong w ξ t ε) : ↑(natMassOn w (slab ξ t)ᶜ) ≤ ε * ↑(natMass w)

def EGZ.slabIntersection {p d : ℕ} (k : ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (t : ℕ → ℕ) : Set (FpCoord p d)

The intersection of the first k stage-indexed slabs.

Equations

• EGZ.slabIntersection k ξ t = {v : EGZ.FpCoord p d | ∀ (i : Fin k), v ∈ EGZ.slab (ξ ↑i) (t (↑i + 1))}

theorem EGZ.sum_three_pow_succ_le (k : ℕ) : ∑ i : Fin k, 3 ^ (↑i + 1) ≤ 3 ^ (k + 1) - 1

theorem EGZ.DirectionChain.slabIntersection_loss_le_sum {p d k : ℕ} [Fact (Nat.Prime p)] {W : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)} {w : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain W (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) : ↑(natMass w) - ↑(natMass (restrictWeight w (slabIntersection k D.direction t))) ≤ (∑ i : Fin k, 3 ^ (↑i + 1) * δ) * ↑(natMass w)

theorem EGZ.DirectionChain.slabIntersection_loss_le {p d k : ℕ} [Fact (Nat.Prime p)] {W : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)} {w : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain W (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) (hδ : 0 ≤ δ) : ↑(natMass w) - ↑(natMass (restrictWeight w (slabIntersection k D.direction t))) ≤ (3 ^ (k + 1) - 1) * δ * ↑(natMass w)

theorem EGZ.DirectionChain.slabIntersection_loss_le_dimension {p d k : ℕ} [Fact (Nat.Prime p)] {W : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)} {w : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain W (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) (hδ : 0 ≤ δ) (hkd : k ≤ d) : ↑(natMass w) - ↑(natMass (restrictWeight w (slabIntersection k D.direction t))) ≤ 3 ^ (d + 1) * δ * ↑(natMass w)

theorem EGZ.DirectionChain.slabIntersection_retainedMass_ge {p d k : ℕ} [Fact (Nat.Prime p)] {W : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)} {w : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain W (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) (hδ : 0 ≤ δ) (hkd : k ≤ d) : (1 - 3 ^ (d + 1) * δ) * ↑(natMass w) ≤ ↑(natMass (restrictWeight w (slabIntersection k D.direction t)))

theorem EGZ.DirectionChain.slabIntersection_nonzero {p d k : ℕ} [Fact (Nat.Prime p)] {W : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)} {w : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain W (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) (hδ : 0 ≤ δ) (hkd : k ≤ d) (hsmall : 3 ^ (d + 1) * δ < 1) (hw : ∃ (v : FpCoord p d), w v ≠ 0) : ∃ (v : FpCoord p d), restrictWeight w (slabIntersection k D.direction t) v ≠ 0

theorem EGZ.DirectionChain.thick_slabIntersection {p d k : ℕ} [Fact (Nat.Prime p)] {W : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)} {w : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain W (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) (hδ : 0 ≤ δ) {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} (hthick : IsThickAlong w ξ (t (k + 1)) (3 ^ (k + 1) * δ)) : IsThickAlong (restrictWeight w (slabIntersection k D.direction t)) ξ (t (k + 1)) δ

The geometric error budget leaves thickness δ after intersecting all chosen slabs. No monotonicity assumptions on the widths are needed.

theorem EGZ.DirectionChain.thick_slabIntersection_of_maximal {p d k : ℕ} [Fact (Nat.Prime p)] {W : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)} {w : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain W (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong w ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) (hδ : 0 ≤ δ) (hmax : ∀ ξ ∉ D.space k, IsThickAlong w ξ (t (k + 1)) (3 ^ (k + 1) * δ)) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (hξ : ξ ∉ D.space k) : IsThickAlong (restrictWeight w (slabIntersection k D.direction t)) ξ (t (k + 1)) δ

theorem EGZ.HasBoundedRepresentative.valMinAbs_natAbs_le {p K : ℕ} [NeZero p] {a : ZMod p} (ha : HasBoundedRepresentative p K a) (hK : 2 * K < p) : a.valMinAbs.natAbs ≤ K

A small bounded representative agrees with the centered representative.

def EGZ.slabCoordinates {p d : ℕ} (k : ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (v : FpCoord p d) : IntCoord k

Integer coordinates supplied by the selected affine functionals.

Equations

• EGZ.slabCoordinates k ξ v i = ((ξ ↑i) v).valMinAbs

@[simp]

theorem EGZ.slabCoordinates_mod {p d k : ℕ} (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (v : FpCoord p d) : IntCoord.mod p (slabCoordinates k ξ v) = fun (i : Fin k) => (ξ ↑i) v

theorem EGZ.slabCoordinates_apply_bound {p d k : ℕ} [NeZero p] (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (t : ℕ → ℕ) {v : FpCoord p d} (hv : v ∈ slabIntersection k ξ t) (i : Fin k) (hsmall : 2 * t (↑i + 1) < p) : (slabCoordinates k ξ v i).natAbs ≤ t (↑i + 1)

theorem EGZ.slabCoordinates_bound {p d k : ℕ} [NeZero p] (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (t : ℕ → ℕ) (ht : Monotone t) (hsmall : ∀ (i : Fin k), 2 * t (↑i + 1) < p) {v : FpCoord p d} (hv : v ∈ slabIntersection k ξ t) : latticeSupNorm (slabCoordinates k ξ v) ≤ t k