OAI/Analysis/InterpolatedFactors/Basic.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.Amplification.corner_one_val line 20
  2. theorem OAI.FreeGroupFactorMain.Amplification.corner_mul_val line 23
  3. theorem OAI.FreeGroupFactorMain.Amplification.map_projection line 26
  4. def OAI.FreeGroupFactorMain.Amplification.cornerCongr line 29
  5. theorem OAI.FreeGroupFactorMain.Amplification.cornerCongr_normal line 53
  6. theorem OAI.FreeGroupFactorMain.Amplification.normalizedCornerTrace_one line 65
  7. theorem OAI.FreeGroupFactorMain.Amplification.cornerCongr_trace line 71
  8. def OAI.FreeGroupFactorMain.Amplification.HasAmplificationIso line 83
  9. abbrev OAI.FreeGroupFactorMain.FreeFock.Hilbert line 95
  10. def OAI.FreeGroupFactorMain.Amplification.subalgebraEquiv line 106
  11. abbrev OAI.FreeGroupFactorMain.Amplification.NestedHilbert line 129
  12. def OAI.FreeGroupFactorMain.Amplification.nestedDirac line 131
  13. theorem OAI.FreeGroupFactorMain.Amplification.nestedDirac_inner line 135
  14. theorem OAI.FreeGroupFactorMain.Amplification.nestedDirac_inner_apply line 145
  15. theorem OAI.FreeGroupFactorMain.Amplification.nestedDirac_orthogonal line 150
  16. def OAI.FreeGroupFactorMain.Amplification.nestedBasis line 160
  17. theorem OAI.FreeGroupFactorMain.Amplification.nestedBasis_apply line 163
  18. def OAI.FreeGroupFactorMain.Amplification.hilbertFlatten line 166
  19. theorem OAI.FreeGroupFactorMain.Amplification.hilbertFlatten_apply line 169
  20. theorem OAI.FreeGroupFactorMain.Amplification.hilbertFlatten_symm_apply line 173
  21. def OAI.FreeGroupFactorMain.Amplification.diagonalValue line 179
  22. theorem OAI.FreeGroupFactorMain.Amplification.diagonalValue_norm_le line 182
  23. theorem OAI.FreeGroupFactorMain.Amplification.diagonalValue_add line 189
  24. theorem OAI.FreeGroupFactorMain.Amplification.diagonalValue_smul line 195
  25. theorem OAI.FreeGroupFactorMain.Amplification.continuous_diagonalValue line 201
  26. def OAI.FreeGroupFactorMain.Amplification.diagonalOp line 210
  27. theorem OAI.FreeGroupFactorMain.Amplification.diagonalOp_apply line 217
  28. theorem OAI.FreeGroupFactorMain.Amplification.diagonalOp_star line 220
  29. def OAI.FreeGroupFactorMain.Amplification.diagonalHom line 234
  30. def OAI.FreeGroupFactorMain.Amplification.productAmplification line 243
  31. theorem OAI.FreeGroupFactorMain.Amplification.productAmplification_apply line 246
  32. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedRightTranslations_eq_range line 261
  33. def OAI.FreeGroupFactorMain.Amplification.pairedIndex line 285
  34. def OAI.FreeGroupFactorMain.Amplification.stabilizationFlatten line 288
  35. theorem OAI.FreeGroupFactorMain.Amplification.pairedIndex_symm_apply line 291
  36. def OAI.FreeGroupFactorMain.Amplification.doubleRight line 295
  37. theorem OAI.FreeGroupFactorMain.Amplification.doubleRight_star line 298
  38. theorem OAI.FreeGroupFactorMain.Amplification.flatten_doubleRight line 301
  39. def OAI.FreeGroupFactorMain.Amplification.doubleStabilization line 314
  40. theorem OAI.FreeGroupFactorMain.Amplification.mem_stabilization_iff_right line 317
  41. theorem OAI.FreeGroupFactorMain.Amplification.mem_doubleStabilization_iff_right line 328
  42. theorem OAI.FreeGroupFactorMain.Amplification.flatten_mem_stabilization line 337
  43. def OAI.FreeGroupFactorMain.Amplification.flattenStabilizationIso line 351
  44. def OAI.FreeGroupFactorMain.Amplification.doubleDiagonal line 355
  45. def OAI.FreeGroupFactorMain.Amplification.repeatFlatten line 364
  46. theorem OAI.FreeGroupFactorMain.Amplification.doubleDiagonal_projection line 366
  47. theorem OAI.FreeGroupFactorMain.Amplification.repeatFlatten_projection line 372
  48. abbrev OAI.FreeGroupFactorMain.Amplification.CornerStabilization line 384
  49. def OAI.FreeGroupFactorMain.Amplification.cornerStabilizationTopology line 387
  50. def OAI.FreeGroupFactorMain.Amplification.cornerStabilizationProjectionTrace line 391
  51. def OAI.FreeGroupFactorMain.Amplification.cornerStabilizationTrace line 395
  52. def OAI.FreeGroupFactorMain.Interpolation.Model.Valid line 405
  53. def OAI.FreeGroupFactorMain.Interpolation.Model.Stabilization line 410
  54. instance OAI.FreeGroupFactorMain.Interpolation.modelStabilizationCStarAlgebra line 416
  55. def OAI.FreeGroupFactorMain.Interpolation.Model.stabilizationTopology line 419
  56. def OAI.FreeGroupFactorMain.Interpolation.Model.projectionTrace line 425
  57. def OAI.FreeGroupFactorMain.Interpolation.Model.stabilizationTrace line 431
  58. abbrev OAI.FreeGroupFactorMain.Interpolation.Model.Iso line 437
  59. abbrev OAI.FreeGroupFactorMain.Interpolation.Model.AmplificationIso line 439
  60. def OAI.FreeGroupFactorMain.Interpolation.Model.fundamentalGroup line 443
  61. abbrev OAI.FreeGroupFactorMain.Interpolation.interpolatedStabilization line 447
  62. abbrev OAI.FreeGroupFactorMain.Interpolation.interpolatedProjectionTrace line 448
  63. abbrev OAI.FreeGroupFactorMain.Interpolation.interpolatedStabilizationTrace line 449
  64. abbrev OAI.FreeGroupFactorMain.Interpolation.interpolatedStabilizationTopology line 450
  65. abbrev OAI.FreeGroupFactorMain.Interpolation.fundamentalGroup line 451
  66. def OAI.FreeGroupFactorMain.Interpolation.standardCornerScale line 453