OAI/Probability/ParisiFinite/RotationAccuracy.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Rotation Accuracy.

  1. theorem OAI.CoherentFock.PacketExpansion.rotation_accuracy line 43
  2. theorem OAI.PointedTree.standard_selective_bounded line 70
  3. theorem OAI.SeedInitialization.spinMap_initial line 119
  4. theorem OAI.SeedInitialization.spinMap_special line 124
  5. theorem OAI.SeedInitialization.specialPhase_map line 129
  6. theorem OAI.SeedInitialization.spinMap_address line 134
  7. def OAI.SeedInitialization.addressInfinity line 145
  8. theorem OAI.SeedInitialization.norm_addressInfinity line 147
  9. theorem OAI.SeedInitialization.modeFock_embed_address line 150
  10. theorem OAI.SeedInitialization.modeFock_addressInfinity line 159
  11. theorem OAI.SeedInitialization.addressInfinity_exact line 163
  12. theorem OAI.SeedInitialization.addressInfinity_escapes line 174
  13. theorem OAI.SeedInitialization.highInfinity_lift line 196
  14. theorem OAI.SeedInitialization.high_addressInfinity_orthogonal line 201
  15. structure OAI.PointedTree.PacketStage line 217
  16. theorem OAI.PointedTree.PacketStage.special_vacuum_zero line 238
  17. theorem OAI.PointedTree.PacketStage.low_bounded line 246
  18. theorem OAI.PointedTree.PacketStage.insertion_bound line 254
  19. def OAI.PointedTree.PacketStage.cost line 266
  20. def OAI.SeedInitialization.initialStage line 297
  21. theorem OAI.CoherentFock.projectSpin_rootZ line 330
  22. theorem OAI.CoherentFock.PacketExpansion.rootZ line 336
  23. theorem OAI.CoherentFock.compensated_error line 350
  24. theorem OAI.ForwardControl.scaled_triangle line 364
  25. theorem OAI.ForwardControl.preserve_transport_bound line 376
  26. def OAI.PointedTree.compensatedGain line 394
  27. theorem OAI.PointedTree.compensatedGain_apply line 398
  28. theorem OAI.PointedTree.compensatedGain_local line 402
  29. def OAI.PointedTree.PacketStage.compensated line 413
  30. theorem OAI.PointedTree.PacketStage.exists_compensated line 454
  31. theorem OAI.ForwardControl.scaled_preserve_transport line 499
  32. theorem OAI.CoherentFock.WZ_rootZ_apply line 531
  33. theorem OAI.PointedTree.local_symm_after_gain line 540
  34. theorem OAI.PointedTree.cost_transport_exact line 550
  35. def OAI.PointedTree.PacketStage.Transported line 563
  36. theorem OAI.PointedTree.PacketStage.Transported.cost line 567
  37. theorem OAI.PointedTree.PacketStage.Transported.compensated line 572
  38. theorem OAI.SeedInitialization.initialStage_transported line 610