OAI/Probability/ThorpRouting/Tail/Model.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

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

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

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

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

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

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

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

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

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

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

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

8. def OAI.ThorpNine.Tail.Thorp.finiteMean line 45

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

9. def OAI.ThorpNine.Tail.Thorp.SwitchIndex line 48

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

10. instance OAI.ThorpNine.Tail.Thorp.(instance at line 52) line 52
11. instance OAI.ThorpNine.Tail.Thorp.(instance at line 57) line 57
12. def OAI.ThorpNine.Tail.Thorp.decodeButterfly line 62

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

13. def OAI.ThorpNine.Tail.Thorp.PairRouting.tupleProbability line 74

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

14. abbrev OAI.ThorpNine.Tail.Thorp.Specht.Cell line 84

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

15. def OAI.ThorpNine.Tail.Thorp.Specht.row line 86

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

16. def OAI.ThorpNine.Tail.Thorp.Specht.col line 88

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

17. lemma OAI.ThorpNine.Tail.Thorp.Specht.row_lt_colLen line 90

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

18. def OAI.ThorpNine.Tail.Thorp.Specht.rowIndex line 93

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

19. abbrev OAI.ThorpNine.Tail.Thorp.Specht.Tabloid line 96

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

20. instance OAI.ThorpNine.Tail.Thorp.Specht.(instance at line 99) line 99
21. def OAI.ThorpNine.Tail.Thorp.Specht.baseTabloid line 101

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

22. def OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct line 103

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

23. lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct_apply line 118

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

24. lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct_one line 121

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

25. lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct_mul line 125

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

26. def OAI.ThorpNine.Tail.Thorp.Specht.tabloidRep line 130

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

27. def OAI.ThorpNine.Tail.Thorp.Specht.delta line 142

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

28. def OAI.ThorpNine.Tail.Thorp.Specht.colGroup line 145

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

29. def OAI.ThorpNine.Tail.Thorp.Specht.permSign line 151

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

30. def OAI.ThorpNine.Tail.Thorp.Specht.alternator line 158

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

31. def OAI.ThorpNine.Tail.Thorp.Specht.polytabloid line 165

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

32. def OAI.ThorpNine.Tail.Thorp.Specht.space line 168

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

33. lemma OAI.ThorpNine.Tail.Thorp.Specht.orbit_mem_space line 171

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

34. lemma OAI.ThorpNine.Tail.Thorp.Specht.action_mem_space line 174

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

35. def OAI.ThorpNine.Tail.Thorp.Specht.subrepresentation line 186

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

36. def OAI.ThorpNine.Tail.Thorp.Specht.representation line 189

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

37. abbrev OAI.ThorpNine.Tail.Thorp.PermutationHilbert.H line 200

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

38. def OAI.ThorpNine.Tail.Thorp.Specht.hilbertEquiv line 207

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

39. def OAI.ThorpNine.Tail.Thorp.Specht.hilbertSpace line 211

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

40. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.continuousRepresentation line 223

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

41. def OAI.ThorpNine.Tail.Thorp.UnitaryFinite.sampleOperator line 234

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

42. def OAI.ThorpNine.Tail.Thorp.Specht.spaceHilbertEquiv line 242

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

43. def OAI.ThorpNine.Tail.Thorp.Specht.unitaryRepresentation line 245

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

44. def OAI.ThorpNine.Tail.Thorp.Specht.relabelledUnitary line 251

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

45. def OAI.ThorpNine.Tail.Thorp.SparseContact.sweepOperator line 260

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

46. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.coordinateRelabel line 271

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

47. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweep line 277

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

48. abbrev OAI.ThorpNine.Tail.Thorp.StrongSmoothing.Tuples line 282

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

49. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.sweepKernel line 284

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

50. def OAI.ThorpNine.Tail.Thorp.StrongSmoothing.reflectedKernel line 288

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

51. def OAI.ThorpNine.Tail.Thorp.StrongTail.tailDiagram line 301

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

52. def OAI.ThorpNine.Tail.Thorp.StrongTail.DensityAt line 307

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

53. def OAI.ThorpNine.Tail.Thorp.StrongTail.MainStatement line 324

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