OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorNodeEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original smooth-selector analyzing coefficients and alternate synthesis satisfy the same actual source node envelope. The only analytic premise is raw-interval concentration for those exact original coefficients.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_selector_node_envelope line 17