OAI/Probability/ParisiFinite/NegativeFlip.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Negative Flip.

  1. def OAI.PointedTree.PacketStage.negativeFlip line 43
  2. theorem OAI.PointedTree.PacketStage.Transported.negativeFlip line 73
  3. theorem OAI.CoherentFock.inner_im_signed_self line 109
  4. theorem OAI.PointedTree.PacketStage.exists_standard_selector line 129
  5. theorem OAI.PointedTree.PacketStage.exists_huge_selector_visible line 156
  6. theorem OAI.PointedTree.PacketStage.exists_negativeFlip line 186
  7. theorem OAI.PointedTree.PacketStage.halfEchoCenter_bounded line 220
  8. theorem OAI.PointedTree.PacketStage.halfEchoCenter_approx line 235
  9. theorem OAI.PointedTree.PacketStage.exists_halfEcho line 257
  10. def OAI.GramCalculus.WeylWord.family line 299
  11. theorem OAI.GramCalculus.WeylWord.low_insertion_match line 304
  12. theorem OAI.PointedTree.PacketStage.actual_insertion_match line 325
  13. theorem OAI.PointedTree.PacketStage.insertionZ_match line 339
  14. theorem OAI.PointedTree.PacketStage.insertionY_match line 347
  15. theorem OAI.CoherentFock.ApproxPacket.inner_escape line 366
  16. def OAI.SeedInitialization.seedDirections line 384
  17. def OAI.SeedInitialization.seedBasis line 387
  18. theorem OAI.SeedInitialization.norm_seedDirections line 389
  19. theorem OAI.SeedInitialization.seedBasis_inner line 393
  20. theorem OAI.SeedInitialization.seedDirections_gram line 399
  21. theorem OAI.SeedInitialization.seedDirections_escape line 419
  22. theorem OAI.SeedInitialization.extend_dictionary line 431
  23. theorem OAI.GramCalculus.combination_map line 477
  24. theorem OAI.GramCalculus.combination_sum_zero line 481
  25. theorem OAI.GramCalculus.PacketMatch.model_map line 490
  26. theorem OAI.GramCalculus.PacketMatch.weaken line 499
  27. theorem OAI.GramCalculus.PacketMatch.reindex line 507
  28. theorem OAI.GramCalculus.ApproxMatch.model_map line 521
  29. theorem OAI.GramCalculus.ApproxMatch.weaken line 526
  30. theorem OAI.GramCalculus.ApproxMatch.reindex line 531
  31. theorem OAI.GramCalculus.GramConverges.model_map line 541
  32. theorem OAI.GramCalculus.GramConverges.reindex line 547
  33. structure OAI.SeedInitialization.CausalFrame line 562
  34. def OAI.SeedInitialization.CausalFrame.directions line 580
  35. def OAI.SeedInitialization.CausalFrame.model line 583
  36. def OAI.SeedInitialization.CausalFrame.initial line 587
  37. def OAI.SeedInitialization.CausalFrame.append line 603
  38. theorem OAI.PointedTree.modeFock_shift line 678
  39. theorem OAI.PointedTree.energyInfinity_fock line 696