OAI/Probability/ThorpRouting/Casimir/Model.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

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

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

2. def OAI.ThorpNine.Casimir.Thorp.Coins line 13

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

3. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 17) line 17
4. def OAI.ThorpNine.Casimir.Thorp.switchFun line 20

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

5. theorem OAI.ThorpNine.Casimir.Thorp.switchFun_involutive line 23

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

6. def OAI.ThorpNine.Casimir.Thorp.pairSwitch line 32

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

7. def OAI.ThorpNine.Casimir.Thorp.rotate line 38

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

8. def OAI.ThorpNine.Casimir.Thorp.step line 44

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

9. def OAI.ThorpNine.Casimir.Thorp.run line 48

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

10. def OAI.ThorpNine.Casimir.Thorp.law line 52

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

11. def OAI.ThorpNine.Casimir.Thorp.Butterfly line 56

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

12. def OAI.ThorpNine.Casimir.Thorp.childLift line 60

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

13. def OAI.ThorpNine.Casimir.Thorp.butterflyPerm line 66

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

14. def OAI.ThorpNine.Casimir.Thorp.finiteMean line 70

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

15. def OAI.ThorpNine.Casimir.Thorp.SwitchIndex line 73

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

16. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 77) line 77
17. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 82) line 82
18. def OAI.ThorpNine.Casimir.Thorp.decodeButterfly line 87

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

19. def OAI.ThorpNine.Casimir.Thorp.PairRouting.tupleProbability line 99

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

20. abbrev OAI.ThorpNine.Casimir.Thorp.BenesCoins line 110

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

21. def OAI.ThorpNine.Casimir.Thorp.palindromePerm line 112

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

22. def OAI.ThorpNine.Casimir.Thorp.palindromeRowMoment line 115

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

23. abbrev OAI.ThorpNine.Casimir.Thorp.Specht.Cell line 125

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

24. def OAI.ThorpNine.Casimir.Thorp.Specht.row line 127

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

25. def OAI.ThorpNine.Casimir.Thorp.Specht.col line 129

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

26. lemma OAI.ThorpNine.Casimir.Thorp.Specht.row_lt_colLen line 131

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

27. def OAI.ThorpNine.Casimir.Thorp.Specht.rowIndex line 134

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

28. abbrev OAI.ThorpNine.Casimir.Thorp.Specht.Tabloid line 137

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

29. instance OAI.ThorpNine.Casimir.Thorp.Specht.(instance at line 140) line 140
30. def OAI.ThorpNine.Casimir.Thorp.Specht.baseTabloid line 142

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

31. def OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct line 144

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

32. lemma OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct_apply line 159

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

33. lemma OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct_one line 162

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

34. lemma OAI.ThorpNine.Casimir.Thorp.Specht.tabloidAct_mul line 166

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

35. def OAI.ThorpNine.Casimir.Thorp.Specht.tabloidRep line 171

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

36. def OAI.ThorpNine.Casimir.Thorp.Specht.delta line 183

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

37. def OAI.ThorpNine.Casimir.Thorp.Specht.colGroup line 186

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

38. def OAI.ThorpNine.Casimir.Thorp.Specht.permSign line 192

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

39. def OAI.ThorpNine.Casimir.Thorp.Specht.alternator line 199

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

40. def OAI.ThorpNine.Casimir.Thorp.Specht.polytabloid line 206

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

41. def OAI.ThorpNine.Casimir.Thorp.Specht.space line 209

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

42. lemma OAI.ThorpNine.Casimir.Thorp.Specht.orbit_mem_space line 212

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

43. lemma OAI.ThorpNine.Casimir.Thorp.Specht.action_mem_space line 215

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

44. def OAI.ThorpNine.Casimir.Thorp.Specht.subrepresentation line 227

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

45. def OAI.ThorpNine.Casimir.Thorp.Specht.representation line 230

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

46. abbrev OAI.ThorpNine.Casimir.Thorp.PermutationHilbert.H line 241

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

47. def OAI.ThorpNine.Casimir.Thorp.Specht.hilbertEquiv line 248

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

48. def OAI.ThorpNine.Casimir.Thorp.Specht.hilbertSpace line 252

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

49. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.continuousRepresentation line 264

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

50. def OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.sampleOperator line 275

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

51. def OAI.ThorpNine.Casimir.Thorp.Specht.spaceHilbertEquiv line 283

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

52. def OAI.ThorpNine.Casimir.Thorp.Specht.unitaryRepresentation line 286

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

53. def OAI.ThorpNine.Casimir.Thorp.Specht.relabelledUnitary line 292

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

54. def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.levelScale line 302

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

55. def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.K line 305

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

56. def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.traceMoment line 310

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

57. def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.fromDistance line 314

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

58. def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.MainStatement line 318

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