OAI/NumberTheory/DukePrimeDegree/Geometry/TerminalNeutralPairs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bring neutral displacements at a terminal time back to the initial time

  1. theorem OAI.DukePrimeDegree.diagonal_negative_iterate_injective line 13
  2. theorem OAI.DukePrimeDegree.neutral_displacement_of_terminal line 19
  3. theorem OAI.DukePrimeDegree.fullFutureObservation_terminal line 35