OAI/Probability/SwitchChain/PairFibers.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.PairFibers.SameFiber line 11
  2. theorem OAI.Problem315.PairFibers.SameFiber.refl line 18
  3. theorem OAI.Problem315.PairFibers.SameFiber.symm line 22
  4. theorem OAI.Problem315.PairFibers.SameFiber.trans line 28
  5. def OAI.Problem315.PairFibers.stateSetoid line 34
  6. def OAI.Problem315.PairFibers.constantSubspace line 44
  7. theorem OAI.Problem315.PairFibers.mem_constantSubspace line 57
  8. def OAI.Problem315.PairFibers.expectation line 60
  9. def OAI.Problem315.PairFibers.deviation line 63
  10. theorem OAI.Problem315.PairFibers.expectation_mem line 66
  11. theorem OAI.Problem315.PairFibers.expectation_constant line 70
  12. theorem OAI.Problem315.PairFibers.expectation_eq_self_iff line 74
  13. theorem OAI.Problem315.PairFibers.deviation_eq_sub line 78
  14. theorem OAI.Problem315.PairFibers.deviation_eq_zero_iff line 85
  15. theorem OAI.Problem315.PairFibers.expectation_idempotent line 90
  16. theorem OAI.Problem315.PairFibers.deviation_idempotent line 94
  17. theorem OAI.Problem315.PairFibers.expectation_symmetric line 99
  18. theorem OAI.Problem315.PairFibers.deviation_symmetric line 103
  19. theorem OAI.Problem315.PairFibers.deviation_energy line 107
  20. theorem OAI.Problem315.PairFibers.deviation_energy_nonneg line 113
  21. def OAI.Problem315.PairFibers.cell line 118
  22. theorem OAI.Problem315.PairFibers.mem_cell line 121
  23. theorem OAI.Problem315.PairFibers.cell_nonempty line 124
  24. theorem OAI.Problem315.PairFibers.cell_eq line 127
  25. def OAI.Problem315.PairFibers.cellIndicator line 132
  26. theorem OAI.Problem315.PairFibers.cellIndicator_mem line 136
  27. theorem OAI.Problem315.PairFibers.inner_cellIndicator line 144
  28. theorem OAI.Problem315.PairFibers.expectation_apply line 148
  29. abbrev OAI.Problem315.PairFibers.StateSpace line 170
  30. def OAI.Problem315.PairFibers.pairExpectation line 172
  31. def OAI.Problem315.PairFibers.pairDeviation line 175
  32. theorem OAI.Problem315.PairFibers.pairDeviation_eq_zero_iff line 178