Level-one witnesses for the weighted lattice

The atom with index (c, r) ∈ ℤ² sits at (c · hgap, r · vgap) and has mass colWeight c, which is 1 for even c and heavy for odd c. A witness for the point (x, y) is a side L ≥ 1 and a finite set A of atoms, all within sup-distance L/2 of (x, y), of total mass at least L²: the closed square of side L centred at (x, y) then has average at least 1.

Six explicit witnesses cover the quarter cell [0, hgap] × [0, vgap/2] except one open slot (exists_isWitness_of_nonneg). Reflections in the two axes and translations by the period (2 hgap, vgap) preserve the atom masses, so they transport witnesses to the whole plane.

noncomputable def LeanPool.CenteredMaximal.Lattice.colWeight (c : ℤ) : ℝ

The mass of an atom in column c: 1 if c is even, heavy if c is odd.

Equations

• LeanPool.CenteredMaximal.Lattice.colWeight c = if Even c then 1 else LeanPool.CenteredMaximal.Lattice.heavy

def LeanPool.CenteredMaximal.Lattice.IsWitness (x y L : ℝ) (A : Finset (ℤ × ℤ)) : Prop

(L, A) witnesses level one at (x, y): L ≥ 1, the atoms of A have total mass at least L², and every atom of A lies in the closed square of side L centred at (x, y).

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.CenteredMaximal.Lattice.nearBox (k l : ℤ) : Finset (ℤ × ℤ)

The atoms that a witness for a point of the period cell with index (k, l) may use.

Equations

• LeanPool.CenteredMaximal.Lattice.nearBox k l = Finset.Icc (2 * k - 2) (2 * k + 2) ×ˢ Finset.Icc (l - 1) (l + 1)

def LeanPool.CenteredMaximal.Lattice.negFst : ℤ × ℤ ≃ ℤ × ℤ

Reflection of atom indices in the vertical axis.

Equations

• LeanPool.CenteredMaximal.Lattice.negFst = Equiv.prodCongr (Equiv.neg ℤ) (Equiv.refl ℤ)

def LeanPool.CenteredMaximal.Lattice.negSnd : ℤ × ℤ ≃ ℤ × ℤ

Reflection of atom indices in the horizontal axis.

Equations

• LeanPool.CenteredMaximal.Lattice.negSnd = (Equiv.refl ℤ).prodCongr (Equiv.neg ℤ)

@[simp]

theorem LeanPool.CenteredMaximal.Lattice.coe_negFst : ⇑negFst = fun (p : ℤ × ℤ) => (-p.1, p.2)

negFst negates the first coordinate.

@[simp]

theorem LeanPool.CenteredMaximal.Lattice.coe_negSnd : ⇑negSnd = fun (p : ℤ × ℤ) => (p.1, -p.2)

negSnd negates the second coordinate.

theorem LeanPool.CenteredMaximal.Lattice.colWeight_neg (c : ℤ) : colWeight (-c) = colWeight c

theorem LeanPool.CenteredMaximal.Lattice.colWeight_add_two_mul (c k : ℤ) : colWeight (c + 2 * k) = colWeight c

theorem LeanPool.CenteredMaximal.Lattice.IsWitness.neg_fst {x y L : ℝ} {A : Finset (ℤ × ℤ)} (hw : IsWitness x y L A) : IsWitness (-x) y L (Finset.map negFst.toEmbedding A)

Reflecting the atoms in the vertical axis (negFst, c ↦ -c) turns a witness for (x, y) into a witness for (-x, y) with the same side; IsWitness.neg_snd is the horizontal analogue.

theorem LeanPool.CenteredMaximal.Lattice.IsWitness.neg_snd {x y L : ℝ} {A : Finset (ℤ × ℤ)} (hw : IsWitness x y L A) : IsWitness x (-y) L (Finset.map negSnd.toEmbedding A)

Reflecting the atoms in the horizontal axis (negSnd, r ↦ -r) turns a witness for (x, y) into a witness for (x, -y) with the same side; IsWitness.neg_fst is the vertical analogue.

theorem LeanPool.CenteredMaximal.Lattice.IsWitness.translate {x y L : ℝ} {A : Finset (ℤ × ℤ)} (hw : IsWitness x y L A) (k l : ℤ) : IsWitness (x + 2 * ↑k * hgap) (y + ↑l * vgap) L (Finset.map (Equiv.toEmbedding (Equiv.addRight (2 * k, l))) A)

Translating the atoms by (2 * k, l) turns a witness for (x, y) into a witness for (x + 2 * k * hgap, y + l * vgap) with the same side. The column shift is even because colWeight has period 2 (colWeight_add_two_mul); map_addRight_subset_nearBox tracks the moved atoms.

theorem LeanPool.CenteredMaximal.Lattice.map_negFst_subset_nearBox {A : Finset (ℤ × ℤ)} (hA : A ⊆ nearBox 0 0) : Finset.map negFst.toEmbedding A ⊆ nearBox 0 0

Reflecting in the vertical axis (negFst) keeps a subset of nearBox 0 0 inside nearBox 0 0: the atom-set companion of IsWitness.neg_fst.

theorem LeanPool.CenteredMaximal.Lattice.map_negSnd_subset_nearBox {A : Finset (ℤ × ℤ)} (hA : A ⊆ nearBox 0 0) : Finset.map negSnd.toEmbedding A ⊆ nearBox 0 0

