OAI/Probability/SwitchChain/OrthogonalPairResampling.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.PairResampling.SameFiber line 14
  2. theorem OAI.Problem315.PairResampling.SameFiber.refl line 19
  3. theorem OAI.Problem315.PairResampling.SameFiber.symm line 24
  4. theorem OAI.Problem315.PairResampling.SameFiber.trans line 30
  5. theorem OAI.Problem315.PairResampling.graphDegree_partition line 37
  6. theorem OAI.Problem315.PairResampling.sameFiber_of_fixed_edges line 53
  7. theorem OAI.Problem315.PairResampling.sameFiber_state_iff line 71
  8. abbrev OAI.Problem315.PairResampling.StateSpace line 81
  9. def OAI.Problem315.PairResampling.fiberSpace line 83
  10. def OAI.Problem315.PairResampling.expectation line 96
  11. def OAI.Problem315.PairResampling.fluctuation line 99
  12. theorem OAI.Problem315.PairResampling.expectation_mem line 104
  13. theorem OAI.Problem315.PairResampling.expectation_eq_self_iff line 108
  14. theorem OAI.Problem315.PairResampling.expectation_isSymmetric line 112
  15. theorem OAI.Problem315.PairResampling.fluctuation_isSymmetric line 116
  16. theorem OAI.Problem315.PairResampling.expectation_idempotent line 120
  17. theorem OAI.Problem315.PairResampling.fluctuation_idempotent line 124
  18. theorem OAI.Problem315.PairResampling.fluctuation_eq_sub line 129
  19. theorem OAI.Problem315.PairResampling.fluctuation_eq_zero_iff line 133
  20. theorem OAI.Problem315.PairResampling.inner_fluctuation line 137
  21. theorem OAI.Problem315.PairResampling.fluctuation_nonneg line 145
  22. def OAI.Problem315.PairResampling.pairs line 150
  23. def OAI.Problem315.PairResampling.generator line 152
  24. theorem OAI.Problem315.PairResampling.generator_apply line 155
  25. theorem OAI.Problem315.PairResampling.generator_isSymmetric line 159
  26. theorem OAI.Problem315.PairResampling.inner_generator line 167
  27. theorem OAI.Problem315.PairResampling.generator_nonneg line 171
  28. theorem OAI.Problem315.PairResampling.generator_eq_zero_iff line 175
  29. theorem OAI.Problem315.PairResampling.state_inner line 191
  30. theorem OAI.Problem315.PairResampling.constant_mem line 195
  31. theorem OAI.Problem315.PairResampling.generator_constant line 200
  32. def OAI.Problem315.PairResampling.fiberStates line 206
  33. theorem OAI.Problem315.PairResampling.mem_fiberStates line 209
  34. theorem OAI.Problem315.PairResampling.self_mem_fiberStates line 213
  35. theorem OAI.Problem315.PairResampling.fiberStates_nonempty line 216
  36. def OAI.Problem315.PairResampling.fiberIndicator line 219
  37. theorem OAI.Problem315.PairResampling.fiberIndicator_mem line 222
  38. theorem OAI.Problem315.PairResampling.expectation_eq_average line 231