OAI/Probability/ParisiFinite/HugeSelectiveBounded.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Huge Selective Bounded.

  1. theorem OAI.PointedTree.huge_selective_bounded line 43
  2. theorem OAI.CoherentFock.real_neg_div_scale line 155
  3. theorem OAI.CoherentFock.real_div_scale line 161
  4. theorem OAI.CoherentFock.complex_neg_real_smul line 167
  5. theorem OAI.CoherentFock.WZ_split_two line 170
  6. theorem OAI.CoherentFock.rootZ_project_zero line 176
  7. theorem OAI.CoherentFock.rootZ_project_one line 181
  8. def OAI.PointedTree.PacketStage.forwardWord line 197
  9. def OAI.PointedTree.PacketStage.forwardVector line 200
  10. def OAI.PointedTree.PacketStage.forwardCenter line 203
  11. theorem OAI.PointedTree.PacketStage.forwardVector_scale line 206
  12. theorem OAI.PointedTree.PacketStage.forward_special_packets line 210
  13. theorem OAI.PointedTree.PacketStage.exists_huge_selector line 221
  14. def OAI.PointedTree.PacketStage.halfEchoWord line 287
  15. def OAI.PointedTree.PacketStage.reverseVector line 291
  16. def OAI.PointedTree.PacketStage.halfEchoResidual line 295
  17. def OAI.PointedTree.PacketStage.halfEchoPhase line 299
  18. def OAI.PointedTree.PacketStage.halfEchoCenter line 303
  19. def OAI.PointedTree.PacketStage.halfEchoGain line 308
  20. theorem OAI.PointedTree.PacketStage.halfEchoGain_apply line 313
  21. theorem OAI.PointedTree.PacketStage.halfEcho_identity_exact line 323
  22. theorem OAI.PointedTree.PacketStage.reverseVector_scale line 333
  23. def OAI.PointedTree.PacketStage.halfEcho line 341
  24. theorem OAI.PointedTree.PacketStage.forward_four line 409
  25. theorem OAI.PointedTree.PacketStage.halfEchoResidual_tendsto line 447
  26. theorem OAI.PointedTree.PacketStage.halfEchoResidual_bounded line 475
  27. def OAI.CoherentFock.preProject line 497
  28. theorem OAI.CoherentFock.spinCoe_preProject line 499
  29. theorem OAI.CoherentFock.preProject_radius line 506
  30. theorem OAI.CoherentFock.preProject_mass line 515
  31. theorem OAI.CoherentFock.transverse_WZ_bounded line 525
  32. theorem OAI.CoherentFock.unit_opposite_separation line 550
  33. theorem OAI.PointedTree.PacketStage.actual_low_norm line 569
  34. theorem OAI.PointedTree.PacketStage.huge_transverse_bounded line 597
  35. def OAI.CoherentFock.ApproxPacket line 655
  36. theorem OAI.CoherentFock.BoundedPacket.approx line 658
  37. theorem OAI.CoherentFock.ApproxPacket.close line 663
  38. theorem OAI.CoherentFock.ApproxPacket.add line 671
  39. theorem OAI.CoherentFock.ApproxPacket.smul line 683
  40. theorem OAI.CoherentFock.ApproxPacket.neg line 689
  41. theorem OAI.CoherentFock.ApproxPacket.sub line 692
  42. theorem OAI.CoherentFock.ApproxPacket.norm_bounded line 695