ParallelCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Parallel tests and the first unknown cell

A cap incidence supplies a witness direction. Grouping eligible cells by their testing ancestor lets one witness control each group. The direction perturbation is handled in the original ambient space.

theorem OAI.Falconer.parallel_count_from_witnesses line 19

Source documentation

The geometric counting step in graph:degrees. The hypotheses are the literal parallel test at each eligible witness and the diameter of a common ancestor. In applications there are at most G testing ancestors.

theorem parallel_count_from_witnesses {E α β : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [DecidableEq α] [DecidableEq β]
    (A : Finset α) (center : α → E) (ancestor : α → β)
    (w₀ base : E) (hw₀ : ‖w₀‖ = 1) {τ δ L W : ℝ} (hδ : 0 ≤ δ)
    {C G : ℕ} (hgroups : (A.image ancestor).card ≤ G)
    (hwidth : 2 * τ + 2 * δ * L ≤ W)
    (hdiam : ∀ x ∈ A, ∀ y ∈ A, ancestor x = ancestor y →
      ‖center x - center y‖ ≤ L)
    (hwitness : ∀ a ∈ A, ∃ w : E, ‖w‖ = 1 ∧ ‖w - w₀‖ ≤ δ ∧
      (A.filter (fun z => ancestor z = ancestor a ∧
        ‖center z - center a‖ ≤ L ∧
…