OAI/Probability/ThorpRouting/Adaptive/Model.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

44. def OAI.ThorpNine.Adaptive.Thorp.Casimir.levelScale line 258

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

45. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.positiveSquare line 267

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

46. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.F line 271

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

47. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.fourthTrace line 275

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

48. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.MainStatement line 279

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