OAI/Analysis/FreeWords/ThroughLabel.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKThroughLabel.beta line 13
  2. def OAI.KKThroughLabel.throughSum line 17
  3. def OAI.KKThroughLabel.wordsThrough line 25
  4. def OAI.KKThroughLabel.distinctThrough line 28
  5. def OAI.KKThroughLabel.repeatedThrough line 31
  6. theorem OAI.KKThroughLabel.mem_wordsThrough line 34
  7. theorem OAI.KKThroughLabel.mem_distinctThrough line 37
  8. theorem OAI.KKThroughLabel.mem_repeatedThrough line 41
  9. theorem OAI.KKThroughLabel.card_sym_le_pow line 45
  10. theorem OAI.KKThroughLabel.card_distinctThrough_le_choose line 61
  11. theorem OAI.KKThroughLabel.exists_double_cons line 90
  12. theorem OAI.KKThroughLabel.repeatedThrough_subset line 102
  13. theorem OAI.KKThroughLabel.card_repeatedThrough_le line 120
  14. theorem OAI.KKThroughLabel.repeatedThrough_one line 149
  15. theorem OAI.KKThroughLabel.repeatedThrough_two line 158
  16. theorem OAI.KKThroughLabel.card_repeatedThrough_le_all line 174
  17. theorem OAI.KKThroughLabel.neg_half_rpow_sq line 182
  18. theorem OAI.KKThroughLabel.beta_sq line 192
  19. theorem OAI.KKThroughLabel.throughSum_eq line 203
  20. theorem OAI.KKThroughLabel.distinct_contribution_le line 233
  21. theorem OAI.KKThroughLabel.repeated_contribution_le line 249
  22. theorem OAI.KKThroughLabel.throughSum_le line 261
  23. theorem OAI.KKThroughLabel.through_label line 279