OAI/Analysis/LipschitzHilbert/Trees/SourceRecenteredSelectedTree.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The ordinary tree estimate for an actual selected packet set. Local angular multiplicity supplies the row count; empty ambient rows disappear.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_recentered_selected_tree_estimate line 14