OAI/Probability/ThreeState/PairCorrelation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Two-message correlation and quantitative entropy increments.

  1. lemma OAI.ThreeState.log_correlation_cubic line 11
  2. def OAI.ThreeState.correlationZ line 58
  3. lemma OAI.ThreeState.continuous_correlationZ line 59
  4. def OAI.ThreeState.symPerm line 65
  5. def OAI.ThreeState.symAvg line 68
  6. lemma OAI.ThreeState.integral_symAvg line 71
  7. lemma OAI.ThreeState.symAvg_correlationZ line 81
  8. lemma OAI.ThreeState.symAvg_correlationZ_sq line 92
  9. lemma OAI.ThreeState.symAvg_correlationZ_cube line 105
  10. lemma OAI.ThreeState.integral_correlationZ line 118
  11. lemma OAI.ThreeState.integral_correlationZ_sq line 123
  12. lemma OAI.ThreeState.integral_correlationZ_cube line 128
  13. lemma OAI.ThreeState.correlationZ_comm line 139
  14. def OAI.ThreeState.pairNormalizer line 142
  15. lemma OAI.ThreeState.pairNormalizer_eq line 145
  16. lemma OAI.ThreeState.continuous_pairNormalizer line 154
  17. lemma OAI.ThreeState.pairNormalizer_pos line 159
  18. def OAI.ThreeState.pairMessage line 167
  19. lemma OAI.ThreeState.continuous_pairMessage line 184
  20. lemma OAI.ThreeState.integral_pairNormalizer line 193
  21. def OAI.ThreeState.pairIncrement line 203
  22. lemma OAI.ThreeState.continuous_pairIntegrand line 206
  23. lemma OAI.ThreeState.pairIncrement_nonneg line 211
  24. lemma OAI.ThreeState.pairIncrement_lower line 228