OAI/Probability/ThorpRouting/Adaptive/ModifiedStageEquiv.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Adaptive.Thorp.modifiedStageEquiv line 11
  2. lemma OAI.ThorpNine.Adaptive.Thorp.modifiedStageEquiv_apply line 17
  3. lemma OAI.ThorpNine.Adaptive.Thorp.palindrome_stage line 26
  4. def OAI.ThorpNine.Adaptive.Thorp.localModifiedPerm line 37
  5. lemma OAI.ThorpNine.Adaptive.Thorp.modified_stage line 41
  6. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator_sandwich line 63
  7. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.localModified_average line 70
  8. lemma OAI.ThorpNine.Adaptive.Thorp.sampleOperator_palindrome_stage line 86
  9. lemma OAI.ThorpNine.Adaptive.Thorp.sampleOperator_modified_stage line 102
  10. def OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.retain line 127
  11. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.retain_commute line 131
  12. lemma OAI.ThorpNine.Adaptive.Thorp.CommutingBlocks.blocks_retain line 137
  13. def OAI.ThorpNine.Adaptive.Thorp.ParallelBlocks.centralProjection line 161
  14. lemma OAI.ThorpNine.Adaptive.Thorp.ParallelBlocks.centralProjection_commute line 165
  15. lemma OAI.ThorpNine.Adaptive.Thorp.ParallelBlocks.local_central_commute line 171
  16. lemma OAI.ThorpNine.Adaptive.Thorp.modified_central_average line 188
  17. lemma OAI.ThorpNine.Adaptive.Thorp.central_local_gap line 201
  18. lemma OAI.ThorpNine.Adaptive.Thorp.central_blocks_exception_bound line 208
  19. theorem OAI.ThorpNine.Adaptive.Thorp.palindrome_exception_bound line 228
  20. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.actionKernel line 251
  21. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.actionKernel_apply line 255
  22. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.randomOperator line 274
  23. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.coefficient_random line 278
  24. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.fixedSpace line 296
  25. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.operator_amplification line 303
  26. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.tupleAction line 336
  27. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.tupleAction_apply line 346
  28. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.tupleAction_transitive line 350
  29. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.tupleAction_fixed_iff line 355
  30. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.tupleAction_kernel line 366
  31. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.irreducible_of_equiv line 378
  32. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.unitaryRepresentation_coe line 395
  33. def OAI.ThorpNine.Adaptive.Thorp.Specht.unitaryEquiv line 403
  34. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.unitaryRepresentation_irreducible line 413
  35. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.unitaryRepresentation_unitary line 418
  36. def OAI.ThorpNine.Adaptive.Thorp.Specht.tupleFixedEquiv line 427
  37. theorem OAI.ThorpNine.Adaptive.Thorp.Specht.tupleFixed_dimension line 445
  38. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator_inv_apply line 462
  39. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator_amplification line 467
  40. def OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.subrepresentationEquiv line 483
  41. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.irreducible_comp_equiv line 499
  42. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.relabelledUnitary_unitary line 511
  43. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.relabelledUnitary_irreducible line 517
  44. def OAI.ThorpNine.Adaptive.Thorp.Specht.relabelledTupleFixed line 522
  45. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.relabelled_tuple_dimension line 556
  46. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.pointStabilizer line 568
  47. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.swap_mem_pointStabilizer line 574
  48. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.point_symmetrizer_zero line 579
  49. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.point_fixed_zero line 611
  50. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.point_unitary_fixed_zero line 623
  51. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.point_relabelled_fixed_zero line 637
  52. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.small_dominating_set line 657
  53. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.powerset_weight_le_exp line 690
  54. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.fixed_size_weight_le line 700
  55. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.neighborhood line 724
  56. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.neighborhood_weight_le line 729
  57. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.root_leaves_weight_le line 751
  58. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.NoIsolated line 774
  59. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.small_dominating_subset line 777
  60. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.noIsolated_weight_le line 803