OAI/Analysis/LipschitzHilbert/Trees/LineSamplingPath.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Total Schwartz paths for short-time sampling. Outside the interval needed in the proof the paths are extended by the identity.

  1. def OAI.LipschitzHilbert.PacketRepresentation.lineDirectionSchwartz line 15
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineDirectionSchwartz_apply line 18
  3. def OAI.LipschitzHilbert.PacketRepresentation.lineSamplingPath line 21
  4. def OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInversePath line 24
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingPath_apply line 27
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInversePath_apply line 31
  7. def OAI.LipschitzHilbert.PacketRepresentation.lineSamplingTangent line 35
  8. def OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverseTangent line 39
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingTangent_apply line 43
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverseTangent_apply line 49
  11. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingPath_hasDerivAt line 63
  12. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInversePath_hasDerivAt line 76