OAI/Analysis/LipschitzHilbert/Estimates/ClippedSlopeBox.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Horizontal clipping before Euclidean enclosure. The width of the clipped interval is bounded by both the testing strip and the original dilation; no large horizontal dilation enters the long-side restriction.

  1. def OAI.LipschitzHilbert.SlopeBox.clipLeft line 14
  2. def OAI.LipschitzHilbert.SlopeBox.clipRight line 15
  3. def OAI.LipschitzHilbert.SlopeBox.clipLength line 16
  4. def OAI.LipschitzHilbert.SlopeBox.clipCenter line 18
  5. theorem OAI.LipschitzHilbert.SlopeBox.clipLength_le_strip line 22
  6. theorem OAI.LipschitzHilbert.SlopeBox.clipLength_le_dilation line 26
  7. theorem OAI.LipschitzHilbert.SlopeBox.clipped_coordinates line 31
  8. theorem OAI.LipschitzHilbert.SlopeBox.clipLength_pos_of_positive_witness line 53