OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-selector top concentration. The frozen main part uses only the active narrow labels; the angular error charges local multiplicity before convolution. Both pieces retain the original analyzing coefficients and arbitrary alternate synthesis profiles.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_source_selector_concentration line 18