OAI/Probability/ParisiFinite/SpinWZeroApply.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Spin W Zero Apply.

  1. theorem OAI.PointedTree.spinW_zero_apply line 40
  2. theorem OAI.PointedTree.reciprocal_scale_eventually line 46
  3. theorem OAI.PointedTree.standard_selective_accuracy line 58
  4. theorem OAI.PointedTree.huge_selective_accuracy line 113
  5. theorem OAI.ForwardControl.scaled_difference_transfer line 211
  6. theorem OAI.ForwardControl.scaled_map_difference line 233
  7. theorem OAI.ForwardControl.scaled_amplitude_finSum line 246
  8. theorem OAI.ForwardControl.four_forward_transfer line 258
  9. theorem OAI.CoherentFock.half_mixer_anticommutes line 285
  10. theorem OAI.PointedTree.standard_four_forward_errors line 300
  11. theorem OAI.CoherentFock.spinCoe_smul line 374
  12. theorem OAI.CoherentFock.spinMass_smul line 379
  13. theorem OAI.CoherentFock.SpinRadiusLE.smul line 383
  14. theorem OAI.ForwardControl.scaled_identity_add line 392
  15. theorem OAI.ForwardControl.scaled_identity_sub line 406
  16. theorem OAI.ForwardControl.scaled_square_small_amplitude line 417
  17. theorem OAI.PointedTree.actualPacket_smul line 438
  18. theorem OAI.PointedTree.norm_actualPacket_le_mass line 442
  19. theorem OAI.PointedTree.huge_four_forward_errors line 448
  20. def OAI.CoherentFock.BoundedPacket line 560
  21. theorem OAI.CoherentFock.BoundedPacket.norm_bounded line 567
  22. theorem OAI.CoherentFock.BoundedPacket.vacuum line 575
  23. theorem OAI.CoherentFock.BoundedPacket.root line 581
  24. theorem OAI.CoherentFock.BoundedPacket.pulse line 592
  25. theorem OAI.CoherentFock.BoundedPacket.smul line 602
  26. structure OAI.CoherentFock.PacketUnitaryFamily line 617
  27. def OAI.CoherentFock.PacketUnitaryFamily.ident line 624
  28. def OAI.CoherentFock.PacketUnitaryFamily.root line 629
  29. def OAI.CoherentFock.PacketUnitaryFamily.pulse line 634
  30. def OAI.CoherentFock.PacketUnitaryFamily.trans line 642
  31. def OAI.CoherentFock.PacketUnitaryFamily.symm line 647
  32. theorem OAI.CoherentFock.PacketUnitaryFamily.insertion_bounded line 654