OAI/NumberTheory/DukePrimeDegree/Entropy/FutureAtomCovariance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact covariance of actual whole-future leaf masses

  1. lemma OAI.DukePrimeDegree.normalized_mass_log_identity line 14
  2. theorem OAI.DukePrimeDegree.EliminationChain.ae_remainingTimeProduct_futureAtom line 29