OAI/Probability/ThreeState/Symmetry.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Spin symmetry and measure identities for posterior fixed points.

  1. lemma OAI.ThreeState.pmf_map_equiv_apply line 12
  2. lemma OAI.ThreeState.uniformSpin_map line 15
  3. lemma OAI.ThreeState.channelPMF_map line 22
  4. def OAI.ThreeState.permMessage line 30
  5. lemma OAI.ThreeState.continuous_permMessage line 37
  6. def OAI.ThreeState.renameOrdered line 43
  7. lemma OAI.ThreeState.orderedLaw_rename line 47
  8. lemma OAI.ThreeState.marginal_equivariant line 66
  9. lemma OAI.ThreeState.posterior_equivariant line 74
  10. lemma OAI.ThreeState.likelihood_equivariant line 86
  11. lemma OAI.ThreeState.likelihoodPMF_equivariant line 96
  12. def OAI.ThreeState.SpinSymmetric line 106
  13. lemma OAI.ThreeState.ordered_likelihood_symmetric line 109
  14. lemma OAI.ThreeState.symmetric_limit line 119
  15. lemma OAI.ThreeState.ordered_exists_symmetric_fixedpoint line 128
  16. lemma OAI.ThreeState.measurable_combineMessage line 141
  17. def OAI.ThreeState.degreeInput line 158
  18. lemma OAI.ThreeState.degreeInput_probability line 162
  19. def OAI.ThreeState.degreeOutput line 171
  20. lemma OAI.ThreeState.degreeOutput_probability line 174
  21. def OAI.ThreeState.densityEvolution line 182
  22. lemma OAI.ThreeState.densityEvolution_probability line 186
  23. lemma OAI.ThreeState.integral_degreeOutput line 196
  24. lemma OAI.ThreeState.integral_densityEvolution_continuous line 208
  25. lemma OAI.ThreeState.fixedpoint_measure line 222
  26. lemma OAI.ThreeState.ae_degreeOutput_of_forall line 239
  27. lemma OAI.ThreeState.ae_fixedpoint_of_output line 246
  28. lemma OAI.ThreeState.integrable_degreeOutput_bound line 256
  29. lemma OAI.ThreeState.integrable_fixedpoint_of_growth line 273
  30. lemma OAI.ThreeState.integral_fixedpoint line 290