OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source selector support and local slope-label multiplicity instantiate the pointwise overlap budget in the single-scale estimate. The bound is uniform in the number of labels and Hilbert coordinates.

  1. theorem OAI.LipschitzHilbert.source_selector_single_scale line 15