OAI/Analysis/FreeGroupFactor/FreeSum.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.ConjugateSectors.basisAction line 16
  2. abbrev OAI.FreeGroupFactorMain.ConjugateSectors.Witness line 29
  3. theorem OAI.FreeGroupFactorMain.ConjugateSectors.basisAction_of line 31
  4. def OAI.FreeGroupFactorMain.ConjugateSectors.witness line 35
  5. theorem OAI.FreeGroupFactorMain.ConjugateSectors.witness_some line 40
  6. theorem OAI.FreeGroupFactorMain.ConjugateSectors.witness_none line 48
  7. def OAI.FreeGroupFactorMain.ConjugateSectors.conjugate line 52
  8. theorem OAI.FreeGroupFactorMain.ConjugateSectors.witness_conjugate line 55
  9. def OAI.FreeGroupFactorMain.ConjugateSectors.begins line 60
  10. theorem OAI.FreeGroupFactorMain.ConjugateSectors.begins_unique line 63
  11. theorem OAI.FreeGroupFactorMain.ConjugateSectors.reduce_prepend line 70
  12. theorem OAI.FreeGroupFactorMain.ConjugateSectors.begins_pow_mul line 91
  13. def OAI.FreeGroupFactorMain.ConjugateSectors.sector line 112
  14. theorem OAI.FreeGroupFactorMain.ConjugateSectors.sector_disjoint line 115
  15. theorem OAI.FreeGroupFactorMain.ConjugateSectors.sector_prefix line 121
  16. abbrev OAI.FreeGroupFactorMain.CoordinateProjection.Hilbert line 134
  17. def OAI.FreeGroupFactorMain.CoordinateProjection.restrict line 136
  18. theorem OAI.FreeGroupFactorMain.CoordinateProjection.restrict_apply line 142
  19. theorem OAI.FreeGroupFactorMain.CoordinateProjection.norm_restrict_le line 145
  20. def OAI.FreeGroupFactorMain.CoordinateProjection.linearMap line 152
  21. def OAI.FreeGroupFactorMain.CoordinateProjection.proj line 163
  22. theorem OAI.FreeGroupFactorMain.CoordinateProjection.proj_apply line 168
  23. theorem OAI.FreeGroupFactorMain.CoordinateProjection.norm_proj_le line 171
  24. theorem OAI.FreeGroupFactorMain.CoordinateProjection.star_proj line 177
  25. theorem OAI.FreeGroupFactorMain.CoordinateProjection.proj_orthogonal line 186
  26. theorem OAI.FreeGroupFactorMain.CoordinateProjection.complement_apply line 197
  27. theorem OAI.FreeGroupFactorMain.FreeSum.norm_sum_sq line 210
  28. theorem OAI.FreeGroupFactorMain.FreeSum.norm_sum_orthogonal line 229
  29. theorem OAI.FreeGroupFactorMain.FreeSum.norm_weighted_sum_orthogonal line 256
  30. theorem OAI.FreeGroupFactorMain.FreeSum.three_block_bound line 276
  31. theorem OAI.FreeGroupFactorMain.operator_eq_zero_of_single line 332
  32. theorem OAI.FreeGroupFactorMain.sector_compression line 338
  33. theorem OAI.FreeGroupFactorMain.concrete_free_sum line 370
  34. theorem OAI.FreeGroupFactorMain.groupUnitary_mul line 391
  35. theorem OAI.FreeGroupFactorMain.groupUnitary_inv line 396
  36. theorem OAI.FreeGroupFactorMain.groupUnitary_one line 401
  37. def OAI.FreeGroupFactorMain.groupLaurent line 405
  38. theorem OAI.FreeGroupFactorMain.groupLaurent_conjugate line 408
  39. theorem OAI.FreeGroupFactorMain.groupLaurent_coe line 417
  40. theorem OAI.FreeGroupFactorMain.groupLaurent_support line 423
  41. theorem OAI.FreeGroupFactorMain.centered_laurent_free_sum line 441