EligibleDyadicGraph.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The graph of eligible original cell--cap incidences

Support of an endpoint symbol in a literal parallel test supplies the witnesses used by the degree estimate. Eligibility only filters the finite cell list; no angular support is cut by a pointwise edge decision.

def OAI.Falconer.DyadicCube.eligiblePaths line 18
theorem OAI.Falconer.DyadicCube.eligiblePaths_subset line 24
theorem OAI.Falconer.DyadicParallelTest.mono line 29
theorem OAI.Falconer.DyadicCube.eligiblePaths_witnesses line 35
def OAI.Falconer.eligibleDyadicEdge line 52
theorem OAI.Falconer.eligibleDyadicEdge_symm line 57

theorem OAI.Falconer.eligibleDyadic_degree line 67

Source documentation

The degree bound holds inside any larger row list. Ineligible rows have degree zero; eligible rows are bounded using their original witnesses.

theorem eligibleDyadic_degree {d n g₁ g₂ L C₁ C₂ : ℕ}
    (Q₁ Q₂ : DyadicCube d) (hQ : 0 < Q₁.side) (hside : Q₂.side = Q₁.side)
    (A B : Finset (List (Fin d → Bool)))
    (hA : ∀ p ∈ A, p.length = n) (hB : ∀ p ∈ B, p.length = n)
    (hg₁ : g₁ ≤ n) (hg₂ : g₂ ≤ n)
    (w₁ w₂ : Space d) (hw₁ : ‖w₁‖ = 1) (hw₂ : ‖w₂‖ = 1)
    {τ δ W₁ W₂ : ℝ} (hδ : 0 ≤ δ)
    (hL : 4*τ*((2 : ℝ)^n/Q₁.side) ≤ L)
    (hwidth₁ : 2*τ+2*δ*(Real.sqrt d*(Q₁.side/(2 : ℝ)^g₁)) ≤ W₁)
    (hwidth₂ : 2*τ+2*δ*(Real.sqrt d*(Q₂.side/(2 : ℝ)^g₂)) ≤ W₂)
    (htest₁ : DyadicCapWitnesses Q₁ A g₁ w₁ δ W₁ C₁)
    (htest₂ : DyadicCapWitnesses Q₂ B g₂ w₂ δ W₂ C₂)
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.DyadicCapWitnesses