OAI/Probability/ParisiFinite/Joint.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Joint.

  1. abbrev OAI.GaussianFactorization.Joint line 25
  2. abbrev OAI.GaussianFactorization.Hilbert line 26
  3. def OAI.GaussianFactorization.wave line 29
  4. theorem OAI.GaussianFactorization.continuous_wave line 32
  5. theorem OAI.GaussianFactorization.norm_wave line 35
  6. theorem OAI.GaussianFactorization.memLp_wave line 39
  7. def OAI.GaussianFactorization.vector line 43
  8. theorem OAI.GaussianFactorization.vector_ae line 45
  9. theorem OAI.GaussianFactorization.kernel_joint line 48
  10. theorem OAI.GaussianFactorization.inner_vector line 59
  11. def OAI.GaussianFactorization.preMap line 69
  12. def OAI.GaussianFactorization.representation line 87
  13. theorem OAI.GaussianFactorization.representation_coherent line 98
  14. theorem OAI.GaussianFactorization.representation_surjective line 107
  15. def OAI.GaussianFactorization.jointGaussianUnitary line 153
  16. theorem OAI.GaussianFactorization.jointGaussianUnitary_coherent line 156
  17. theorem OAI.GaussianFactorization.memLp_seedPhase line 166
  18. def OAI.GaussianFactorization.seedPhase line 175
  19. theorem OAI.GaussianFactorization.seedPhase_ae line 178
  20. def OAI.GaussianFactorization.seedPhaseIsometry line 182
  21. theorem OAI.GaussianFactorization.phase_inl line 206
  22. theorem OAI.GaussianFactorization.phase_inr line 210
  23. theorem OAI.GaussianFactorization.seedPhase_vector line 214
  24. theorem OAI.GaussianFactorization.representation_W_external line 231
  25. theorem OAI.GaussianFactorization.endogenous_vector line 242
  26. theorem OAI.GaussianFactorization.representation_W_endogenous line 259
  27. theorem OAI.QuantumCLT.exp_remainder_bound line 280
  28. theorem OAI.QuantumCLT.norm_exp_le line 311
  29. theorem OAI.QuantumCLT.exp_second_bound line 315
  30. theorem OAI.QuantumCLT.product_second_bound line 338
  31. def OAI.QuantumCLT.HasSecond line 391
  32. theorem OAI.QuantumCLT.jet_norm_bound line 396
  33. theorem OAI.QuantumCLT.HasSecond.mul line 415
  34. theorem OAI.QuantumCLT.exp_hasSecond line 426
  35. def OAI.QuantumCLT.generators line 438
  36. def OAI.QuantumCLT.second line 440
  37. theorem OAI.QuantumCLT.generators_hasSecond line 444
  38. theorem OAI.QuantumCLT.HasSecond.matrixElement line 454
  39. theorem OAI.QuantumCLT.scalar_scaled_limit line 466
  40. theorem OAI.QuantumCLT.scalar_power_limit line 492
  41. theorem OAI.QuantumCLT.generators_vacuum_limit line 501
  42. def OAI.QuantumCLT.JetBound line 525
  43. theorem OAI.QuantumCLT.JetBound.mul line 530
  44. def OAI.QuantumCLT.exponentialBound line 556
  45. theorem OAI.QuantumCLT.exponentialBound_nonneg line 558
  46. theorem OAI.QuantumCLT.exp_jetBound line 562
  47. def OAI.QuantumCLT.orderedBound line 585
  48. theorem OAI.QuantumCLT.orderedBound_nonneg line 589
  49. theorem OAI.QuantumCLT.generators_jetBound line 599
  50. theorem OAI.QuantumCLT.moving_generators_vacuum_limit line 610