OAI/Analysis/LipschitzHilbert/Estimates/LocalSelectedWidths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Width bounds at the local interval scale, derived from actual non-removal rather than imposed as extra geometric assumptions.

  1. theorem OAI.LipschitzHilbert.local_selected_widths line 12