OAI/Probability/ThorpRouting/Contact/Model.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ThorpNine.Contact.Thorp.Card line 11

   Also declared: ComparatorChallenges/ThorpRouting.lean:911 (same declaration text).

2. def OAI.ThorpNine.Contact.Thorp.switchFun line 13

   Also declared: ComparatorChallenges/ThorpRouting.lean:913 (same declaration text).

3. theorem OAI.ThorpNine.Contact.Thorp.switchFun_involutive line 16

   Also declared: ComparatorChallenges/ThorpRouting.lean:916 (same declaration text).

4. def OAI.ThorpNine.Contact.Thorp.pairSwitch line 25

   Also declared: ComparatorChallenges/ThorpRouting.lean:925 (same declaration text).

5. def OAI.ThorpNine.Contact.Thorp.Butterfly line 31

   Also declared: ComparatorChallenges/ThorpRouting.lean:931 (same declaration text).

6. def OAI.ThorpNine.Contact.Thorp.childLift line 35

   Also declared: ComparatorChallenges/ThorpRouting.lean:935 (same declaration text).

7. def OAI.ThorpNine.Contact.Thorp.butterflyPerm line 41

   Also declared: ComparatorChallenges/ThorpRouting.lean:941 (same declaration text).

8. def OAI.ThorpNine.Contact.Thorp.SwitchIndex line 45

   Also declared: ComparatorChallenges/ThorpRouting.lean:945 (same declaration text).

9. instance OAI.ThorpNine.Contact.Thorp.(instance at line 49) line 49
10. instance OAI.ThorpNine.Contact.Thorp.(instance at line 54) line 54
11. def OAI.ThorpNine.Contact.Thorp.decodeButterfly line 59

    Also declared: ComparatorChallenges/ThorpRouting.lean:959 (same declaration text).

12. abbrev OAI.ThorpNine.Contact.Thorp.Specht.Cell line 69

    Also declared: ComparatorChallenges/ThorpRouting.lean:969 (same declaration text).

13. def OAI.ThorpNine.Contact.Thorp.Specht.row line 71

    Also declared: ComparatorChallenges/ThorpRouting.lean:971 (same declaration text).

14. def OAI.ThorpNine.Contact.Thorp.Specht.col line 73

    Also declared: ComparatorChallenges/ThorpRouting.lean:973 (same declaration text).

15. lemma OAI.ThorpNine.Contact.Thorp.Specht.row_lt_colLen line 75

    Also declared: ComparatorChallenges/ThorpRouting.lean:975 (same declaration text).

16. def OAI.ThorpNine.Contact.Thorp.Specht.rowIndex line 78

    Also declared: ComparatorChallenges/ThorpRouting.lean:978 (same declaration text).

17. abbrev OAI.ThorpNine.Contact.Thorp.Specht.Tabloid line 81

    Also declared: ComparatorChallenges/ThorpRouting.lean:981 (same declaration text).

18. instance OAI.ThorpNine.Contact.Thorp.Specht.(instance at line 84) line 84
19. def OAI.ThorpNine.Contact.Thorp.Specht.baseTabloid line 86

    Also declared: ComparatorChallenges/ThorpRouting.lean:986 (same declaration text).

20. def OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct line 88

    Also declared: ComparatorChallenges/ThorpRouting.lean:988 (same declaration text).

21. lemma OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct_apply line 103

    Also declared: ComparatorChallenges/ThorpRouting.lean:1003 (same declaration text).

22. lemma OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct_one line 106

    Also declared: ComparatorChallenges/ThorpRouting.lean:1006 (same declaration text).

23. lemma OAI.ThorpNine.Contact.Thorp.Specht.tabloidAct_mul line 110

    Also declared: ComparatorChallenges/ThorpRouting.lean:1010 (same declaration text).

24. def OAI.ThorpNine.Contact.Thorp.Specht.tabloidRep line 115

    Also declared: ComparatorChallenges/ThorpRouting.lean:1015 (same declaration text).

25. def OAI.ThorpNine.Contact.Thorp.Specht.delta line 127

    Also declared: ComparatorChallenges/ThorpRouting.lean:1027 (same declaration text).

26. def OAI.ThorpNine.Contact.Thorp.Specht.colGroup line 130

    Also declared: ComparatorChallenges/ThorpRouting.lean:1030 (same declaration text).

27. def OAI.ThorpNine.Contact.Thorp.Specht.permSign line 136

    Also declared: ComparatorChallenges/ThorpRouting.lean:1036 (same declaration text).

28. def OAI.ThorpNine.Contact.Thorp.Specht.alternator line 143

    Also declared: ComparatorChallenges/ThorpRouting.lean:1043 (same declaration text).

29. def OAI.ThorpNine.Contact.Thorp.Specht.polytabloid line 150

    Also declared: ComparatorChallenges/ThorpRouting.lean:1050 (same declaration text).

30. def OAI.ThorpNine.Contact.Thorp.Specht.space line 153

    Also declared: ComparatorChallenges/ThorpRouting.lean:1053 (same declaration text).

31. lemma OAI.ThorpNine.Contact.Thorp.Specht.orbit_mem_space line 156

    Also declared: ComparatorChallenges/ThorpRouting.lean:1056 (same declaration text).

32. lemma OAI.ThorpNine.Contact.Thorp.Specht.action_mem_space line 159

    Also declared: ComparatorChallenges/ThorpRouting.lean:1059 (same declaration text).

33. def OAI.ThorpNine.Contact.Thorp.Specht.subrepresentation line 171

    Also declared: ComparatorChallenges/ThorpRouting.lean:1071 (same declaration text).

34. def OAI.ThorpNine.Contact.Thorp.Specht.representation line 174

    Also declared: ComparatorChallenges/ThorpRouting.lean:1074 (same declaration text).

35. abbrev OAI.ThorpNine.Contact.Thorp.PermutationHilbert.H line 185

    Also declared: ComparatorChallenges/ThorpRouting.lean:1085 (same declaration text).

36. def OAI.ThorpNine.Contact.Thorp.Specht.hilbertEquiv line 192

    Also declared: ComparatorChallenges/ThorpRouting.lean:1092 (same declaration text).

37. def OAI.ThorpNine.Contact.Thorp.Specht.hilbertSpace line 196

    Also declared: ComparatorChallenges/ThorpRouting.lean:1096 (same declaration text).

38. def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.continuousRepresentation line 208

    Also declared: ComparatorChallenges/ThorpRouting.lean:1108 (same declaration text).

39. def OAI.ThorpNine.Contact.Thorp.UnitaryFinite.sampleOperator line 219

    Also declared: ComparatorChallenges/ThorpRouting.lean:1119 (same declaration text).

40. def OAI.ThorpNine.Contact.Thorp.Specht.spaceHilbertEquiv line 227

    Also declared: ComparatorChallenges/ThorpRouting.lean:1127 (same declaration text).

41. def OAI.ThorpNine.Contact.Thorp.Specht.unitaryRepresentation line 230

    Also declared: ComparatorChallenges/ThorpRouting.lean:1130 (same declaration text).

42. def OAI.ThorpNine.Contact.Thorp.Specht.relabelledUnitary line 236

    Also declared: ComparatorChallenges/ThorpRouting.lean:1136 (same declaration text).

43. def OAI.ThorpNine.Contact.Thorp.SparseContact.sweepOperator line 245

    Also declared: ComparatorChallenges/ThorpRouting.lean:1145 (same declaration text).

44. def OAI.ThorpNine.Contact.Thorp.SparseContact.MainStatement line 252

    Also declared: ComparatorChallenges/ThorpRouting.lean:1152 (same declaration text).