OAI/Probability/SwitchChain/PairEqualityProjection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.PairEquality.observable line 12
  2. def OAI.Problem315.PairEquality.centered line 15
  3. def OAI.Problem315.PairEquality.active line 18
  4. def OAI.Problem315.PairEquality.equalitySpace line 21
  5. def OAI.Problem315.PairEquality.projection line 42
  6. theorem OAI.Problem315.PairEquality.projection_eq_self_iff line 45
  7. def OAI.Problem315.PairEquality.crossTotal line 49
  8. theorem OAI.Problem315.PairEquality.active_sameFiber line 53
  9. theorem OAI.Problem315.PairEquality.crossTotal_sameFiber line 60
  10. theorem OAI.Problem315.PairEquality.observable_zero_of_inactive line 66
  11. theorem OAI.Problem315.PairEquality.centered_zero_of_inactive line 77
  12. def OAI.Problem315.PairEquality.multiply line 96
  13. theorem OAI.Problem315.PairEquality.expectation_multiply line 99
  14. theorem OAI.Problem315.PairEquality.fluctuation_multiply line 115
  15. theorem OAI.Problem315.PairEquality.multiply_centered_mem line 124
  16. theorem OAI.Problem315.PairEquality.fluctuation_weighted_observable_mem line 144
  17. theorem OAI.Problem315.PairEquality.fluctuation_weighted_centered_flag_mem line 153
  18. theorem OAI.Problem315.PairEquality.projection_fixes_weighted_flag_fluctuation line 164
  19. theorem OAI.Problem315.PairEquality.line_projection_norm_le line 176