OAI/Analysis/BoundedHochschild/CochainLimits.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Weak-star cochain limits, averaging operators and preadjoints.

  1. def OAI.BoundedHochschild.PredualTendsto line 29
  2. lemma OAI.BoundedHochschild.predual_tendsto_unique line 32
  3. lemma OAI.BoundedHochschild.predual_tendsto_const line 38
  4. lemma OAI.BoundedHochschild.predual_tendsto_add line 41
  5. lemma OAI.BoundedHochschild.predual_tendsto_smul line 47
  6. lemma OAI.BoundedHochschild.exists_predual_ultralimit line 54
  7. theorem OAI.BoundedHochschild.bounded_cochain_ultralimit line 77
  8. def OAI.BoundedHochschild.translateLastCLM line 108
  9. theorem OAI.BoundedHochschild.translateLast_one line 116
  10. theorem OAI.BoundedHochschild.translateLast_mul line 124
  11. def OAI.BoundedHochschild.averageLastCLM line 130
  12. theorem OAI.BoundedHochschild.averageLastCLM_apply line 144
  13. def OAI.BoundedHochschild.residualCLM line 150
  14. theorem OAI.BoundedHochschild.residualCLM_apply line 159
  15. lemma OAI.BoundedHochschild.residual_eq_differential line 166
  16. lemma OAI.BoundedHochschild.insertLast_translateLast line 173
  17. lemma OAI.BoundedHochschild.residual_translate_cocycle line 178
  18. lemma OAI.BoundedHochschild.residual_average_invariant line 189
  19. lemma OAI.BoundedHochschild.residual_iterate line 208
  20. lemma OAI.BoundedHochschild.predual_tendsto_of_norm line 229
  21. lemma OAI.BoundedHochschild.predual_tendsto_neg line 235
  22. lemma OAI.BoundedHochschild.predual_tendsto_sub line 240
  23. lemma OAI.BoundedHochschild.predual_tendsto_sum line 245
  24. lemma OAI.BoundedHochschild.predual_norm_le line 252
  25. lemma OAI.BoundedHochschild.predual_tendsto_tsum line 263
  26. def OAI.BoundedHochschild.HasPreadjoint line 285
  27. lemma OAI.BoundedHochschild.HasPreadjoint.tendsto line 288