OAI/Analysis/BoundedHochschild/CollisionBounds.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Repeated indices, block words, range counts and normalized collision errors.

  1. def OAI.HochschildCollision.count line 19
  2. lemma OAI.HochschildCollision.count_cons line 21
  3. lemma OAI.HochschildCollision.count_parity line 25
  4. lemma OAI.HochschildCollision.combined_count_ne_one line 47
  5. lemma OAI.HochschildCollision.count_reduce_le line 57
  6. lemma OAI.HochschildCollision.exists_repeat_of_not_nodup line 61
  7. lemma OAI.HochschildCollision.sum_count line 71
  8. theorem OAI.HochschildCollision.range_card_le_of_repeated_reduction line 81
  9. lemma OAI.HochschildBlockWords.length_signed line 130
  10. def OAI.HochschildBlockWords.Ends line 135
  11. lemma OAI.HochschildBlockWords.signed_odd_ends line 138
  12. lemma OAI.HochschildBlockWords.reduce_signed_odd_ends line 151
  13. lemma OAI.HochschildBlockWords.ends_append line 161
  14. lemma OAI.HochschildBlockWords.reduced_append_of_ends line 169
  15. theorem OAI.HochschildBlockWords.reduce_append_odd_blocks line 180
  16. lemma OAI.HochschildIndexedHaagerup.norm_sum_sq line 204
  17. lemma OAI.HochschildIndexedHaagerup.norm_sum_le line 234
  18. abbrev OAI.HochschildRangeCount.SmallRange line 266
  19. def OAI.HochschildRangeCount.composeSmall line 269
  20. lemma OAI.HochschildRangeCount.composeSmall_surjective line 278
  21. theorem OAI.HochschildRangeCount.card_smallRange_le line 293
  22. def OAI.HochschildCollision.tupleWord line 306
  23. lemma OAI.HochschildCollision.tupleWord_length line 310
  24. lemma OAI.HochschildCollision.tupleWord_map line 314
  25. abbrev OAI.HochschildCollision.BadPairs line 317
  26. lemma OAI.HochschildCollision.ofFn_toFinset line 323
  27. def OAI.HochschildCollision.pairToSmall line 328
  28. lemma OAI.HochschildCollision.pairToSmall_injective line 336
  29. theorem OAI.HochschildCollision.card_badPairs_le line 350
  30. abbrev OAI.HochschildBlockError.BadTerms line 363
  31. def OAI.HochschildBlockError.wordOf line 367
  32. def OAI.HochschildBlockError.pairToBad line 370
  33. lemma OAI.HochschildBlockError.pairToBad_injective line 376
  34. def OAI.HochschildBlockError.badSum line 394
  35. lemma OAI.HochschildBlockError.badSum_norm_le line 398
  36. def OAI.HochschildBlockError.normalizer line 411
  37. lemma OAI.HochschildBlockError.normalizer_nonneg line 413
  38. lemma OAI.HochschildBlockError.normalizer_sq line 415
  39. lemma OAI.HochschildBlockError.normalizer_cancel line 420
  40. theorem OAI.HochschildBlockError.normalized_badSum_sq_le line 432
  41. theorem OAI.HochschildBlockError.tendsto_normalized_badSum line 467
  42. theorem OAI.HochschildBlockError.tendsto_total_badSum line 482