OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalInsignificant.lean

GitHub source file

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.

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