OAI/Combinatorics/BalancedRyser/Probability/SparsePatterns.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.SparsePatterns.differingPositions line 18
  2. def OAI.Balanced.SparsePatterns.sparseFunctions line 21
  3. theorem OAI.Balanced.SparsePatterns.mem_differingPositions line 25
  4. theorem OAI.Balanced.SparsePatterns.mem_sparseFunctions line 29
  5. theorem OAI.Balanced.SparsePatterns.differingPositions_eq_empty line 34
  6. theorem OAI.Balanced.SparsePatterns.sparseFunctions_zero line 38
  7. theorem OAI.Balanced.SparsePatterns.differingPositions_update_base line 46
  8. theorem OAI.Balanced.SparsePatterns.sparseFunctions_succ_subset line 55
  9. theorem OAI.Balanced.SparsePatterns.card_sparseFunctions_succ_le line 80
  10. theorem OAI.Balanced.SparsePatterns.card_sparseFunctions_le line 104
  11. theorem OAI.Balanced.SparsePatterns.card_sparse_endomaps_le line 117
  12. theorem OAI.Balanced.SparsePatterns.card_sparse_tuple_maps_le line 121
  13. def OAI.Balanced.SparsePatterns.firstOccurrence line 136
  14. theorem OAI.Balanced.SparsePatterns.value_firstOccurrence line 139
  15. theorem OAI.Balanced.SparsePatterns.firstOccurrence_le line 144
  16. theorem OAI.Balanced.SparsePatterns.firstOccurrence_eq_of_value_eq line 147
  17. theorem OAI.Balanced.SparsePatterns.firstOccurrence_eq_iff line 151
  18. theorem OAI.Balanced.SparsePatterns.firstOccurrence_idem line 159
  19. theorem OAI.Balanced.SparsePatterns.mem_firstOccurrence_range line 163
  20. theorem OAI.Balanced.SparsePatterns.card_firstOccurrence_range line 172
  21. theorem OAI.Balanced.SparsePatterns.card_differing_firstOccurrence line 191
  22. theorem OAI.Balanced.SparsePatterns.firstOccurrence_mem_sparse line 202
  23. theorem OAI.Balanced.SparsePatterns.firstOccurrence_eq_iff_same_pattern line 208
  24. theorem OAI.Balanced.SparsePatterns.card_canonical_patterns_le line 221
  25. theorem OAI.Balanced.SparsePatterns.card_canonical_tuple_patterns_le line 234
  26. theorem OAI.Balanced.SparsePatterns.exists_canonical_tuple_representatives line 246
  27. theorem OAI.Balanced.SparsePatterns.exists_relabeling_of_same_pattern line 278
  28. theorem OAI.Balanced.SparsePatterns.exists_assignment_equiv_of_same_pattern line 297
  29. theorem OAI.Balanced.SparsePatterns.sum_assignments_eq_of_same_pattern line 307