SourceSupportedSelectorInsignificant.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Insignificant source nodes: the actual physical analyzing coefficients, alternate synthesis profiles, original length stopping and actual top masks give an exponentially small amplitude. The same radial shrink therefore removes the entire node, including the case of an empty eligible top set.

theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_supported_selector_insignificant_node line 19