OAI/NumberTheory/DukePrimeDegree/Entropy/AtomicRootEntropy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Vanishing transverse conditional entropy for atomic root products

  1. lemma OAI.DukePrimeDegree.observationEntropy_dirac_eq_zero line 13
  2. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_nonneg line 22
  3. theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalEntropy_fst_eq_zero_of_atomic_roots line 38
  4. theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalEntropy_eq_zero_of_atomic_roots line 62