OAI/Analysis/BoundedHochschild/ProductTaylor.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Noncommutative product expansions and linear and quadratic error terms.

  1. def OAI.HochschildPatching.ProductTaylor.oldProduct line 20
  2. def OAI.HochschildPatching.ProductTaylor.totalProduct line 21
  3. lemma OAI.HochschildPatching.ProductTaylor.old_nil line 22
  4. lemma OAI.HochschildPatching.ProductTaylor.total_nil line 23
  5. lemma OAI.HochschildPatching.ProductTaylor.old_cons line 24
  6. lemma OAI.HochschildPatching.ProductTaylor.total_cons line 25
  7. lemma OAI.HochschildPatching.ProductTaylor.old_append line 26
  8. lemma OAI.HochschildPatching.ProductTaylor.total_append line 28
  9. def OAI.HochschildPatching.ProductTaylor.differenceTerms line 31
  10. def OAI.HochschildPatching.ProductTaylor.linearTerms line 34
  11. def OAI.HochschildPatching.ProductTaylor.quadraticTerms line 37
  12. lemma OAI.HochschildPatching.ProductTaylor.sum_map_mul_left line 41
  13. lemma OAI.HochschildPatching.ProductTaylor.total_eq_old_add_difference line 46
  14. lemma OAI.HochschildPatching.ProductTaylor.total_eq_old_add_linear_add_quadratic line 53
  15. lemma OAI.HochschildPatching.ProductTaylor.mem_differenceTerms line 67
  16. lemma OAI.HochschildPatching.ProductTaylor.mem_linearTerms line 77
  17. lemma OAI.HochschildPatching.ProductTaylor.mem_quadraticTerms line 87
  18. lemma OAI.HochschildPatching.ProductTaylor.differenceTerms_length line 100
  19. lemma OAI.HochschildPatching.ProductTaylor.linearTerms_length line 104
  20. lemma OAI.HochschildPatching.ProductTaylor.quadraticTerms_length_le line 108