OAI/Analysis/BoundedHochschild/PrimitiveAverages.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Trace preduals, primitives from averages and finite exactness.

  1. def OAI.BoundedHochschild.TraceInPredual line 32
  2. lemma OAI.BoundedHochschild.trace_predual_tendsto line 35
  3. lemma OAI.BoundedHochschild.preGNS_norm_le_of_predual_tendsto line 43
  4. lemma OAI.BoundedHochschild.preGNS_norm_unitary_right line 60
  5. theorem OAI.BoundedHochschild.primitive_from_average line 79
  6. lemma OAI.BoundedHochschild.last_bound_average line 122
  7. lemma OAI.BoundedHochschild.last_bound_iterate line 147
  8. lemma OAI.BoundedHochschild.last_bound_cesaro line 159
  9. theorem OAI.BoundedHochschild.cesaro_limit_last_modulus line 185
  10. def OAI.HochschildWalk.atomicLaw line 213
  11. lemma OAI.HochschildWalk.atomicLaw_probability line 217
  12. lemma OAI.HochschildWalk.integral_atomicLaw line 224
  13. lemma OAI.BoundedHochschild.average_fixed_harmonic line 242
  14. theorem OAI.BoundedHochschild.primitive_of_walk_and_last_modulus line 277
  15. lemma OAI.BoundedHochschild.predual_tendsto_differential line 316
  16. theorem OAI.BoundedHochschild.primitive_of_finite_exactness line 334