OAI/Probability/DirectionalWalk/MarkedSums.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.sumKernel line 16
  2. instance OAI.DirectionalZeroOne.sumKernel_markov line 20
  3. def OAI.DirectionalZeroOne.markedSumLaw line 23
  4. instance OAI.DirectionalZeroOne.markedSumLaw_probability line 26
  5. lemma OAI.DirectionalZeroOne.markedSumLaw_atom line 30
  6. lemma OAI.DirectionalZeroOne.markedSumLaw_fst line 34
  7. lemma OAI.DirectionalZeroOne.markedSumLaw_conv line 38
  8. lemma OAI.DirectionalZeroOne.conditionalInfo_markedSum line 61
  9. lemma OAI.DirectionalZeroOne.markedSumLaw_conditional_entropy line 78
  10. lemma OAI.DirectionalZeroOne.commonBlock_integrable_total line 104
  11. lemma OAI.DirectionalZeroOne.commonGapLaw_lattice_integrable line 123
  12. lemma OAI.DirectionalZeroOne.markedSumLaw_entropy line 142
  13. lemma OAI.DirectionalZeroOne.entropyOf_nonneg line 173
  14. lemma OAI.DirectionalZeroOne.sum_entropy_integrable_bounded line 178
  15. lemma OAI.DirectionalZeroOne.markedSumLaw_entropy_bounds line 188