OAI/Probability/ThreeStateClauses/Correlation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Correlation.

  1. lemma OAI.ThreeState.TreeClauses.Positive.log_cubic_lower line 16
  2. def OAI.ThreeState.TreeClauses.Positive.orbit line 66
  3. def OAI.ThreeState.TreeClauses.Positive.avgSix line 70
  4. def OAI.ThreeState.TreeClauses.Positive.dotAvg line 73
  5. lemma OAI.ThreeState.TreeClauses.Positive.avgSix_dot line 75
  6. lemma OAI.ThreeState.TreeClauses.Positive.avgSix_dot_sq line 80
  7. lemma OAI.ThreeState.TreeClauses.Positive.avgSix_dot_cube line 85
  8. lemma OAI.ThreeState.TreeClauses.Positive.avgSix_mono line 90
  9. theorem OAI.ThreeState.TreeClauses.Positive.correlation_orbit_lower line 94
  10. def OAI.ThreeState.TreeClauses.Experiment.pairZ line 116
  11. def OAI.ThreeState.TreeClauses.Experiment.pairPosterior line 118
  12. lemma OAI.ThreeState.TreeClauses.Experiment.pairZ_lower line 133
  13. lemma OAI.ThreeState.TreeClauses.Experiment.pairZ_positive line 141
  14. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_pairZ line 144
  15. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_pairPosterior line 148
  16. lemma OAI.ThreeState.TreeClauses.Experiment.pairZ_dot line 155
  17. lemma OAI.ThreeState.TreeClauses.Experiment.integral_pairZ line 162
  18. lemma OAI.ThreeState.TreeClauses.Experiment.integral_pair_coordinate line 171
  19. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_pairEntropy line 180
  20. def OAI.ThreeState.TreeClauses.Experiment.pairCorrelation line 184
  21. lemma OAI.ThreeState.TreeClauses.Experiment.pairCorrelation_nonneg line 187
  22. def OAI.ThreeState.TreeClauses.Experiment.orbitIndex line 204
  23. def OAI.ThreeState.TreeClauses.Experiment.orbitPerm line 207
  24. lemma OAI.ThreeState.TreeClauses.Experiment.orbitPerm_apply line 210
  25. lemma OAI.ThreeState.TreeClauses.Experiment.pairZ_orbit line 214
  26. lemma OAI.ThreeState.TreeClauses.Experiment.integral_avgSix_measure line 223
  27. lemma OAI.ThreeState.TreeClauses.Experiment.xMoment_edge line 238
  28. lemma OAI.ThreeState.TreeClauses.Experiment.yMoment_edge line 243
  29. lemma OAI.ThreeState.TreeClauses.Experiment.pairCorrelation_increment_at line 248
  30. theorem OAI.ThreeState.TreeClauses.Experiment.pairCorrelation_increment line 294