OAI/Analysis/InterpolatedFactors/Polar.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.Amplification.Polar.Operator line 14
  2. def OAI.FreeGroupFactorMain.Amplification.Polar.modulus line 16
  3. theorem OAI.FreeGroupFactorMain.Amplification.Polar.modulus_star line 18
  4. theorem OAI.FreeGroupFactorMain.Amplification.Polar.modulus_sq line 21
  5. theorem OAI.FreeGroupFactorMain.Amplification.Polar.modulus_norm line 24
  6. def OAI.FreeGroupFactorMain.Amplification.Polar.closedRange line 35
  7. instance OAI.FreeGroupFactorMain.Amplification.Polar.closedRange_complete line 37
  8. def OAI.FreeGroupFactorMain.Amplification.Polar.intoClosedRange line 40
  9. theorem OAI.FreeGroupFactorMain.Amplification.Polar.intoClosedRange_dense line 44
  10. def OAI.FreeGroupFactorMain.Amplification.Polar.polarSpatial line 50
  11. theorem OAI.FreeGroupFactorMain.Amplification.Polar.polarSpatial_modulus line 55
  12. def OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry line 59
  13. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_factorization line 63
  14. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_on_range line 72
  15. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_inner line 77
  16. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_initial line 85
  17. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_adjoint line 94
  18. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_final line 106
  19. theorem OAI.FreeGroupFactorMain.Amplification.Polar.modulus_commute line 118
  20. theorem OAI.FreeGroupFactorMain.Amplification.Polar.closedRange_invariant line 123
  21. theorem OAI.FreeGroupFactorMain.Amplification.Polar.orthogonal_invariant line 132
  22. theorem OAI.FreeGroupFactorMain.Amplification.Polar.starProjection_commute line 140
  23. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_projection line 151
  24. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_commute line 160
  25. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_mem_centralizer line 194
  26. theorem OAI.FreeGroupFactorMain.Amplification.Polar.closedRange_eq_orthogonal_ker line 209
  27. theorem OAI.FreeGroupFactorMain.Amplification.Polar.modulus_ker line 214
  28. theorem OAI.FreeGroupFactorMain.Amplification.Polar.modulus_closedRange line 222
  29. theorem OAI.FreeGroupFactorMain.Amplification.Polar.closedRange_projection_mem_centralizer line 225
  30. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_nonzero line 232
  31. theorem OAI.FreeGroupFactorMain.Amplification.Polar.fixed_on_closedRange line 241
  32. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_left_support line 252
  33. theorem OAI.FreeGroupFactorMain.Amplification.Polar.modulus_right_support line 258
  34. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_right_support line 266
  35. theorem OAI.FreeGroupFactorMain.Amplification.Polar.partialIsometry_partial line 278
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.weighted_creation_norm line 293
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.weighted_creation_opNorm_le line 296
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.P_creation_true line 301
  39. def OAI.FreeGroupFactorMain.WeightedFock.offDiagonal line 306
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_formula line 308
  41. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_right line 323
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_left line 328
  43. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_lower_bound line 332
  44. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_ker line 357
  45. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_mem_ambient line 377
  46. theorem OAI.FreeGroupFactorMain.Amplification.Polar.kernel_orthogonal_projection line 386
  47. def OAI.FreeGroupFactorMain.WeightedFock.edgePolar line 411
  48. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_mem_ambient line 413
  49. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_initial line 417
  50. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_left line 422
  51. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_right line 425
  52. def OAI.FreeGroupFactorMain.WeightedFock.edgeRange line 428
  53. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_projection line 430
  54. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_mem_ambient line 434
  55. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_le_P line 437
  56. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_trace line 440
  57. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_apply line 462
  58. theorem OAI.FreeGroupFactorMain.WeightedFock.creation_apply_prepend line 468
  59. theorem OAI.FreeGroupFactorMain.WeightedFock.P_apply_prepend_true line 477
  60. def OAI.FreeGroupFactorMain.WeightedFock.alternatingExtension line 481
  61. theorem OAI.FreeGroupFactorMain.WeightedFock.alternatingExtension_length line 486
  62. theorem OAI.FreeGroupFactorMain.WeightedFock.alternatingExtension_injective line 493
  63. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_balanced_recurrence line 500
  64. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_balanced_injective line 512
  65. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_ker_balanced line 532
  66. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_initial_balanced line 548
  67. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_trace_balanced line 553
  68. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeRange_balanced line 568