OAI/Analysis/LipschitzHilbert/Estimates/SlopeAdmissibility.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Admissibility of the actual thin enclosing rectangle from a slope popularity witness, with an explicit short horizontal localization.

  1. theorem OAI.LipschitzHilbert.slopeRectangle_popular line 14
  2. theorem OAI.LipschitzHilbert.slopeRectangle_admissible line 30