OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedTopConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-selector concentration for the assigned top families, recentered at their own slopes. All source bounds concern the original labels and selected packets. Neither restriction introduces multiplicity or changes the analyzing coefficient.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_assigned_top_selector_concentration line 17