OAI/Probability/ParisiFinite/GramPosSemidef.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Gram Pos Semidef.

  1. theorem OAI.CoherentFock.gram_posSemidef line 23
  2. theorem OAI.CoherentFock.ones_posSemidef line 43
  3. theorem OAI.CoherentFock.entry_pow_posSemidef line 46
  4. theorem OAI.CoherentFock.entry_exp_posSemidef line 54
  5. def OAI.CoherentFock.kernel line 97
  6. theorem OAI.CoherentFock.kernel_posSemidef line 100
  7. def OAI.CoherentFock.PreSpace line 114
  8. instance OAI.CoherentFock.(instance at line 115) line 115
  9. instance OAI.CoherentFock.(instance at line 116) line 116
  10. def OAI.CoherentFock.toFinsupp line 118
  11. abbrev OAI.CoherentFock.core line 122
  12. instance OAI.CoherentFock.(instance at line 146) line 146
  13. instance OAI.CoherentFock.(instance at line 148) line 148
  14. abbrev OAI.CoherentFock.Space line 150
  15. def OAI.CoherentFock.coherent line 153
  16. theorem OAI.CoherentFock.inner_coherent line 156
  17. theorem OAI.CoherentFock.kernel_self line 164
  18. theorem OAI.CoherentFock.norm_coherent line 172
  19. theorem OAI.CoherentFock.kernel_eq line 176
  20. theorem OAI.CoherentFock.norm_kernel line 189
  21. def OAI.CoherentFock.phase line 195
  22. theorem OAI.CoherentFock.norm_phase line 197
  23. theorem OAI.CoherentFock.phase_zero_left line 200
  24. theorem OAI.CoherentFock.phase_zero_right line 201
  25. theorem OAI.CoherentFock.phase_cocycle line 204
  26. theorem OAI.CoherentFock.kernel_translate line 211
  27. def OAI.CoherentFock.basis line 234
  28. theorem OAI.CoherentFock.inner_basis line 236
  29. theorem OAI.CoherentFock.coe_basis line 242
  30. def OAI.CoherentFock.preWLinear line 244
  31. theorem OAI.CoherentFock.preWLinear_basis line 247
  32. theorem OAI.CoherentFock.inner_preW line 252
  33. def OAI.CoherentFock.preW line 270
  34. def OAI.CoherentFock.W line 276
  35. theorem OAI.CoherentFock.W_coe line 278
  36. theorem OAI.CoherentFock.W_coherent line 281
  37. theorem OAI.CoherentFock.norm_W line 284
  38. theorem OAI.CoherentFock.inner_W line 290
  39. theorem OAI.CoherentFock.sum_basis line 300
  40. theorem OAI.CoherentFock.ext_coherent line 309
  41. theorem OAI.CoherentFock.W_zero line 322
  42. theorem OAI.CoherentFock.W_mul line 328
  43. theorem OAI.CoherentFock.phase_neg_left line 334
  44. theorem OAI.CoherentFock.phase_neg_right line 339
  45. def OAI.CoherentFock.weyl line 345
  46. theorem OAI.CoherentFock.weyl_apply line 358
  47. theorem OAI.CoherentFock.norm_inner_translated_coherent line 361
  48. theorem OAI.CoherentFock.continuous_kernel line 366
  49. theorem OAI.CoherentFock.continuous_phase line 370
  50. theorem OAI.CoherentFock.norm_sub_coherent line 374
  51. theorem OAI.CoherentFock.continuous_coherent line 382
  52. def OAI.CoherentFock.preGammaLinear line 397
  53. theorem OAI.CoherentFock.preGammaLinear_basis line 400
  54. theorem OAI.CoherentFock.kernel_map line 405
  55. theorem OAI.CoherentFock.phase_map line 408
  56. theorem OAI.CoherentFock.inner_preGamma line 411
  57. def OAI.CoherentFock.preGamma line 426
  58. def OAI.CoherentFock.Gamma line 431
  59. theorem OAI.CoherentFock.Gamma_coe line 434
  60. theorem OAI.CoherentFock.Gamma_coherent line 437
  61. theorem OAI.CoherentFock.norm_Gamma line 441
  62. theorem OAI.CoherentFock.Gamma_W line 448
  63. theorem OAI.CoherentFock.Gamma_id line 457
  64. theorem OAI.CoherentFock.Gamma_comp line 462
  65. def OAI.CoherentFock.secondQuantization line 472
  66. theorem OAI.CoherentFock.coe_eq_sum line 495
  67. theorem OAI.CoherentFock.tendsto_norm_separated line 503
  68. theorem OAI.CoherentFock.tendsto_inner_translated_coherent line 520
  69. theorem OAI.CoherentFock.tendsto_inner_translated_pre line 535
  70. theorem OAI.CoherentFock.inner_translate_approx line 547
  71. theorem OAI.CoherentFock.tendsto_inner_translated line 564
  72. theorem OAI.CoherentFock.continuous_W_coherent line 589
  73. theorem OAI.CoherentFock.continuous_W_coe line 597
  74. theorem OAI.CoherentFock.continuous_W line 605
  75. theorem OAI.CoherentFock.tendsto_W line 625