Reflecting in the horizontal axis (negSnd) keeps a subset of nearBox 0 0 inside nearBox 0 0: the atom-set companion of IsWitness.neg_snd.

theorem LeanPool.CenteredMaximal.Lattice.map_addRight_subset_nearBox {A : Finset (ℤ × ℤ)} (hA : A ⊆ nearBox 0 0) (k l : ℤ) : Finset.map (Equiv.toEmbedding (Equiv.addRight (2 * k, l))) A ⊆ nearBox k l

Translating a subset of nearBox 0 0 by (2 * k, l) lands in nearBox k l: the atom-set companion of IsWitness.translate.

The six witnesses

theorem LeanPool.CenteredMaximal.Lattice.isWitness_light {x y : ℝ} (hx : |x| ≤ 1 / 2) (hy : |y| ≤ 1 / 2) : IsWitness x y 1 {(0, 0)}

The light atom at the origin, side 1.

theorem LeanPool.CenteredMaximal.Lattice.isWitness_hlh2 {x y : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1 / 2) (hy : 1 / 2 ≤ y) (hy' : y ≤ vgap / 2) : IsWitness x y (2 * hgap + 1) {(-1, 0), (0, 0), (1, 0), (-1, 1), (0, 1), (1, 1)}

Heavy, light, heavy atoms (columns -1, 0, 1) in rows 0 and 1, side 2 hgap + 1; their total mass 4 heavy + 2 is exactly the area (2 hgap + 1)².

theorem LeanPool.CenteredMaximal.Lattice.isWitness_lh1 {x y : ℝ} (hx : 1 / 2 ≤ x) (hx' : x ≤ root / 2) (hy : 0 ≤ y) (hy' : y ≤ root / 2) : IsWitness x y root {(0, 0), (1, 0)}

A light and a heavy atom (columns 0, 1) in row 0, side root; their total mass 1 + heavy is exactly the area root².

theorem LeanPool.CenteredMaximal.Lattice.isWitness_lh2 {x y : ℝ} (hx : 1 / 2 ≤ x) (hx' : x ≤ sideLH2 / 2) (hy : vgap - sideLH2 / 2 ≤ y) (hy' : y ≤ vgap / 2) : IsWitness x y sideLH2 {(0, 0), (1, 0), (0, 1), (1, 1)}

Light and heavy atoms (columns 0, 1) in rows 0 and 1, side sideLH2; their total mass 2 (1 + heavy) is exactly the area sideLH2².

theorem LeanPool.CenteredMaximal.Lattice.isWitness_h1 {x y : ℝ} (hx : hgap - sideH1 / 2 ≤ x) (hx' : x ≤ hgap) (hy : 0 ≤ y) (hy' : y ≤ sideH1 / 2) : IsWitness x y sideH1 {(1, 0)}

One heavy atom (column 1, row 0), side sideH1; its mass heavy is exactly the area sideH1².

theorem LeanPool.CenteredMaximal.Lattice.isWitness_lhl2 {x y : ℝ} (hx : 2 * hgap - sideLHL2 / 2 ≤ x) (hx' : x ≤ hgap) (hy : vgap - sideLHL2 / 2 ≤ y) (hy' : y ≤ vgap / 2) : IsWitness x y sideLHL2 {(0, 0), (1, 0), (2, 0), (0, 1), (1, 1), (2, 1)}

Light, heavy, light atoms (columns 0, 1, 2) in rows 0 and 1, side sideLHL2; their total mass 2 (2 + heavy) is exactly the area sideLHL2².

Coverage

theorem LeanPool.CenteredMaximal.Lattice.exists_isWitness_of_nonneg {x y : ℝ} (hx : 0 ≤ x) (hx' : x ≤ hgap) (hy : 0 ≤ y) (hy' : y ≤ vgap / 2) (hslot : ¬(root / 2 < x ∧ x < 2 * hgap - sideLHL2 / 2 ∧ sideH1 / 2 < y ∧ y < vgap - sideLH2 / 2)) : ∃ (L : ℝ), ∃ A ⊆ nearBox 0 0, IsWitness x y L A

The six witnesses cover the quarter cell [0, hgap] × [0, vgap/2] except the open slot (root/2, 2 hgap - sideLHL2/2) × (sideH1/2, vgap - sideLH2/2), using only atoms of nearBox 0 0. exists_isWitness_of_abs extends this to the whole period cell by reflection.

theorem LeanPool.CenteredMaximal.Lattice.exists_isWitness_of_abs {x y : ℝ} (hx : |x| ≤ hgap) (hy : |y| ≤ vgap / 2) (hslot : ¬(root / 2 < |x| ∧ |x| < 2 * hgap - sideLHL2 / 2 ∧ sideH1 / 2 < |y| ∧ |y| < vgap - sideLH2 / 2)) : ∃ (L : ℝ), ∃ A ⊆ nearBox 0 0, IsWitness x y L A

Every point of the period cell [-hgap, hgap] × [-vgap/2, vgap/2] outside the open slot of exists_isWitness_of_nonneg and its reflections in one or both axes has a level-one witness whose atoms lie in nearBox 0 0. This is the whole-cell form of exists_isWitness_of_nonneg; exists_isWitness_of_mem_goodCopy moves it to the cell with index (k, l).