OAI/Probability/ParisiFinite/ExpVector.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Exp Vector.

  1. def OAI.CoherentFock.expVector line 17
  2. theorem OAI.CoherentFock.inner_expVector line 20
  3. theorem OAI.CoherentFock.continuous_expVector line 31
  4. theorem OAI.CoherentFock.expVector_zero line 35
  5. theorem OAI.CoherentFock.eq_of_inner_coherent line 37
  6. theorem OAI.CoherentFock.eq_of_inner_expVector line 42
  7. theorem OAI.CoherentFock.map_circleIntegral line 52
  8. def OAI.CoherentFock.oneParticle line 60
  9. theorem OAI.CoherentFock.circleIntegrable_oneParticle_integrand line 63
  10. theorem OAI.CoherentFock.inner_expVector_oneParticle line 72
  11. theorem OAI.CoherentFock.inner_oneParticle_expVector line 94
  12. theorem OAI.CoherentFock.inner_oneParticle line 98
  13. def OAI.CoherentFock.oneParticleEmbedding line 118
  14. theorem OAI.CoherentFock.oneParticle_orthogonal_vacuum line 133
  15. theorem OAI.CoherentFock.norm_oneParticle line 143
  16. theorem OAI.CoherentFock.inner_coherent_oneParticle line 146
  17. theorem OAI.CoherentFock.W_neg_cancel line 159
  18. theorem OAI.CoherentFock.inner_W_right line 162
  19. theorem OAI.CoherentFock.inner_coherent_W_oneParticle line 168
  20. def OAI.CoherentFock.fieldCoherent line 186
  21. theorem OAI.CoherentFock.inner_coherent_field line 189
  22. theorem OAI.CoherentFock.fieldCoherent_symmetric line 209
  23. theorem OAI.CoherentFock.norm_fieldCoherent_le line 218
  24. theorem OAI.CoherentFock.fieldCoherent_weyl_shift line 231
  25. def OAI.CoherentFock.preField line 247
  26. theorem OAI.CoherentFock.preField_basis line 250
  27. theorem OAI.CoherentFock.preField_eq_sum line 254
  28. theorem OAI.CoherentFock.preField_symmetric line 257
  29. theorem OAI.CoherentFock.preField_ker line 266
  30. def OAI.CoherentFock.spanEmbedding line 274
  31. def OAI.CoherentFock.fieldDomain line 277
  32. def OAI.CoherentFock.field line 279
  33. def OAI.CoherentFock.inDomain line 283
  34. theorem OAI.CoherentFock.coe_inDomain line 286
  35. theorem OAI.CoherentFock.field_inDomain line 288
  36. theorem OAI.CoherentFock.field_symmetric line 295
  37. theorem OAI.CoherentFock.preField_weyl_shift line 304
  38. theorem OAI.CoherentFock.coherent_taylor_one line 322
  39. theorem OAI.CoherentFock.coherent_sub_vacuum_le line 356
  40. theorem OAI.CoherentFock.phase_sub_one_le line 367
  41. theorem OAI.CoherentFock.W_coherent_sub_le line 377
  42. def OAI.CoherentFock.tailBound line 402
  43. theorem OAI.CoherentFock.W_coe_sub_le line 405
  44. theorem OAI.CoherentFock.centered_probe line 425
  45. theorem OAI.CoherentFock.unitary_phase_remainder line 452
  46. theorem OAI.CoherentFock.oneParticle_add line 467
  47. theorem OAI.CoherentFock.oneParticle_real_smul line 470
  48. theorem OAI.CoherentFock.coherent_hasFDerivAt_zero line 474
  49. theorem OAI.CoherentFock.W_coherent_reorder line 487
  50. theorem OAI.CoherentFock.W_coherent_taylor line 500
  51. def OAI.CoherentFock.secondTailBound line 544
  52. theorem OAI.CoherentFock.W_coe_taylor line 547
  53. theorem OAI.CoherentFock.fieldCoherent_add line 574
  54. theorem OAI.CoherentFock.fieldCoherent_real_smul line 580
  55. theorem OAI.CoherentFock.preField_real_smul line 590
  56. theorem OAI.CoherentFock.hasDerivAt_W_coe_zero line 599
  57. theorem OAI.CoherentFock.inner_oneParticle_eq_deriv line 627
  58. theorem OAI.CoherentFock.inner_expVector_W_oneParticle line 643
  59. theorem OAI.CoherentFock.inner_W_oneParticle_expVector line 654
  60. theorem OAI.CoherentFock.inner_W_oneParticle_oneParticle line 661
  61. theorem OAI.CoherentFock.W_oneParticle_sub_le line 680