OAI/NumberTheory/JointDickman/Amplification/ReindexedCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Reindexing partial output cells

  1. theorem OAI.JointDickman.optionCellMass_map_equiv line 12
  2. theorem OAI.JointDickman.partialFairPrimeTransition_map_equiv line 22
  3. theorem OAI.JointDickman.independentCellMarginal_map_equiv line 28
  4. def OAI.JointDickman.trivialResidueEquiv line 36
  5. def OAI.JointDickman.logarithmicCell line 42
  6. theorem OAI.JointDickman.logarithmicCell_mass line 46
  7. theorem OAI.JointDickman.logarithmicCell_primeProduct_mass line 52
  8. theorem OAI.JointDickman.logarithmicCell_marginal line 59