OAI/Analysis/BoundedHochschild/NormalModulus.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Normal cochains, bounded-ball continuity and primitive construction.

  1. lemma OAI.BoundedHochschild.preGNS_zero_of_predual_limit line 30
  2. theorem OAI.BoundedHochschild.predual_tendsto_of_preGNS line 43
  3. theorem OAI.BoundedHochschild.exists_bounded_preGNS_limit line 62
  4. lemma OAI.BoundedHochschild.preGNS_sq_le_trace line 83
  5. lemma OAI.BoundedHochschild.monotone_contractions_preGNS_cauchy line 93
  6. def OAI.BoundedHochschild.GNSTendsto line 124
  7. lemma OAI.BoundedHochschild.GNSTendsto.const line 127
  8. lemma OAI.BoundedHochschild.GNSTendsto.add line 131
  9. lemma OAI.BoundedHochschild.GNSTendsto.neg line 138
  10. lemma OAI.BoundedHochschild.GNSTendsto.sub line 142
  11. lemma OAI.BoundedHochschild.GNSTendsto.star line 147
  12. lemma OAI.BoundedHochschild.GNSTendsto.mul line 152
  13. lemma OAI.BoundedHochschild.GNSTendsto.unique line 165
  14. lemma OAI.BoundedHochschild.GNSTendsto.predual line 192
  15. lemma OAI.BoundedHochschild.norm_pow_pos_contraction line 196
  16. theorem OAI.BoundedHochschild.exists_power_projection line 204
  17. structure OAI.BoundedHochschild.IsSupportProjection line 258
  18. lemma OAI.BoundedHochschild.exists_support_contraction line 265
  19. theorem OAI.BoundedHochschild.exists_support_projection line 288
  20. lemma OAI.BoundedHochschild.IsSupportProjection.le_of_support line 308
  21. lemma OAI.BoundedHochschild.IsSupportProjection.unique line 314
  22. lemma OAI.BoundedHochschild.IsSupportProjection.mul_eq_zero_iff line 319
  23. lemma OAI.BoundedHochschild.IsSupportProjection.commute line 327