OAI/Analysis/LipschitzHilbert/Geometry/SmoothDirectionApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual compact smooth approximants of a bounded Lipschitz direction.

  1. def OAI.LipschitzHilbert.PacketRepresentation.lineDirectionMollifier line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineDirectionMollifier_radius_tendsto line 19
  3. def OAI.LipschitzHilbert.PacketRepresentation.smoothDirectionApprox line 25
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.smoothDirectionApprox_lipschitz line 31
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.smoothDirectionApprox_bound line 35
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.smoothDirectionApprox_compact line 39
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.smoothDirectionApprox_tendsto line 43