OAI/Probability/ParisiFinite/SecondCoefficient.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Second Coefficient.

  1. def OAI.QuantumCLT.secondCoefficient line 25
  2. theorem OAI.QuantumCLT.second_matrixElement line 29
  3. theorem OAI.QuantumCLT.secondCoefficient_tendsto line 46
  4. theorem OAI.QuantumCLT.moving_generators_gram_limit line 61
  5. theorem OAI.QuantumCLT.scalar_first_limit line 78
  6. theorem OAI.QuantumCLT.step_tendsto_one line 111
  7. theorem OAI.QuantumCLT.scalar_power_pred_limit line 125
  8. theorem OAI.QuantumCLT.scalar_inserted_limit line 139
  9. theorem OAI.QuantumCLT.JetBound.insertion line 153
  10. theorem OAI.QuantumCLT.JetBound.vacuum line 181
  11. theorem OAI.QuantumCLT.sqrt_inverse_bound line 192
  12. theorem OAI.QuantumCLT.sqrt_inverse_sq line 199
  13. theorem OAI.QuantumCLT.moving_generators_inserted_limit line 204
  14. def OAI.QuantumCLT.weylProduct line 246
  15. theorem OAI.QuantumCLT.secondCoefficient_gram_cons line 250
  16. theorem OAI.QuantumCLT.gram_exponent line 260
  17. theorem OAI.QuantumCLT.weylProduct_coherent_zero line 268
  18. theorem OAI.QuantumCLT.weylProduct_vacuum line 280
  19. theorem OAI.QuantumCLT.secondCoefficient_map line 291
  20. theorem OAI.QuantumCLT.moving_generators_weyl_limit line 300
  21. def OAI.FiniteTensor.power line 321
  22. theorem OAI.FiniteTensor.power_apply line 325
  23. theorem OAI.FiniteTensor.inner_power line 330
  24. def OAI.FiniteTensor.matrixPower line 341
  25. theorem OAI.FiniteTensor.matrixPower_mulVec line 344
  26. def OAI.FiniteTensor.operatorPower line 357
  27. theorem OAI.FiniteTensor.operatorPower_apply line 362
  28. theorem OAI.FiniteTensor.inner_operatorPower line 372
  29. def OAI.QuantumCLT.vacuumFunctional line 385
  30. theorem OAI.QuantumCLT.vacuumFunctional_apply line 388
  31. theorem OAI.QuantumCLT.vacuumFunctional_norm line 391
  32. def OAI.QuantumCLT.testGate line 403
  33. theorem OAI.QuantumCLT.testGate_jetBound line 407
  34. def OAI.QuantumCLT.testedGate line 415
  35. theorem OAI.QuantumCLT.testedGate_pairing line 419
  36. def OAI.QuantumCLT.testedBound line 431
  37. theorem OAI.QuantumCLT.testedBound_nonneg line 434
  38. theorem OAI.QuantumCLT.testedGate_jetBound line 437
  39. theorem OAI.QuantumCLT.testedGate_first line 455
  40. theorem OAI.QuantumCLT.testedGate_second line 462
  41. theorem OAI.QuantumCLT.tested_pairing_bound line 472
  42. theorem OAI.QuantumCLT.moving_tested_limit line 492
  43. def OAI.FiniteTensor.exponentialVector line 521
  44. theorem OAI.FiniteTensor.moving_tensor_pairing_limit line 527
  45. theorem OAI.FiniteTensor.moving_tensor_gram_limit line 548
  46. def OAI.FiniteTensor.mixedPower line 574
  47. theorem OAI.FiniteTensor.mixedPower_constant line 578
  48. theorem OAI.FiniteTensor.inner_mixedPower line 581
  49. def OAI.FiniteTensor.mixedMatrix line 590
  50. theorem OAI.FiniteTensor.mixedMatrix_mulVec line 593
  51. def OAI.FiniteTensor.mixedOperator line 606
  52. theorem OAI.FiniteTensor.mixedOperator_apply line 612
  53. theorem OAI.FiniteTensor.inner_mixedOperator line 624
  54. theorem OAI.FiniteTensor.prod_one_marked line 632
  55. def OAI.FiniteTensor.insertionSum line 646
  56. theorem OAI.FiniteTensor.inner_insertionSum line 650
  57. def OAI.FiniteTensor.normalizedInsertion line 665
  58. theorem OAI.FiniteTensor.inner_normalizedInsertion line 670
  59. def OAI.QuantumCLT.markedFunctional line 696
  60. theorem OAI.QuantumCLT.markedFunctional_apply line 699
  61. theorem OAI.QuantumCLT.markedFunctional_norm line 702