OAI/Probability/ThorpRouting/Dense/Model.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

13. def OAI.ThorpNine.Dense.Thorp.orbitSet line 69

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

14. abbrev OAI.ThorpNine.Dense.Thorp.RoutingNetwork.SelectedCycle line 80

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

15. instance OAI.ThorpNine.Dense.Thorp.RoutingNetwork.(instance at line 83) line 83
16. def OAI.ThorpNine.Dense.Thorp.pairLayer line 95

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

17. def OAI.ThorpNine.Dense.Thorp.coinStepEquiv line 109

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

18. def OAI.ThorpNine.Dense.Thorp.headTailEquiv line 123

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

19. def OAI.ThorpNine.Dense.Thorp.CycleColoring.alternatingPerm line 133

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

20. def OAI.ThorpNine.Dense.Thorp.PairRouting.required line 146

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

21. def OAI.ThorpNine.Dense.Thorp.PairRouting.Compatible line 148

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

22. def OAI.ThorpNine.Dense.Thorp.PairRouting.colors line 151

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

23. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.required_colors line 155

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

24. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.colors_compatible line 161

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

25. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.Compatible.tail_injective line 166

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

26. def OAI.ThorpNine.Dense.Thorp.PairRouting.childEmbedding line 177

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

27. def OAI.ThorpNine.Dense.Thorp.PairRouting.labelSet line 180

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

28. def OAI.ThorpNine.Dense.Thorp.PairRouting.alternatingProjection line 182

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

29. def OAI.ThorpNine.Dense.Thorp.PairRouting.alternatingCycles line 184

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

30. def OAI.ThorpNine.Dense.Thorp.PairRouting.switchedEmbedding line 188

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

31. abbrev OAI.ThorpNine.Dense.Thorp.BenesCoins line 197

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

32. def OAI.ThorpNine.Dense.Thorp.palindromePerm line 199

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

33. def OAI.ThorpNine.Dense.Thorp.sandwichShuffle line 202

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

34. def OAI.ThorpNine.Dense.Thorp.benesStepEquiv line 209

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

35. def OAI.ThorpNine.Dense.Thorp.palindromeCost line 213

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

36. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.AdmissibleCycleLaw line 231

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

37. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.h line 235

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

38. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.AdmissibleAllocation line 239

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

39. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.H line 243

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

40. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.entropyCorrection line 247

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

41. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.densityExponent line 250

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

42. def OAI.ThorpNine.Dense.Thorp.DenseTruncation.MainStatement line 255

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