OAI/Analysis/LipschitzHilbert/Trees/SourceParentWidth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The parent residual cone fits the manuscript's physical packet width W=mw. The actual dyadic branching is much smaller than m; no enlargement of the source packet profiles is required.

  1. theorem OAI.LipschitzHilbert.SourceParameters.eventually_parent_reference_width line 14