OAI/Probability/ParisiFinite/InnerRootYCoordinates.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Inner Root Y Coordinates.

  1. theorem OAI.CoherentFock.inner_rootY_coordinates line 26
  2. theorem OAI.CoherentFock.inner_rootY_spinW_same_plus line 31
  3. theorem OAI.CoherentFock.inner_rootY_spinW_same_minus line 36
  4. def OAI.CoherentFock.hugePacket line 43
  5. theorem OAI.CoherentFock.norm_hugePacket_le line 46
  6. theorem OAI.CoherentFock.inner_rootY_hugePacket line 52
  7. theorem OAI.CoherentFock.tendsto_inner_rootY_hugePacket line 64
  8. theorem OAI.CoherentFock.inner_rootY_error_bound line 93
  9. theorem OAI.CoherentFock.huge_transverse_actual line 109
  10. abbrev OAI.GaussianCoherent.Mode line 151
  11. abbrev OAI.GaussianCoherent.Hilbert line 152
  12. def OAI.GaussianCoherent.offset line 156
  13. def OAI.GaussianCoherent.wave line 158
  14. theorem OAI.GaussianCoherent.continuous_wave line 161
  15. theorem OAI.GaussianCoherent.wave_pair line 165
  16. theorem OAI.GaussianCoherent.integrable_wave_pair line 180
  17. theorem OAI.GaussianCoherent.exponent_pair line 185
  18. theorem OAI.GaussianCoherent.integral_wave_pair line 204
  19. theorem OAI.GaussianCoherent.memLp_wave line 213
  20. def OAI.GaussianCoherent.vector line 222
  21. theorem OAI.GaussianCoherent.vector_ae line 224
  22. theorem OAI.GaussianCoherent.inner_vector line 227
  23. def OAI.GaussianCoherent.preMap line 237
  24. def OAI.GaussianCoherent.representation line 256
  25. theorem OAI.GaussianCoherent.representation_coherent line 266
  26. def OAI.GaussianCoherent.realMode line 280
  27. theorem OAI.GaussianCoherent.realMode_apply line 282
  28. theorem OAI.GaussianCoherent.norm_realMode_sq line 284
  29. theorem OAI.GaussianCoherent.offset_realMode line 288
  30. theorem OAI.GaussianCoherent.wave_realMode line 291
  31. theorem OAI.GaussianCoherent.norm_wave_realMode line 301
  32. theorem OAI.GaussianCoherent.memLp_seedPhase line 305
  33. def OAI.GaussianCoherent.seedPhase line 314
  34. theorem OAI.GaussianCoherent.seedPhase_ae line 317
  35. def OAI.GaussianCoherent.seedPhaseIsometry line 323
  36. theorem OAI.GaussianCoherent.offset_real_add line 348
  37. theorem OAI.GaussianCoherent.phase_wave_real_add line 368
  38. theorem OAI.GaussianCoherent.seedPhase_vector line 377
  39. theorem OAI.GaussianCoherent.representation_W_real line 389
  40. def OAI.FourierDensity.character line 405
  41. theorem OAI.FourierDensity.continuous_character line 407
  42. theorem OAI.FourierDensity.norm_character line 411
  43. theorem OAI.FourierDensity.character_neg line 414
  44. theorem OAI.FourierDensity.integrable_character_mul line 419
  45. theorem OAI.FourierDensity.dual_eq_sum line 424
  46. theorem OAI.FourierDensity.ae_zero_of_real_fourier_zero line 435
  47. theorem OAI.FourierDensity.ae_re_zero_of_fourier_zero line 493
  48. theorem OAI.FourierDensity.ae_zero_of_fourier_zero line 522
  49. theorem OAI.GaussianCoherent.representation_surjective line 548
  50. def OAI.GaussianCoherent.gaussianUnitary line 580
  51. theorem OAI.GaussianCoherent.gaussianUnitary_coherent line 583
  52. theorem OAI.GaussianCoherent.gaussianUnitary_W_real line 586
  53. theorem OAI.CoherentFock.eq_zero_of_inner_coherent line 596