OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedTopOffchild.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

On a unary block, the actual off-child packet sum with original smooth-selector coefficients is exponentially small. The proof retains its lost-mass factor and uses only the precise raw-interval concentration, top masks and the actual eligibility geometry.

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