OAI/Probability/ThorpRouting/Smoothing/Model.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

14. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.coordinateRelabel line 83

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

15. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweep line 89

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

16. abbrev OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.Tuples line 94

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

17. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweepKernel line 96

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

18. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflectedKernel line 100

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

19. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.regularAbsoluteEvenTrace line 105

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

20. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.MainStatement line 108

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