OAI/Analysis/LipschitzHilbert/Estimates/ComparableSelectedSlab.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A comparable-length subfamily of an actual selection run has bounded mass in a local strip. The required width bounds follow from non-removal.

  1. theorem OAI.LipschitzHilbert.comparable_selected_slab line 14