OAI/Probability/SwitchChain/DisjointIndicators.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.DisjointIndicators.normalizedFlag line 10
  2. def OAI.Problem315.DisjointIndicators.correlation line 14
  3. theorem OAI.Problem315.DisjointIndicators.correlation_sq_lt_one line 17
  4. theorem OAI.Problem315.DisjointIndicators.correlation_nondegenerate line 33
  5. theorem OAI.Problem315.DisjointIndicators.centered_inner_self line 37
  6. theorem OAI.Problem315.DisjointIndicators.centered_cross_inner line 47
  7. theorem OAI.Problem315.DisjointIndicators.normalizedFlag_inner_self line 58
  8. theorem OAI.Problem315.DisjointIndicators.normalizedFlag_cross_inner line 70
  9. theorem OAI.Problem315.DisjointIndicators.normalized_flags_gram line 81
  10. theorem OAI.Problem315.DisjointIndicators.normalizedFlag_centered line 97
  11. theorem OAI.Problem315.DisjointIndicators.normalizedFlag_fixed line 104