OAI/Analysis/LipschitzHilbert/Trees/LineSamplingL2Path.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded L2 sampling paths and their agreement with the Schwartz paths.

  1. def OAI.LipschitzHilbert.PacketRepresentation.lineSamplingL2Path line 15
  2. def OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverseL2Path line 20
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingL2Path_onSchwartz line 26
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverseL2Path_onSchwartz line 34
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingL2Path_bound line 42
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverseL2Path_bound line 49
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingTangent_eq line 56