OAI/Analysis/LipschitzHilbert/Trees/SourceTreeExitBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The ordinary amplitude envelope gives the actual mass-stop cost. No positive lower bound on a stopped top weight is needed.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_stop_exit_bound line 14