OAI/NumberTheory/DukePrimeDegree/Entropy/FutureBlockInformation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Iterated whole-future masses

The same normalization factor occurs for every future index. In particular every later whole-future atom has positive finite mass once the zero-future atom does, despite the nonintegrable possible height.

  1. lemma OAI.DukePrimeDegree.EliminationChain.remainingFutureAtom_shift_index line 20
  2. theorem OAI.DukePrimeDegree.EliminationChain.ae_remainingTimeProduct_futureAtom_index line 32
  3. theorem OAI.DukePrimeDegree.EliminationChain.ae_all_futureMass_pos_ne_top line 55
  4. theorem OAI.DukePrimeDegree.EliminationChain.futureBlockInformation_integrable_integral line 95