OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationErrorPhysical.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted physical concentration of the original selector error. The analyzing coefficients are untouched; the alternate synthesis profile enters only through its common carrier-free raw bounds.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selector_error_top_neighborhood line 34