OAI/Analysis/LipschitzHilbert/Geometry/CompactDirectionCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compact cutoffs of bounded Lipschitz directions, normalized to preserve the exact Lipschitz constant one.

  1. def OAI.LipschitzHilbert.PacketRepresentation.directionTent line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.directionTent_nonneg line 14
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.directionTent_le_one line 16
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.directionTent_zero line 22
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.directionTent_difference line 28
  6. def OAI.LipschitzHilbert.PacketRepresentation.compactDirectionCutoff line 37
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.compactDirectionCutoff_compact line 40
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.compactDirectionCutoff_bound line 47
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.compactDirectionCutoff_lipschitz line 58
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.compactDirectionCutoff_tendsto line 83