OAI/Analysis/BoundedHochschild/BlockSpans.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Signed block sums, good patterns and spans of word evaluations.

  1. def OAI.HochschildBlockAssembly.allSum line 18
  2. lemma OAI.HochschildBlockAssembly.sum_badSum line 21
  3. lemma OAI.HochschildBlockAssembly.map_allSum_eq_badSum line 45
  4. lemma OAI.HochschildBlockAssembly.tendsto_map_allSum line 62
  5. def OAI.HochschildWordEval.letter line 87
  6. def OAI.HochschildWordEval.eval line 89
  7. lemma OAI.HochschildWordEval.eval_nil line 91
  8. lemma OAI.HochschildWordEval.eval_cons line 92
  9. lemma OAI.HochschildWordEval.eval_append line 94
  10. lemma OAI.HochschildWordEval.letter_smul line 97
  11. lemma OAI.HochschildWordEval.eval_smul line 100
  12. lemma OAI.HochschildWordEval.letter_sum line 108
  13. lemma OAI.HochschildWordEval.wordOf_cons line 112
  14. lemma OAI.HochschildWordEval.map_singleton line 119
  15. lemma OAI.HochschildWordEval.allSum_cons line 125
  16. lemma OAI.HochschildWordEval.eval_sum_eq line 145
  17. lemma OAI.HochschildWordEval.eval_freeSum line 152
  18. def OAI.HochschildGoodPatterns.Good line 166
  19. def OAI.HochschildGoodPatterns.alt line 170
  20. lemma OAI.HochschildGoodPatterns.length_alt line 174
  21. lemma OAI.HochschildGoodPatterns.signed_fst line 179
  22. lemma OAI.HochschildGoodPatterns.signed_snd line 184
  23. lemma OAI.HochschildGoodPatterns.good_alt line 190
  24. lemma OAI.HochschildGoodPatterns.good_append line 201
  25. lemma OAI.HochschildGoodPatterns.good_length_pos line 207
  26. def OAI.HochschildGoodPatterns.invPattern line 213
  27. lemma OAI.HochschildGoodPatterns.invPattern_invPattern line 215
  28. lemma OAI.HochschildGoodPatterns.invRev_snd line 218
  29. lemma OAI.HochschildGoodPatterns.ends_invRev line 222
  30. lemma OAI.HochschildGoodPatterns.good_inv line 233
  31. lemma OAI.HochschildGoodPatterns.letter_not line 241
  32. lemma OAI.HochschildGoodPatterns.eval_inv line 244
  33. lemma OAI.HochschildGoodPatterns.eval_alt line 253
  34. def OAI.HochschildBlockSpan.span line 272
  35. lemma OAI.HochschildBlockSpan.generator_mem line 275
  36. lemma OAI.HochschildBlockSpan.mul_mem line 278
  37. lemma OAI.HochschildBlockSpan.pow_mem line 303
  38. lemma OAI.HochschildBlockSpan.star_mem line 310
  39. lemma OAI.HochschildBlockSpan.polynomial_block_mem line 327
  40. lemma OAI.HochschildBlockSpan.polarApprox_mem line 337
  41. lemma OAI.HochschildBlockSpan.tendsto_eval_of_good line 344
  42. lemma OAI.HochschildBlockSpan.tendsto_of_mem line 365