OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationMain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted centered-main concentration on the actual active labels. The modulation constant is bounded by the narrow selector separation, so the wide angular-error cone never enters the main constant.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_main_concentration line 15