OAI/Analysis/BoundedHochschild/PolarApproximation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Newton polar polynomials and normalized free sums.

  1. def OAI.HochschildNewtonPolar.polarPoly line 18
  2. def OAI.HochschildNewtonPolar.defectPoly line 22
  3. lemma OAI.HochschildNewtonPolar.defect_succ line 24
  4. lemma OAI.HochschildNewtonPolar.eval_defect_bounds line 31
  5. lemma OAI.HochschildNewtonPolar.eval_defect_le_one line 55
  6. def OAI.HochschildNewtonPolar.polarApprox line 63
  7. lemma OAI.HochschildNewtonPolar.aeval_selfAdjoint line 66
  8. lemma OAI.HochschildNewtonPolar.polarApprox_defect line 72
  9. lemma OAI.HochschildNewtonPolar.spectrum_star_mul_bound line 88
  10. lemma OAI.HochschildNewtonPolar.defect_nonneg line 98
  11. lemma OAI.HochschildNewtonPolar.polarApprox_norm_le_one line 106
  12. lemma OAI.HochschildNewtonPolar.defect_le_cutoff line 113
  13. def OAI.HochschildFreeSums.freeSum line 137
  14. lemma OAI.HochschildFreeSums.collisionCard_of_injective line 140
  15. lemma OAI.HochschildFreeSums.norm_freeSum_le_two line 151
  16. lemma OAI.HochschildFreeSums.star_mul_freeSum line 168
  17. def OAI.HochschildFreeSums.catalanFunctional line 180
  18. lemma OAI.HochschildFreeSums.catalanFunctional_X_pow line 183
  19. lemma OAI.HochschildFreeSums.polynomial_moments_tendsto line 190
  20. lemma OAI.HochschildFreeSums.freeSum_moments_tendsto line 203
  21. lemma OAI.HochschildFreeSums.cutoff_catalan_tendsto_zero line 215