OAI/Analysis/FreeGroupFactor/LaurentApproximation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.MobiusLog.norm_neg_smul_star_lt line 15
  2. def OAI.FreeGroupFactorMain.MobiusLog.denominator line 23
  3. theorem OAI.FreeGroupFactorMain.MobiusLog.denominator_coe line 26
  4. def OAI.FreeGroupFactorMain.MobiusLog.mobius line 30
  5. theorem OAI.FreeGroupFactorMain.MobiusLog.denominator_add_star_isUnit line 35
  6. theorem OAI.FreeGroupFactorMain.MobiusLog.mobius_add_one_isUnit line 58
  7. theorem OAI.FreeGroupFactorMain.MobiusLog.mobius_norm_sub_one_lt_two line 70
  8. theorem OAI.FreeGroupFactorMain.MobiusLog.mobius_bounded_log line 78
  9. theorem OAI.FreeGroupFactorMain.MobiusLog.mobius_decomp line 84
  10. theorem OAI.FreeGroupFactorMain.MobiusLog.trace_star_mul_denominator_inv line 97
  11. theorem OAI.FreeGroupFactorMain.MobiusLog.trace_star_mul_mobius line 117
  12. abbrev OAI.FreeGroupFactorMain.ElementalMobius.unitaryElemental line 131
  13. def OAI.FreeGroupFactorMain.ElementalMobius.inclusion line 135
  14. theorem OAI.FreeGroupFactorMain.ElementalMobius.inclusion_apply line 140
  15. theorem OAI.FreeGroupFactorMain.ElementalMobius.unitaryElemental_zpow line 144
  16. def OAI.FreeGroupFactorMain.ElementalMobius.value line 151
  17. theorem OAI.FreeGroupFactorMain.ElementalMobius.trace line 155
  18. theorem OAI.FreeGroupFactorMain.ElementalMobius.bounded_log line 164
  19. theorem OAI.FreeGroupFactorMain.twoNorm_one line 182
  20. theorem OAI.FreeGroupFactorMain.twoNorm_unitary line 185
  21. theorem OAI.FreeGroupFactorMain.twoNorm_sub_unitary_sq line 189
  22. def OAI.FreeGroupFactorMain.canonicalTraceContinuous line 202
  23. theorem OAI.FreeGroupFactorMain.canonicalTraceContinuous_apply line 207
  24. theorem OAI.FreeGroupFactorMain.haar_approx_log line 210
  25. def OAI.FreeGroupFactorMain.LaurentApprox.value line 244
  26. def OAI.FreeGroupFactorMain.LaurentApprox.powers line 247
  27. theorem OAI.FreeGroupFactorMain.LaurentApprox.adjoin_mem_span line 254
  28. theorem OAI.FreeGroupFactorMain.LaurentApprox.approx line 268
  29. theorem OAI.FreeGroupFactorMain.LaurentApprox.approx_selfAdjoint line 277
  30. theorem OAI.FreeGroupFactorMain.LaurentApprox.value_add line 303
  31. theorem OAI.FreeGroupFactorMain.LaurentApprox.value_sub line 307
  32. theorem OAI.FreeGroupFactorMain.LaurentApprox.value_single line 311
  33. theorem OAI.FreeGroupFactorMain.LaurentApprox.trace_value line 315
  34. theorem OAI.FreeGroupFactorMain.LaurentApprox.approx_selfAdjoint_exp line 322
  35. theorem OAI.FreeGroupFactorMain.LaurentApprox.center line 344
  36. theorem OAI.FreeGroupFactorMain.haar_centered_laurent line 385