AngularGrid.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

A common line grid for the planar incidence obstruction

Each original strip gives a bounded list of common-grid line parameters. The list is attached to its original direction label. Rounding therefore turns the manuscript's covering-number upper bound into the cardinality upper bound needed by published_furstenberg_labelled_obstruction.

def OAI.Falconer.gridLine line 18
theorem OAI.Falconer.gridLine_fst line 21
theorem OAI.Falconer.gridLine_snd line 24
theorem OAI.Falconer.integer_grid_separation line 27
theorem OAI.Falconer.gridLine_dist_ge line 38
theorem OAI.Falconer.gridLine_injective line 55
theorem OAI.Falconer.gridLine_image_separated line 63
Source documentation
Every finite subfamily of the common line grid is δ-separated.
```
theorem gridLine_image_separated {δ : ℝ} (hδ : 0 < δ) (S : Finset (ℤ × ℤ)) :
    FiniteSeparatedAt δ (S.image (gridLine δ)) := by
…
```
Mentions: OAI.Falconer.FiniteSeparatedAt, OAI.Falconer.gridLine
theorem OAI.Falconer.roundedIncidentLine_family_separated line 73

theorem OAI.Falconer.roundedIncidentLine_in_chart line 87

Source documentation

A fixed smaller chart leaves room for rounding while staying inside the unit chart used by the published finite theorem.

theorem roundedIncidentLine_in_chart {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 2)
    (x : Space 2) (hx0 : |x 0| ≤ 1 / 4) (hx1 : |x 1| ≤ 1 / 4)
    (m : ℝ) (hm : |m| ≤ 1 / 2) :
    |roundedIncidentLine δ x m 0| ≤ 1 ∧ |roundedIncidentLine δ x m 1| ≤ 1 := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.roundedIncidentLine

def OAI.Falconer.roundedStripCandidates line 117
Source documentation
The bounded candidate intercept list for one strip, retaining its original slope label even if other labels have the same rounded slope.
```
noncomputable def roundedStripCandidates (δ m a : ℝ) (L : ℕ) : Finset (Space 2) :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.roundedStripCandidates_card_le line 121
theorem OAI.Falconer.roundedIncidentLine_mem_candidates line 134
Source documentation
A rounded line through any point of a strip belongs to that strip's bounded candidate list. This is the fixed-width loss in ang:planar-measures.
```
theorem roundedIncidentLine_mem_candidates {δ C a m : ℝ} (hδ : 0 < δ)
    (x : Space 2) (hx : |x 0| ≤ 1)
    (hstrip : |x 1 - m * x 0 - a| ≤ C * δ)
    (L : ℕ) (hL : C + 2 ≤ (L : ℝ)) :
    roundedIncidentLine δ x m ∈ roundedStripCandidates δ m a L := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.roundedIncidentLine, OAI.Falconer.roundedStripCandidates