OAI/Probability/Localization/Model.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RepeatedLocalization.Coordinate line 10

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:10 (same declaration text), ComparatorChallenges/GaussianInformation.lean:11 (same declaration text).

2. abbrev OAI.RepeatedLocalization.GaussianBlock line 11

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:11 (same declaration text), ComparatorChallenges/GaussianInformation.lean:12 (same declaration text).

3. abbrev OAI.RepeatedLocalization.Label line 12

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:12 (same declaration text), ComparatorChallenges/GaussianInformation.lean:13 (same declaration text).

4. abbrev OAI.RepeatedLocalization.History line 13

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:13 (same declaration text), ComparatorChallenges/GaussianInformation.lean:14 (same declaration text).

5. abbrev OAI.RepeatedLocalization.Cell line 14

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:14 (same declaration text), ComparatorChallenges/GaussianInformation.lean:15 (same declaration text).

6. instance OAI.RepeatedLocalization.cellMeasurableSpace line 16

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:16 (same declaration text), ComparatorChallenges/GaussianInformation.lean:17 (same declaration text).

7. def OAI.RepeatedLocalization.initialCube line 18

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:18 (same declaration text), ComparatorChallenges/GaussianInformation.lean:19 (same declaration text).

8. def OAI.RepeatedLocalization.cubePrior line 21

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:21 (same declaration text), ComparatorChallenges/GaussianInformation.lean:22 (same declaration text).

9. def OAI.RepeatedLocalization.chart line 24

   Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:24 (same declaration text), ComparatorChallenges/GaussianInformation.lean:25 (same declaration text).

10. def OAI.RepeatedLocalization.cellSet line 27

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:27 (same declaration text), ComparatorChallenges/GaussianInformation.lean:28 (same declaration text).

11. def OAI.RepeatedLocalization.rootCell line 31

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:31 (same declaration text), ComparatorChallenges/GaussianInformation.lean:32 (same declaration text).

12. def OAI.RepeatedLocalization.gaussianBlockLaw line 33

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:33 (same declaration text), ComparatorChallenges/GaussianInformation.lean:34 (same declaration text).

13. def OAI.RepeatedLocalization.exactLabel line 36

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:36 (same declaration text), ComparatorChallenges/GaussianInformation.lean:37 (same declaration text).

14. structure OAI.RepeatedLocalization.BlockRule line 39

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:39 (same declaration text), ComparatorChallenges/GaussianInformation.lean:40 (same declaration text).

15. abbrev OAI.RepeatedLocalization.Rules line 45

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:45 (same declaration text), ComparatorChallenges/GaussianInformation.lean:46 (same declaration text).

16. def OAI.RepeatedLocalization.past line 47

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:47 (same declaration text), ComparatorChallenges/GaussianInformation.lean:48 (same declaration text).

17. def OAI.RepeatedLocalization.through line 50

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:50 (same declaration text), ComparatorChallenges/GaussianInformation.lean:51 (same declaration text).

18. def OAI.RepeatedLocalization.blockProbability line 53

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:53 (same declaration text), ComparatorChallenges/GaussianInformation.lean:54 (same declaration text).

19. def OAI.RepeatedLocalization.historyLikelihood line 57

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:57 (same declaration text), ComparatorChallenges/GaussianInformation.lean:58 (same declaration text).

20. def OAI.RepeatedLocalization.experimentLaw line 61

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:61 (same declaration text), ComparatorChallenges/GaussianInformation.lean:62 (same declaration text).

21. abbrev OAI.RepeatedLocalization.Disclosure line 67

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:67 (same declaration text), ComparatorChallenges/GaussianInformation.lean:68 (same declaration text).

22. def OAI.RepeatedLocalization.ValidDisclosure line 69

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:69 (same declaration text), ComparatorChallenges/GaussianInformation.lean:70 (same declaration text).

23. def OAI.RepeatedLocalization.transcriptMap line 77

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:77 (same declaration text), ComparatorChallenges/GaussianInformation.lean:78 (same declaration text).

24. def OAI.RepeatedLocalization.augmentedLaw line 81

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:81 (same declaration text), ComparatorChallenges/GaussianInformation.lean:82 (same declaration text).

25. def OAI.RepeatedLocalization.mutualInformation line 84

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:84 (same declaration text), ComparatorChallenges/GaussianInformation.lean:85 (same declaration text).

26. def OAI.RepeatedLocalization.finalLevel line 88

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:88 (same declaration text), ComparatorChallenges/GaussianInformation.lean:89 (same declaration text).

27. def OAI.RepeatedLocalization.MainStatement line 95

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:95 (same declaration text), ComparatorChallenges/GaussianInformation.lean:96 (same declaration text).

28. def OAI.RepeatedLocalization.FiniteEntropy.uniformCell line 105

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:105 (same declaration text).

29. def OAI.RepeatedLocalization.FiniteEntropy.Descendant line 108

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:108 (same declaration text).

30. def OAI.RepeatedLocalization.FiniteEntropy.threshold line 111

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:111 (same declaration text).

31. def OAI.RepeatedLocalization.FiniteEntropy.Heavy line 113

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:113 (same declaration text).

32. def OAI.RepeatedLocalization.FiniteEntropy.FirstHeavy line 116

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:116 (same declaration text).

33. def OAI.RepeatedLocalization.FiniteEntropy.residual line 119

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:119 (same declaration text).

34. abbrev OAI.RepeatedLocalization.FiniteEntropy.Letter line 122

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:122 (same declaration text).

35. abbrev OAI.RepeatedLocalization.FiniteEntropy.Log line 123

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:123 (same declaration text).

36. instance OAI.RepeatedLocalization.FiniteEntropy.logMeasurableSpace line 124

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:124 (same declaration text).

37. def OAI.RepeatedLocalization.FiniteEntropy.branch line 126

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:126 (same declaration text).

38. def OAI.RepeatedLocalization.FiniteEntropy.attemptLetter line 132

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:132 (same declaration text).

39. structure OAI.RepeatedLocalization.FiniteEntropy.State line 137

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:137 (same declaration text).

40. def OAI.RepeatedLocalization.FiniteEntropy.update line 142

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:142 (same declaration text).

41. def OAI.RepeatedLocalization.FiniteEntropy.state line 150

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:150 (same declaration text).

42. def OAI.RepeatedLocalization.FiniteEntropy.run line 153

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:153 (same declaration text).

43. def OAI.RepeatedLocalization.FiniteEntropy.Terminates line 161

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:161 (same declaration text).

44. def OAI.RepeatedLocalization.FiniteEntropy.attempts line 164

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:164 (same declaration text).

45. def OAI.RepeatedLocalization.FiniteEntropy.terminalLog line 168

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:168 (same declaration text).

46. def OAI.RepeatedLocalization.FiniteEntropy.terminalCell line 171

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:171 (same declaration text).

47. def OAI.RepeatedLocalization.FiniteEntropy.terminalLaw line 174

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:174 (same declaration text).

48. def OAI.RepeatedLocalization.FiniteEntropy.depth line 177

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:177 (same declaration text).

49. def OAI.RepeatedLocalization.FiniteEntropy.Regular line 180

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:180 (same declaration text).

50. def OAI.RepeatedLocalization.FiniteEntropy.FiniteEntropyStatement line 184

    Also declared: ComparatorChallenges/GaussianFiniteEntropy.lean:184 (same declaration text).