OAI/NumberTheory/Ostmann/Arithmetic/GuardedHistoryPair.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal product of both reconstructed history supports

  1. theorem OAI.Ostmann.guardedHistoryAmplitude_pair line 12
  2. theorem OAI.Ostmann.reconstructedHistoryAmplitude_pair line 28