OAI/Probability/ParisiFinite/ActualDisplacement.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Actual Displacement.

  1. def OAI.PointedTree.actualDisplacement line 37
  2. theorem OAI.PointedTree.norm_actualDisplacement line 40
  3. def OAI.PointedTree.actualTail line 45
  4. theorem OAI.PointedTree.probeGain_packet line 51
  5. theorem OAI.PointedTree.spinMass_actualTail line 61
  6. theorem OAI.PointedTree.spinMass_actualTail_le line 70
  7. theorem OAI.PointedTree.radius_actualTail line 76
  8. theorem OAI.PointedTree.radius_actualTail_le line 88
  9. theorem OAI.PointedTree.rapid_decay_actual_packets line 100
  10. theorem OAI.CoherentFock.phaseZ_zero_apply line 136
  11. theorem OAI.CoherentFock.probePhase_zero_apply line 140
  12. theorem OAI.CoherentFock.ProbeProduct.phase_zero line 144
  13. theorem OAI.CoherentFock.centered_product_forward_bound line 155
  14. theorem OAI.PointedTree.actual_forward_bound line 173
  15. theorem OAI.PointedTree.tendsto_actual_direction line 196
  16. theorem OAI.PulseControl.two_axis_sum line 221
  17. theorem OAI.PulseControl.two_axis_zero_clock line 234
  18. theorem OAI.CoherentFock.probeField_zero_two_clocks line 246
  19. def OAI.PointedTree.actualVelocity line 266
  20. def OAI.PointedTree.startingVelocity line 269
  21. theorem OAI.PointedTree.norm_actualVelocity line 272
  22. theorem OAI.PointedTree.norm_startingVelocity line 276
  23. theorem OAI.PointedTree.norm_velocity_difference line 280
  24. theorem OAI.PointedTree.actualDisplacement_eq_velocity line 285
  25. theorem OAI.PointedTree.actual_zero_clock_bound line 293
  26. theorem OAI.PacketGeometry.tendsto_of_scaled line 335
  27. theorem OAI.PacketGeometry.huge_imaginary_scaled_tendsto line 344
  28. def OAI.RootSpin.rotatedZ line 379
  29. theorem OAI.RootSpin.rotatedZ_star line 381
  30. theorem OAI.RootSpin.rotatedZ_unitary line 384
  31. theorem OAI.RootSpin.rotatedZ_symmetric line 387
  32. theorem OAI.PointedTree.actual_huge_phase_modulus line 400
  33. theorem OAI.PacketGeometry.scaled_norm_sum_tendsto line 443
  34. def OAI.PointedTree.actualPacket line 463
  35. theorem OAI.PointedTree.actualPacket_root line 466
  36. def OAI.PointedTree.hugeCrossError line 472
  37. theorem OAI.PointedTree.actual_huge_phase_tendsto line 484
  38. theorem OAI.PointedTree.rapid_actual_packet_sum_right line 518
  39. theorem OAI.RootSpin.matrixMass_Z line 548
  40. theorem OAI.PointedTree.rapid_actual_packet_sum_left line 557
  41. theorem OAI.PointedTree.hugeCrossError_packets_tendsto line 580
  42. theorem OAI.PointedTree.actual_forward_tendsto line 639
  43. theorem OAI.PointedTree.actual_zero_clock_tendsto line 662