AngularGainFinite.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite labelled incidence obstruction

The sampling argument in ang:planar-measures ends with finite point and line families. Their counting contradiction follows from the precise published Furstenberg input. All line families must use a common separated grid before cardinalities replace covering numbers. Direction labels remain distinct throughout the upper counting estimate.

theorem OAI.Falconer.labelled_line_union_card_le line 22

Source documentation

A labelled family bounds a union even when two labels have the same geometric coordinate. No identification of their fibers is required.

theorem labelled_line_union_card_le {ι : Type*} [DecidableEq ι]
    (P : Finset (Space 2)) (T : Space 2 → Finset (Space 2))
    (D : Finset ι) (U : ι → Finset (Space 2)) {L : ℝ}
    (hcover : ∀ x ∈ P, ∀ l ∈ T x, ∃ i ∈ D, l ∈ U i)
    (hU : ∀ i ∈ D, ((U i).card : ℝ) ≤ L) :
    ((P.biUnion T).card : ℝ) ≤ (D.card : ℝ) * L := by
…

Mentions: OAI.Falconer.Space

theorem OAI.Falconer.published_furstenberg_labelled_obstruction line 46

Source documentation

After the two sampling steps, fewer than δ^(-b-ε/4) labels with fewer than that many line cells per label contradict the published Furstenberg estimate. This is the final quantitative contradiction in the planar measure-incidence argument.

theorem published_furstenberg_labelled_obstruction
    (hpublished : PublishedPlanarFurstenberg) {b f : ℝ}
    (hb : 0 < b) (hb' : b ≤ 1 / 2) (hbf : b < f) (hf : f < 1) :
    ∃ ε δ₀ : ℝ, 0 < ε ∧ 0 < δ₀ ∧ δ₀ ≤ 1 ∧
    ∀ δ : ℝ, 0 < δ → δ < δ₀ →
    ∀ P : Finset (Space 2), P.Nonempty → InBoundedLineChart P →
      FiniteSeparatedAt δ P → NormalizedFiniteBallBound δ f (δ ^ (-ε)) P →
    ∀ T : Space 2 → Finset (Space 2),
      (∀ x ∈ P, (T x).Nonempty ∧ InBoundedLineChart (T x) ∧
        FiniteSeparatedAt δ (T x) ∧ NormalizedFiniteBallBound δ b (δ ^ (-ε)) (T x) ∧
        ∀ l ∈ T x, TubeIncident δ x l) →
    ∀ (ι : Type) [DecidableEq ι] (D : Finset ι) (U : ι → Finset (Space 2)),
…

Mentions: OAI.Falconer.PublishedPlanarFurstenberg, OAI.Falconer.Space, OAI.Falconer.InBoundedLineChart, OAI.Falconer.FiniteSeparatedAt, OAI.Falconer.NormalizedFiniteBallBound, OAI.Falconer.TubeIncident

def OAI.Falconer.lineGridRound line 81
Source documentation
Rounding a line coordinate to a grid of mesh δ.
```
noncomputable def lineGridRound (δ a : ℝ) : ℝ := δ * (round (a / δ) : ℝ)
```
theorem OAI.Falconer.lineGridRound_error line 83
def OAI.Falconer.roundedIncidentLine line 97
Source documentation
Choose the grid slope first, then the grid intercept nearest the exact line through the point. Every constructed line remains incident.
```
noncomputable def roundedIncidentLine (δ : ℝ) (x : Space 2) (m : ℝ) : Space 2 :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.roundedIncidentLine_fst line 101
theorem OAI.Falconer.roundedIncidentLine_snd line 104
theorem OAI.Falconer.roundedIncidentLine_incident line 108
theorem OAI.Falconer.roundedIncidentLine_near_strip line 122
Source documentation
A strip in one original direction contains only a bounded interval of grid intercepts after rounding that direction. The interval is uniform in its original label, so coincident directions need not share covers.
```
theorem roundedIncidentLine_near_strip {δ C a m : ℝ} (hδ : 0 < δ)
    (x : Space 2) (hx : |x 0| ≤ 1)
    (hstrip : |x 1 - m * x 0 - a| ≤ C * δ) :
    |roundedIncidentLine δ x m 1 - a| ≤ (C + 1) * δ := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.roundedIncidentLine