OAI/Probability/SwitchChain/SwitchFlip.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem315.SwitchFlip.not_valid_reverse line 14
  2. lemma OAI.Problem315.SwitchFlip.valid_reverse_result line 21
  3. lemma OAI.Problem315.SwitchFlip.state_reverse line 28
  4. def OAI.Problem315.SwitchFlip.flip line 34
  5. theorem OAI.Problem315.SwitchFlip.flip_of_valid line 39
  6. theorem OAI.Problem315.SwitchFlip.flip_of_reverse_valid line 43
  7. theorem OAI.Problem315.SwitchFlip.flip_reverse line 49
  8. theorem OAI.Problem315.SwitchFlip.flip_involutive line 55
  9. def OAI.Problem315.SwitchFlip.equiv line 69
  10. theorem OAI.Problem315.SwitchFlip.equiv_apply line 72
  11. def OAI.Problem315.SwitchFlip.isometry line 75
  12. theorem OAI.Problem315.SwitchFlip.isometry_apply line 79
  13. def OAI.Problem315.SwitchFlip.operator line 83
  14. theorem OAI.Problem315.SwitchFlip.operator_apply line 87
  15. theorem OAI.Problem315.SwitchFlip.operator_involutive line 91
  16. theorem OAI.Problem315.SwitchFlip.operator_symmetric line 96
  17. def OAI.Problem315.SwitchFlip.projection line 104
  18. theorem OAI.Problem315.SwitchFlip.projection_apply line 108
  19. theorem OAI.Problem315.SwitchFlip.projection_idempotent line 113
  20. theorem OAI.Problem315.SwitchFlip.projection_symmetric line 119
  21. theorem OAI.Problem315.SwitchFlip.inner_projection line 129
  22. theorem OAI.Problem315.SwitchFlip.projection_reverse line 137
  23. theorem OAI.Problem315.SwitchFlip.norm_projection_sq line 142
  24. theorem OAI.Problem315.SwitchFlip.proposal_sameFiber line 152
  25. theorem OAI.Problem315.SwitchFlip.flip_sameFiber line 174
  26. theorem OAI.Problem315.SwitchFlip.projection_eq_zero_of_fiber line 190
  27. theorem OAI.Problem315.SwitchFlip.projection_mem_orthogonal line 198
  28. theorem OAI.Problem315.SwitchFlip.projection_expectation line 208
  29. theorem OAI.Problem315.SwitchFlip.fluctuation_projection line 213
  30. theorem OAI.Problem315.SwitchFlip.projection_fluctuation line 219
  31. theorem OAI.Problem315.SwitchFlip.isSymmetricProjection line 225
  32. theorem OAI.Problem315.SwitchFlip.norm_projection_le_of_mem line 233
  33. theorem OAI.Problem315.SwitchFlip.projection_mem_jointOrthogonal line 249
  34. theorem OAI.Problem315.SwitchFlip.norm_projection_le_jointOrthogonal line 257