OAI/Probability/SwitchChain/PairEqualityErrorLine.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.PairEqualityErrorLine.crossTotal line 15
  2. def OAI.Problem315.PairEqualityErrorLine.rowExtreme line 18
  3. def OAI.Problem315.PairEqualityErrorLine.equalityIndicator line 21
  4. theorem OAI.Problem315.PairEqualityErrorLine.rowExtreme_eq_gated_equality line 24
  5. theorem OAI.Problem315.PairEqualityErrorLine.singleton_gate_eq_of_sameFiber line 34
  6. theorem OAI.Problem315.PairEqualityErrorLine.expectation_mul_fiberConstant line 40
  7. theorem OAI.Problem315.PairEqualityErrorLine.fluctuation_mul_fiberConstant line 57
  8. theorem OAI.Problem315.PairEqualityErrorLine.fluctuation_rowExtreme line 69
  9. theorem OAI.Problem315.PairEqualityErrorLine.rowExtreme_of_total_two line 95
  10. theorem OAI.Problem315.PairEqualityErrorLine.fluctuation_affine line 101
  11. theorem OAI.Problem315.PairEqualityErrorLine.fluctuation_cell_affine_rowExtreme line 112
  12. theorem OAI.Problem315.PairEqualityErrorLine.leftSet_mem_iff_adj_of_singleton line 136
  13. theorem OAI.Problem315.PairEqualityErrorLine.equalityIndicator_eq_leftSet line 143