OAI/Probability/ParisiFinite/Act.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Act.

  1. def OAI.ProbeProduct.act line 17
  2. theorem OAI.ProbeProduct.act_nil line 21
  3. theorem OAI.ProbeProduct.act_cons line 22
  4. theorem OAI.ProbeProduct.norm_act_le line 25
  5. theorem OAI.ProbeProduct.firstOrder_remainder line 34
  6. theorem OAI.ProbeProduct.zero_clock_remainder line 101
  7. theorem OAI.ProbeProduct.error_of_norm_remainder line 112
  8. theorem OAI.CoherentFock.matrixMass_nonneg line 130
  9. theorem OAI.CoherentFock.scaled_probe_error line 135
  10. theorem OAI.CoherentFock.zero_clock_spin_probes line 159
  11. def OAI.CoherentFock.mass line 212
  12. theorem OAI.CoherentFock.mass_nonneg line 215
  13. def OAI.CoherentFock.RadiusLE line 221
  14. theorem OAI.CoherentFock.translated_coherent_bound line 224
  15. theorem OAI.CoherentFock.translated_pre_bound line 239
  16. theorem OAI.CoherentFock.scaled_translated_pre_bound line 269
  17. theorem OAI.CoherentFock.rapid_decay line 287
  18. theorem OAI.CoherentFock.mass_basis line 324
  19. theorem OAI.CoherentFock.mass_zero line 329
  20. theorem OAI.CoherentFock.mass_add_le line 332
  21. theorem OAI.CoherentFock.mass_smul line 337
  22. theorem OAI.CoherentFock.mass_sum line 342
  23. theorem OAI.CoherentFock.RadiusLE.zero line 352
  24. theorem OAI.CoherentFock.RadiusLE.basis line 355
  25. theorem OAI.CoherentFock.RadiusLE.add line 360
  26. theorem OAI.CoherentFock.RadiusLE.smul line 370
  27. theorem OAI.CoherentFock.RadiusLE.sum line 377
  28. theorem OAI.CoherentFock.RadiusLE.mono line 388
  29. theorem OAI.CoherentFock.mass_preW_le line 391
  30. theorem OAI.CoherentFock.RadiusLE.preW line 402
  31. theorem OAI.CoherentFock.secondTailBound_le_mass line 413
  32. theorem OAI.CoherentFock.finite_packet_displacement line 423
  33. theorem OAI.CoherentFock.mass_preGamma_le line 435
  34. theorem OAI.CoherentFock.RadiusLE.preGamma line 447
  35. def OAI.CoherentFock.spinMass line 458
  36. def OAI.CoherentFock.SpinRadiusLE line 460
  37. theorem OAI.CoherentFock.spinMass_nonneg line 463
  38. theorem OAI.CoherentFock.mass_le_spinMass line 467
  39. theorem OAI.CoherentFock.spinMass_preRoot line 471
  40. theorem OAI.CoherentFock.SpinRadiusLE.preRoot line 489
  41. theorem OAI.CoherentFock.spinBound_le_mass line 495
  42. def OAI.CoherentFock.preWZ line 501
  43. theorem OAI.CoherentFock.spinCoe_preWZ line 504
  44. theorem OAI.CoherentFock.spinMass_preWZ line 508
  45. theorem OAI.CoherentFock.SpinRadiusLE.preWZ line 511
  46. def OAI.CoherentFock.preProbe line 520
  47. theorem OAI.CoherentFock.spinCoe_preProbe line 523
  48. theorem OAI.CoherentFock.spinMass_preProbe line 527
  49. theorem OAI.CoherentFock.SpinRadiusLE.preProbe line 537
  50. theorem OAI.ProbeProduct.perturbation_bound line 548
  51. def OAI.CoherentFock.spinW line 581
  52. theorem OAI.CoherentFock.spinW_apply line 585
  53. theorem OAI.CoherentFock.norm_spinW line 587
  54. theorem OAI.CoherentFock.spinW_root line 593
  55. def OAI.CoherentFock.phaseZ line 598
  56. theorem OAI.CoherentFock.phaseZ_apply line 602
  57. theorem OAI.CoherentFock.norm_phaseZ line 606
  58. theorem OAI.CoherentFock.phaseZ_sub_le line 612
  59. theorem OAI.CoherentFock.centered_WZ line 633
  60. def OAI.CoherentFock.probePhase line 644
  61. theorem OAI.CoherentFock.probePhase_apply line 647
  62. theorem OAI.CoherentFock.norm_probePhase line 650
  63. theorem OAI.CoherentFock.probePhase_sub_le line 654
  64. theorem OAI.CoherentFock.root_right_inverse line 663
  65. theorem OAI.CoherentFock.centered_toggled_probe line 669