OAI/Analysis/LipschitzHilbert/Estimates/ClippedAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The indicator average of the actual thin enclosing rectangle controls intersection with a dilated top. The area cost is explicitly quadratic.

  1. theorem OAI.LipschitzHilbert.SlopeBox.thinEnclosure_average line 14