OAI/Probability/ParisiFinite/ActualCenterPhase.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Actual Center Phase.

  1. theorem OAI.PointedTree.actual_center_phase line 40
  2. theorem OAI.PointedTree.scaled_huge_center_phase line 47
  3. theorem OAI.PointedTree.actual_special_phase_tendsto line 70
  4. theorem OAI.PointedTree.rotated_imaginary line 110
  5. theorem OAI.PointedTree.rotated_projection_tendsto line 121
  6. theorem OAI.PointedTree.actual_special_packet_tendsto line 146
  7. theorem OAI.PointedTree.actual_rotation_on_special line 196
  8. theorem OAI.PointedTree.selective_packet_accuracy line 232
  9. theorem OAI.CoherentFock.spinW_neg_cancel line 286
  10. theorem OAI.CoherentFock.centered_rotation_error line 293
  11. theorem OAI.ForwardControl.difference_sum_remainder_bound line 307
  12. theorem OAI.ForwardControl.scaled_difference_finSum_tendsto line 325
  13. theorem OAI.ForwardControl.scaled_amplitude_error line 344
  14. theorem OAI.ForwardControl.scaled_special_transport line 365
  15. theorem OAI.CoherentFock.scaled_echo_ordinary line 398
  16. def OAI.PointedTree.wordGain line 424
  17. theorem OAI.PointedTree.wordGain_apply line 427
  18. def OAI.PointedTree.echoWord line 432
  19. theorem OAI.PointedTree.probeGain_on_local line 435
  20. theorem OAI.PointedTree.wordGain_echo line 442
  21. theorem OAI.PointedTree.actual_echo_ordinary_scaled line 456
  22. theorem OAI.PacketGeometry.norm_tendsto_of_scaled_square line 494
  23. theorem OAI.PointedTree.actual_huge_packet_phase line 510
  24. lemma OAI.PacketGeometry.finite_positive_floor line 550
  25. lemma OAI.PacketGeometry.imaginary_real_multiple line 570
  26. lemma OAI.PacketGeometry.projection_separation_bound line 576
  27. theorem OAI.PacketGeometry.finite_projection_separation line 588
  28. theorem OAI.PointedTree.standard_center_phase line 616
  29. theorem OAI.PointedTree.huge_ordinary_scaled_phases line 622
  30. theorem OAI.ForwardControl.scaled_identity_transfer line 681