OAI/Analysis/LipschitzHilbert/Trees/SourceMarkedResidual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full residual square controls every marked prefix chosen later by the spatial mass stopping rule. No choice of marks costs a factor.

  1. theorem OAI.LipschitzHilbert.marked_prefix_square_le line 13