OAI/Probability/ParisiFinite/Compatible.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Compatible.

  1. def OAI.PointedTree.EvenUnitary.Compatible line 19
  2. theorem OAI.PointedTree.EvenUnitary.Compatible.symm_apply line 22
  3. theorem OAI.PointedTree.EvenUnitary.Compatible.insertion line 28
  4. theorem OAI.PointedTree.EvenUnitary.Compatible.followedBy line 36
  5. theorem OAI.PointedTree.EvenUnitary.compatible_ident line 44
  6. theorem OAI.PointedTree.EvenUnitary.compatible_mixer line 46
  7. theorem OAI.PointedTree.EvenUnitary.compatible_cost line 50
  8. inductive OAI.PointedTree.Gate line 61
  9. def OAI.PointedTree.ordinary line 66
  10. theorem OAI.PointedTree.ordinary_compatible line 76
  11. theorem OAI.PointedTree.ordinary_insertion_empty line 95
  12. theorem OAI.CoherentFock.Gamma_expVector line 106
  13. theorem OAI.CoherentFock.Gamma_oneParticle line 109
  14. def OAI.CoherentFock.creationVacuum line 117
  15. def OAI.CoherentFock.creationEmbedding line 119
  16. theorem OAI.CoherentFock.norm_creationVacuum line 127
  17. theorem OAI.CoherentFock.creationVacuum_orthogonal line 129
  18. theorem OAI.CoherentFock.Gamma_creationVacuum line 132
  19. def OAI.PointedTree.plusEmbedding line 142
  20. theorem OAI.PointedTree.plusEmbedding_apply line 157
  21. theorem OAI.PointedTree.plusEmbedding_coherent_zero line 160
  22. theorem OAI.PointedTree.spinMap_plusEmbedding line 163
  23. def OAI.PointedTree.rootShift line 167
  24. theorem OAI.PointedTree.rootShift_coe line 183
  25. theorem OAI.PointedTree.rootShift_empty line 187
  26. def OAI.PointedTree.treeEnergy line 198
  27. theorem OAI.PointedTree.treeEnergy_empty line 201
  28. theorem OAI.PointedTree.treeEnergy_sub_le line 207
  29. def OAI.ProbeProduct.coreAct line 234
  30. theorem OAI.ProbeProduct.coreAct_nil line 238
  31. theorem OAI.ProbeProduct.coreAct_cons line 239
  32. theorem OAI.ProbeProduct.coreAct_bound line 242
  33. theorem OAI.ProbeProduct.core_perturbation_bound line 256
  34. def OAI.CoherentFock.prePhaseZ line 295
  35. theorem OAI.CoherentFock.spinCoe_prePhaseZ line 298
  36. theorem OAI.CoherentFock.spinBound_prePhaseZ line 304
  37. def OAI.CoherentFock.preProbePhase line 308
  38. theorem OAI.CoherentFock.spinCoe_preProbePhase line 311
  39. theorem OAI.CoherentFock.spinBound_preProbePhase line 316
  40. theorem OAI.CoherentFock.norm_probe_sub_le line 326
  41. theorem OAI.CoherentFock.coreAct_preProbePhase line 337
  42. theorem OAI.CoherentFock.centered_product_rotation_bound line 347
  43. theorem OAI.CoherentFock.phaseZ_add line 391
  44. theorem OAI.CoherentFock.phaseZ_sub_phaseZ_le line 400
  45. theorem OAI.CoherentFock.probePhase_sub_probePhase_le line 407
  46. theorem OAI.CoherentFock.rotation_product_bound line 415
  47. theorem OAI.CoherentFock.special_product_bound line 432
  48. theorem OAI.CoherentFock.scaled_translated_spin_bound line 455
  49. theorem OAI.CoherentFock.scaled_spin_matrix_bound line 476
  50. theorem OAI.CoherentFock.rapid_decay_spin_matrix line 491
  51. theorem OAI.PacketGeometry.symmetric_diagonal_im line 535
  52. theorem OAI.PacketGeometry.huge_center_imaginary line 545
  53. theorem OAI.PacketGeometry.inner_remainder_bound line 584
  54. theorem OAI.PacketGeometry.huge_imaginary_modulus line 611