OAI/Probability/ThorpRouting/Contact/ModifiedStageEquiv.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Contact.Thorp.modifiedStageEquiv line 11
  2. lemma OAI.ThorpNine.Contact.Thorp.modifiedStageEquiv_apply line 17
  3. lemma OAI.ThorpNine.Contact.Thorp.palindrome_stage line 26
  4. def OAI.ThorpNine.Contact.Thorp.localModifiedPerm line 37
  5. lemma OAI.ThorpNine.Contact.Thorp.modified_stage line 41
  6. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.sampleOperator_sandwich line 63
  7. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.localModified_average line 70
  8. lemma OAI.ThorpNine.Contact.Thorp.sampleOperator_palindrome_stage line 86
  9. lemma OAI.ThorpNine.Contact.Thorp.sampleOperator_modified_stage line 102
  10. def OAI.ThorpNine.Contact.Thorp.CommutingBlocks.retain line 127
  11. lemma OAI.ThorpNine.Contact.Thorp.CommutingBlocks.retain_commute line 131
  12. lemma OAI.ThorpNine.Contact.Thorp.CommutingBlocks.blocks_retain line 137
  13. def OAI.ThorpNine.Contact.Thorp.ParallelBlocks.centralProjection line 161
  14. lemma OAI.ThorpNine.Contact.Thorp.ParallelBlocks.centralProjection_commute line 165
  15. lemma OAI.ThorpNine.Contact.Thorp.ParallelBlocks.local_central_commute line 171
  16. lemma OAI.ThorpNine.Contact.Thorp.modified_central_average line 188
  17. lemma OAI.ThorpNine.Contact.Thorp.central_local_gap line 201
  18. lemma OAI.ThorpNine.Contact.Thorp.central_blocks_exception_bound line 208
  19. theorem OAI.ThorpNine.Contact.Thorp.palindrome_exception_bound line 228
  20. def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.actionKernel line 251
  21. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.actionKernel_apply line 255
  22. def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.randomOperator line 274
  23. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.coefficient_random line 278
  24. def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.fixedSpace line 296
  25. theorem OAI.ThorpNine.Contact.Thorp.UnitaryFinite.operator_amplification line 303
  26. def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.tupleAction line 336
  27. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.tupleAction_apply line 346
  28. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.tupleAction_transitive line 350
  29. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.tupleAction_fixed_iff line 355
  30. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.tupleAction_kernel line 366
  31. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.irreducible_of_equiv line 378
  32. lemma OAI.ThorpNine.Contact.Thorp.Specht.unitaryRepresentation_coe line 395
  33. def OAI.ThorpNine.Contact.Thorp.Specht.unitaryEquiv line 403
  34. lemma OAI.ThorpNine.Contact.Thorp.Specht.unitaryRepresentation_irreducible line 413
  35. lemma OAI.ThorpNine.Contact.Thorp.Specht.unitaryRepresentation_unitary line 418
  36. def OAI.ThorpNine.Contact.Thorp.Specht.tupleFixedEquiv line 427
  37. theorem OAI.ThorpNine.Contact.Thorp.Specht.tupleFixed_dimension line 445
  38. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.sampleOperator_inv_apply line 462
  39. theorem OAI.ThorpNine.Contact.Thorp.UnitaryFinite.sampleOperator_amplification line 467
  40. def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.subrepresentationEquiv line 483
  41. lemma OAI.ThorpNine.Contact.Thorp.UnitaryFinite.irreducible_comp_equiv line 499
  42. lemma OAI.ThorpNine.Contact.Thorp.Specht.relabelledUnitary_unitary line 511
  43. lemma OAI.ThorpNine.Contact.Thorp.Specht.relabelledUnitary_irreducible line 517
  44. def OAI.ThorpNine.Contact.Thorp.Specht.relabelledTupleFixed line 522
  45. lemma OAI.ThorpNine.Contact.Thorp.Specht.relabelled_tuple_dimension line 556
  46. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.small_dominating_set line 568
  47. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.powerset_weight_le_exp line 601
  48. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.fixed_size_weight_le line 611
  49. def OAI.ThorpNine.Contact.Thorp.SparseContact.neighborhood line 635
  50. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.neighborhood_weight_le line 640
  51. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.root_leaves_weight_le line 662
  52. def OAI.ThorpNine.Contact.Thorp.SparseContact.NoIsolated line 685
  53. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.small_dominating_subset line 688
  54. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.noIsolated_weight_le line 714
  55. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.noIsolated_probability_le line 793
  56. def OAI.ThorpNine.Contact.Thorp.SparseContact.typedSet line 817
  57. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.mem_typedSet line 822
  58. def OAI.ThorpNine.Contact.Thorp.SparseContact.fiber line 827
  59. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.mem_fiber line 832
  60. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.typedSet_fiber line 837
  61. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.typedSet_prod line 843
  62. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.typedSet_card line 853
  63. lemma OAI.ThorpNine.Contact.Thorp.SparseContact.subset_typedSet line 862