DyadicAncestors.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Ancestor groups for the retained graph witnesses

There are at most 2^(d*g) ancestor groups at relative depth g. All centers within one group lie in the same original dyadic cube, giving the diameter used in the parallel-test witness argument.

theorem OAI.Falconer.dyadic_ancestor_count line 18
theorem OAI.Falconer.DyadicCube.center_mem_ancestor line 27
theorem OAI.Falconer.DyadicCube.same_ancestor_center_dist line 37

theorem OAI.Falconer.DyadicCube.parallel_count line 51

Source documentation

One eligible point--angle witness per cell supplies the literal parallel test; the candidate count then costs only the number of actual dyadic ancestors, independently of their occupied masses.

theorem DyadicCube.parallel_count {d n g C : ℕ} (Q : DyadicCube d)
    (hQ : 0 < Q.side) (A : Finset (List (Fin d → Bool)))
    (hA : ∀ p ∈ A, p.length = n) (hg : g ≤ n)
    (w₀ base : Space d) (hw₀ : ‖w₀‖ = 1) {τ δ W : ℝ} (hδ : 0 ≤ δ)
    (hwidth : 2*τ + 2*δ*(Real.sqrt d * (Q.side/(2 : ℝ)^g)) ≤ W)
    (hwitness : ∀ a ∈ A, ∃ w : Space d, ‖w‖ = 1 ∧ ‖w-w₀‖ ≤ δ ∧
      (A.filter (fun z => z.take g = a.take g ∧
        ‖(Q.descendant z).center - (Q.descendant a).center‖ ≤
          Real.sqrt d * (Q.side/(2 : ℝ)^g) ∧
        ‖perpendicularPart w ((Q.descendant z).center - (Q.descendant a).center)‖ ≤ W)).card ≤ C) :
    (A.filter (fun z => ‖perpendicularPart w₀
      ((Q.descendant z).center - base)‖ ≤ τ)).card ≤ C*2^(d*g) := by
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.DyadicCube.center, OAI.Falconer.perpendicularPart