OAI/NumberTheory/PrimePackets/ObservationRefinement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Refining and recoding finite observations

  1. lemma OAI.PrimeDegreePackets.observationEntropy_injective line 15
  2. lemma OAI.PrimeDegreePackets.conditionalObservationEntropy_injective line 31
  3. lemma OAI.PrimeDegreePackets.conditionalObservationEntropy_comp_preserving line 44
  4. theorem OAI.PrimeDegreePackets.conditionalObservationEntropy_coarsening_le line 56
  5. theorem OAI.PrimeDegreePackets.conditionalObservationEntropy_pair_pair_le line 82
  6. lemma OAI.PrimeDegreePackets.observationEntropy_le_add_conditional line 99