OAI/Analysis/InterpolatedFactors/Spectral.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.BicommutantAtom.rankOne_commute_fixed line 15
  2. theorem OAI.FreeGroupFactorMain.BicommutantAtom.rankOne_commute_zero line 24
  3. theorem OAI.FreeGroupFactorMain.BicommutantAtom.scalar_of_rankOne_commutes line 35
  4. theorem OAI.FreeGroupFactorMain.BicommutantAtom.common_kernel_scalar line 62
  5. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mem_edge line 88
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.edge_sum_mem_edge line 92
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_mul_P line 97
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_mem_edge line 100
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_mem_edge line 109
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_mem_edge line 112
  11. def OAI.FreeGroupFactorMain.WeightedFock.edgeDefect line 115
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_projection line 117
  13. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_mem_edge line 120
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_mul_offDiagonal line 123
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mul_edgeDefect line 134
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_mul_P line 137
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeSum_mul_defect line 141
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.edge_algebra_scalar_on_defect line 153
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_trace line 160
  20. theorem OAI.FreeGroupFactorMain.JacobiNonatom.semicircular_eigenvector_zero line 173
  21. def OAI.FreeGroupFactorMain.IsometricSemicircle.chain line 204
  22. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.chain_zero line 207
  23. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.chain_succ line 209
  24. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.inner_map line 213
  25. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.inner_root_succ line 218
  26. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.chain_inner line 224
  27. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.chain_orthonormal line 241
  28. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.chain_coeff_decay line 245
  29. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.adjoint_chain_succ line 253
  30. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.sum_chain_zero line 259
  31. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.sum_chain_succ line 263
  32. theorem OAI.FreeGroupFactorMain.IsometricSemicircle.eigen_root_zero line 270
  33. def OAI.FreeGroupFactorMain.SupportedSemicircle.extension line 294
  34. theorem OAI.FreeGroupFactorMain.SupportedSemicircle.extension_isometry line 297
  35. theorem OAI.FreeGroupFactorMain.SupportedSemicircle.supported_sum_left line 306
  36. theorem OAI.FreeGroupFactorMain.SupportedSemicircle.supported_sum_right line 312
  37. theorem OAI.FreeGroupFactorMain.SupportedSemicircle.eigen_root_zero line 319
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTrace_supported_root line 347
  39. def OAI.FreeGroupFactorMain.WeightedFock.defectCreation line 360
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.defectCreation_left line 363
  41. theorem OAI.FreeGroupFactorMain.WeightedFock.defectCreation_right line 367
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.defectCreation_covariance line 371
  43. theorem OAI.FreeGroupFactorMain.WeightedFock.defectCreation_root line 390
  44. theorem OAI.FreeGroupFactorMain.SupportedSemicircle.unnormalized_eigen_root_zero line 406
  45. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_root_ne_zero line 443
  46. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_root_inner line 452
  47. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_eigen_root_zero line 463