OAI/Analysis/BoundedHochschild/Catalan.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Catalan functionals, cutoff decay and positive tracial moments.

  1. lemma OAI.HochschildCatalan.catalan_ratio line 17
  2. def OAI.HochschildCatalan.catalanDifferential line 27
  3. lemma OAI.HochschildCatalan.catalanDifferential_apply line 31
  4. lemma OAI.HochschildCatalan.catalanDifferential_X_pow line 34
  5. lemma OAI.HochschildCatalan.differential_moment_zero line 46
  6. def OAI.HochschildCatalan.cutoff line 57
  7. lemma OAI.HochschildCatalan.catalanDifferential_cutoff_pow line 59
  8. lemma OAI.HochschildCatalan.cutoff_recurrence line 80
  9. lemma OAI.HochschildCatalan.cutoff_moment_sq_le line 89
  10. theorem OAI.HochschildCatalan.cutoff_moment_tendsto_zero line 118
  11. def OAI.HochschildCatalan.momentFunctional line 138
  12. lemma OAI.HochschildCatalan.momentFunctional_apply line 142
  13. lemma OAI.HochschildCatalan.momentFunctional_X_pow line 146
  14. lemma OAI.HochschildCatalan.aeval_cutoff line 151
  15. lemma OAI.HochschildCatalan.cutoff_trace_tendsto_zero line 156
  16. lemma OAI.HochschildCatalan.cutoff_preGNS_tendsto_zero line 163
  17. theorem OAI.HochschildCatalan.eq_zero_of_mul_eq_zero_of_catalan line 183