GraphDegrees.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Degrees of the higher-dimensional retained graph

The vertex sets are the eligible depth-p grid cells for a fixed pair of caps. A parallel test controls the first unknown cell; the scalar constraint then controls the second, in its own cap direction.

theorem OAI.Falconer.perpendicularPart_neg line 17
def OAI.Falconer.retainedGridEdge line 24
Source documentation
The three center tests for a fixed pair of angular caps.
```
def retainedGridEdge {d : ℕ} (s : ℝ) (w₁ w₂ : Space d) (τ : ℝ)
    (row col : (Fin d → ℤ) × (Fin d → ℤ)) : Prop :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.retainedGridEdge_symm line 31
theorem OAI.Falconer.retainedGridEdge_swap line 39

theorem OAI.Falconer.pair_card_le line 48

Source documentation

Counting a finite set of pairs by its first-coordinate candidates and the uniformly bounded second-coordinate fibers.

theorem pair_card_le {α β : Type*} [DecidableEq α] [DecidableEq β]
    (S : Finset (α × β)) (A : Finset α) (K : ℕ)
    (hA : ∀ z ∈ S, z.1 ∈ A)
    (hK : ∀ a ∈ A, ((S.filter (fun z => z.1 = a)).image Prod.snd).card ≤ K) :
    S.card ≤ K * A.card := by
…

theorem OAI.Falconer.retainedGrid_degree_first line 63

Source documentation

Row degree from the first endpoint's parallel-test count. The second endpoint only uses its unit cap direction and the grid packing bound.

theorem retainedGrid_degree_first {d L C : ℕ} {s τ : ℝ} (hs : 0 < s)
    (hL : 4 * τ * s ≤ L) (A B : Finset (Fin d → ℤ))
    (w₁ w₂ : Space d) (hw₂ : ‖w₂‖ = 1)
    (row : (Fin d → ℤ) × (Fin d → ℤ))
    (hparallel : (A.filter (fun z =>
      ‖perpendicularPart w₁ (scaledGridPoint s z - scaledGridPoint s row.1)‖ ≤ τ)).card ≤ C) :
    ((A ×ˢ B).filter (retainedGridEdge s w₁ w₂ τ row)).card ≤
      (2 * L + 1)^d * C := by
…

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

theorem OAI.Falconer.retainedGrid_degree_min line 95

Source documentation

Both choices of the first unknown are valid, so the smaller parallel count controls the degree.

theorem retainedGrid_degree_min {d L C₁ C₂ : ℕ} {s τ : ℝ} (hs : 0 < s)
    (hL : 4 * τ * s ≤ L) (A B : Finset (Fin d → ℤ))
    (w₁ w₂ : Space d) (hw₁ : ‖w₁‖ = 1) (hw₂ : ‖w₂‖ = 1)
    (row : (Fin d → ℤ) × (Fin d → ℤ))
    (h₁ : (A.filter (fun z =>
      ‖perpendicularPart w₁ (scaledGridPoint s z - scaledGridPoint s row.1)‖ ≤ τ)).card ≤ C₁)
    (h₂ : (B.filter (fun z =>
      ‖perpendicularPart w₂ (scaledGridPoint s z - scaledGridPoint s row.2)‖ ≤ τ)).card ≤ C₂) :
    ((A ×ˢ B).filter (retainedGridEdge s w₁ w₂ τ row)).card ≤
      (2 * L + 1)^d * min C₁ C₂ := by
…

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

theorem OAI.Falconer.retainedGrid_column_degree_min line 128

Source documentation

Reversing every edge gives the identical column degree bound.

theorem retainedGrid_column_degree_min {d L C₁ C₂ : ℕ} {s τ : ℝ} (hs : 0 < s)
    (hL : 4 * τ * s ≤ L) (A B : Finset (Fin d → ℤ))
    (w₁ w₂ : Space d) (hw₁ : ‖w₁‖ = 1) (hw₂ : ‖w₂‖ = 1)
    (col : (Fin d → ℤ) × (Fin d → ℤ))
    (h₁ : (A.filter (fun z =>
      ‖perpendicularPart w₁ (scaledGridPoint s z - scaledGridPoint s col.1)‖ ≤ τ)).card ≤ C₁)
    (h₂ : (B.filter (fun z =>
      ‖perpendicularPart w₂ (scaledGridPoint s z - scaledGridPoint s col.2)‖ ≤ τ)).card ≤ C₂) :
    ((A ×ˢ B).filter (fun row => retainedGridEdge s w₁ w₂ τ row col)).card ≤
      (2 * L + 1)^d * min C₁ C₂ := by
…

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