GridCount.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Candidate grid counts in any ambient dimension

The remaining unknown cell in a retained graph edge is confined to a small ball. Its integer coordinate labels therefore lie in a product of short integer intervals. This gives the dimension-dependent degree factor.

def OAI.Falconer.scaledGridPoint line 19
Source documentation
Grid centers with mesh s⁻¹. A common fixed translation cancels in all pair differences and so does not enter the counting argument.
```
noncomputable def scaledGridPoint {d : ℕ} (s : ℝ) (z : Fin d → ℤ) : Space d :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.scaledGridPoint_apply line 22

theorem OAI.Falconer.grid_coordinate_bound line 26

Source documentation

Euclidean distance bounds every integer coordinate difference.

theorem grid_coordinate_bound {d L : ℕ} {s r : ℝ} (hs : 0 < s)
    (hL : r * s ≤ L) {z w : Fin d → ℤ}
    (hz : ‖scaledGridPoint s z - scaledGridPoint s w‖ ≤ r) (i : Fin d) :
    |z i - w i| ≤ (L : ℤ) := by
…

Mentions: OAI.Falconer.scaledGridPoint

theorem OAI.Falconer.grid_box_card line 38

Source documentation

A finite family in a coordinate box has at most (2L+1)^d labels.

theorem grid_box_card {d L : ℕ} (S : Finset (Fin d → ℤ)) (w : Fin d → ℤ)
    (hS : ∀ z ∈ S, ∀ i, |z i - w i| ≤ (L : ℤ)) :
    S.card ≤ (2 * L + 1)^d := by
…

theorem OAI.Falconer.grid_ball_card line 66

Source documentation

Ball count at a chosen grid center, with explicit integer radius.

theorem grid_ball_card {d L : ℕ} {s r : ℝ} (hs : 0 < s) (hL : r * s ≤ L)
    (S : Finset (Fin d → ℤ)) (w : Fin d → ℤ)
    (hS : ∀ z ∈ S, ‖scaledGridPoint s z - scaledGridPoint s w‖ ≤ r) :
    S.card ≤ (2 * L + 1)^d :=
…

Mentions: OAI.Falconer.scaledGridPoint

theorem OAI.Falconer.retained_grid_card line 74

Source documentation

In the retained graph, the scalar and perpendicular tests give exactly this grid count. No transversality condition between cap directions is used.

theorem retained_grid_card {d L : ℕ} {s τ c : ℝ} (hs : 0 < s) (hL : 4 * τ * s ≤ L)
    (S : Finset (Fin d → ℤ)) (w : Space d) (hw : ‖w‖ = 1)
    (hlong : ∀ z ∈ S, |inner ℝ w (scaledGridPoint s z) - c| ≤ τ)
    (hperp : ∀ z ∈ S, ‖perpendicularPart w (scaledGridPoint s z)‖ ≤ τ) :
    S.card ≤ (2 * L + 1)^d := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.scaledGridPoint, OAI.Falconer.perpendicularPart

theorem OAI.Falconer.retained_grid_card_translated line 91

Source documentation

The same count with an arbitrary common origin for the displacement tests. The grid itself need not be centered at the origin of the tube.

theorem retained_grid_card_translated {d L : ℕ} {s τ c : ℝ}
    (hs : 0 < s) (hL : 4 * τ * s ≤ L)
    (S : Finset (Fin d → ℤ)) (w u : Space d) (hw : ‖w‖ = 1)
    (hlong : ∀ z ∈ S, |inner ℝ w (scaledGridPoint s z - u) - c| ≤ τ)
    (hperp : ∀ z ∈ S, ‖perpendicularPart w (scaledGridPoint s z - u)‖ ≤ τ) :
    S.card ≤ (2 * L + 1)^d := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.scaledGridPoint, OAI.Falconer.perpendicularPart