OAI/Probability/ThorpRouting/SparseSaving/Model.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

44. def OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.MainStatement line 256

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