OAI/Analysis/LipschitzHilbert/Phase/AngularCountBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.AngularGrid.independent_cells_card_le line 18

   Source documentation

   Select one significant top in each nonempty angular cell. Disjoint cells make this selection injective, and nonneighbors make its slopes separated. Thus the previously proved simultaneous list bound applies to every independent cell collection.

   theorem independent_cells_card_le {ι : Type*} [DecidableEq ι]
       (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox) (d : ι → ℝ)
       (z : ℝ × ℝ) (cutoff : ℝ) (base level : ℕ) (parent : ℤ)
       (cells : Finset ℤ) {rho B K D : ℝ}
       (hprecision : cutoff / (g.branching : ℝ) ^ level ≤ rho / B ^ 2)
       (hspan : g.width base ≤ B * rho)
       (hancestor : ∀ c ∈ cells,
         g.cellTops tops (fun i => (T i).slope) d cutoff level c ⊆
           g.cellTops tops (fun i => (T i).slope) d cutoff base parent)
       (hsignificant : ∀ c ∈ cells, ∃ i ∈ g.cellTops tops (fun i => (T i).slope) d cutoff level c,
         (T i).radius z ≤ K)
       (hindependent : (cells : Set ℤ).Pairwise (fun c e => ¬g.neighbors level rho c e))
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox