OAI/Analysis/BoundedHochschild/MixedWords.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Mixed-word Taylor expansions, moment corners and patch coefficients.

  1. def OAI.HochschildPatching.wordProduct line 37
  2. lemma OAI.HochschildPatching.wordProduct_nil line 40
  3. lemma OAI.HochschildPatching.wordProduct_cons line 41
  4. lemma OAI.HochschildPatching.wordProduct_append line 43
  5. lemma OAI.HochschildPatching.norm_wordProduct_le_one line 48
  6. def OAI.HochschildPatching.wordCoeff line 59
  7. lemma OAI.HochschildPatching.wordCoeff_none line 60
  8. lemma OAI.HochschildPatching.wordCoeff_some line 61
  9. lemma OAI.HochschildPatching.norm_wordCoeff line 62
  10. abbrev OAI.HochschildPatching.WordAtom line 66
  11. abbrev OAI.HochschildPatching.BoundedWord line 67
  12. instance OAI.HochschildPatching.(instance at line 68) line 68
  13. instance OAI.HochschildPatching.(instance at line 71) line 71
  14. def OAI.HochschildPatching.admissibleTail line 73
  15. def OAI.HochschildPatching.evaluatedTail line 76
  16. def OAI.HochschildPatching.mixedEval line 78
  17. lemma OAI.HochschildPatching.norm_mixedEval line 80
  18. lemma OAI.HochschildPatching.wordProduct_tendsto line 90
  19. lemma OAI.HochschildPatching.mixedEval_tendsto line 102
  20. lemma OAI.HochschildPatching.trace_tendsto_of_gns line 111
  21. def OAI.HochschildPatching.MomentBound line 120
  22. lemma OAI.HochschildPatching.momentBound_limit line 125
  23. lemma OAI.HochschildPatching.ProductTaylor.mem_linearTerms_map line 146
  24. lemma OAI.HochschildPatching.ProductTaylor.mem_quadraticTerms_map line 153
  25. def OAI.HochschildPatching.atomPower line 167
  26. def OAI.HochschildPatching.splitFactor line 168
  27. lemma OAI.HochschildPatching.oldProduct_split line 170
  28. lemma OAI.HochschildPatching.totalProduct_split line 175
  29. lemma OAI.HochschildPatching.mixedEval_split line 183
  30. lemma OAI.HochschildPatching.admissible_middle line 191
  31. lemma OAI.HochschildPatching.trace_list_sum_bound line 204
  32. lemma OAI.HochschildPatching.mixedEval_patch_bound line 213
  33. lemma OAI.HochschildPatching.centered_word_bound line 244
  34. lemma OAI.HochschildPatching.support_wrapped_eval line 255
  35. lemma OAI.HochschildPatching.support_wrapped_admissible line 262
  36. lemma OAI.HochschildPatching.normalized_corner_trace_eq line 275
  37. lemma OAI.HochschildPatching.residual_centered_word_bound line 284
  38. lemma OAI.HochschildPatching.mixedEval_zero line 299
  39. lemma OAI.HochschildPatching.momentBound_zero line 306
  40. abbrev OAI.HochschildPatching.ShortTail line 322
  41. abbrev OAI.HochschildPatching.LinearLabel line 323
  42. instance OAI.HochschildPatching.(instance at line 324) line 324
  43. instance OAI.HochschildPatching.(instance at line 327) line 327
  44. def OAI.HochschildPatching.linearCoeff line 328
  45. def OAI.HochschildPatching.linearPower line 331
  46. lemma OAI.HochschildPatching.linear_trace_bound line 336
  47. def OAI.HochschildPatching.residualScalar line 358
  48. lemma OAI.HochschildPatching.residualScalar_bound line 362
  49. lemma OAI.HochschildPatching.quadratic_trace_bound line 372