OAI/NumberTheory/DukePrimeDegree/Entropy/FutureShiftBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Boundedness and finite mass survive the one-step future shift

  1. theorem OAI.DukePrimeDegree.EliminationChain.ae_bounded_one_future_of_zero line 16
  2. theorem OAI.DukePrimeDegree.EliminationChain.ae_one_future_mass_pos_ne_top line 35