OAI/Probability/ThorpShuffle/Walsh.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Conditional.character line 16
  2. theorem OAI.Thorp.Conditional.character_symm line 19
  3. theorem OAI.Thorp.Conditional.character_false line 25
  4. theorem OAI.Thorp.Conditional.character_sq line 29
  5. theorem OAI.Thorp.Conditional.sum_character_pair line 37
  6. theorem OAI.Thorp.Conditional.sum_character_pair_dual line 67
  7. def OAI.Thorp.Conditional.coefficient line 78
  8. theorem OAI.Thorp.Conditional.parseval line 81
  9. theorem OAI.Thorp.Conditional.coefficient_false line 112
  10. theorem OAI.Thorp.Conditional.character_reindex line 116
  11. theorem OAI.Thorp.Conditional.character_cons line 121