OAI/Probability/PosteriorReplicas/Model.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PosteriorReplicas.Vec line 15

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:14 (same declaration text).

2. abbrev OAI.PosteriorReplicas.Rows line 16

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:15 (same declaration text).

3. abbrev OAI.PosteriorReplicas.Labels line 17

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:16 (same declaration text).

4. abbrev OAI.PosteriorReplicas.Data line 18

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:17 (same declaration text).

5. abbrev OAI.PosteriorReplicas.Tuple line 19

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:18 (same declaration text).

6. def OAI.PosteriorReplicas.sphereLaw line 21

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:20 (same declaration text).

7. def OAI.PosteriorReplicas.gaussianRows line 25

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:24 (same declaration text).

8. instance OAI.PosteriorReplicas.(instance at line 28) line 28
9. def OAI.PosteriorReplicas.labels line 32

   Also declared: ComparatorChallenges/PosteriorReplicas.lean:31 (same declaration text).

10. lemma OAI.PosteriorReplicas.measurable_labels line 35

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:34 (same declaration text).

11. def OAI.PosteriorReplicas.messageKernel line 40

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:39 (same declaration text).

12. instance OAI.PosteriorReplicas.(instance at line 46) line 46
13. def OAI.PosteriorReplicas.signalMessageLaw line 51

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:50 (same declaration text).

14. instance OAI.PosteriorReplicas.(instance at line 56) line 56
15. def OAI.PosteriorReplicas.sideLaw line 62

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:61 (same declaration text).

16. instance OAI.PosteriorReplicas.(instance at line 67) line 67
17. def OAI.PosteriorReplicas.messageEntropy line 72

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:71 (same declaration text).

18. def OAI.PosteriorReplicas.conditionalInformation line 75

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:74 (same declaration text).

19. def OAI.PosteriorReplicas.GaussianReplicaBlock line 79

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:78 (same declaration text).

20. inductive OAI.PosteriorReplicas.BaseLaw line 93

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:92 (same declaration text).

21. def OAI.PosteriorReplicas.BaseLaw.measure line 98

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:97 (same declaration text).

22. def OAI.PosteriorReplicas.rowGram line 103

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:102 (same declaration text).

23. def OAI.PosteriorReplicas.liftLabel line 106

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

24. def OAI.PosteriorReplicas.kernelComponent line 109

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

25. def OAI.PosteriorReplicas.baseFiber line 112

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

26. def OAI.PosteriorReplicas.baseDensity line 122

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:121 (same declaration text).

27. def OAI.PosteriorReplicas.tiltMass line 135

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:134 (same declaration text).

28. def OAI.PosteriorReplicas.projectedDensity line 139

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:138 (same declaration text).

29. def OAI.PosteriorReplicas.tiltedFiber line 143

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

30. def OAI.PosteriorReplicas.differences line 148

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:147 (same declaration text).

31. def OAI.PosteriorReplicas.differenceSpan line 151

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

32. def OAI.PosteriorReplicas.affineVolume line 154

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

33. def OAI.PosteriorReplicas.constrainedRows line 157

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:156 (same declaration text).

34. def OAI.PosteriorReplicas.equalLabelLeft line 161

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:160 (same declaration text).

35. def OAI.PosteriorReplicas.equalLabelRight line 167

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:166 (same declaration text).

36. def OAI.PosteriorReplicas.EqualLabelMeasureIdentity line 174

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:173 (same declaration text).

37. def OAI.PosteriorReplicas.DistanceReplicaBlock line 182

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:181 (same declaration text).

38. def OAI.PosteriorReplicas.SyntheticReplicaBlock line 193

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:192 (same declaration text).

39. def OAI.PosteriorReplicas.IncidenceReplicaBlock line 205

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:204 (same declaration text).

40. def OAI.PosteriorReplicas.labelNorm line 216

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:215 (same declaration text).

41. def OAI.PosteriorReplicas.ballDensityVersion line 218

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:217 (same declaration text).

42. def OAI.PosteriorReplicas.gaussianDensityVersion line 224

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:223 (same declaration text).

43. def OAI.PosteriorReplicas.EqualLabelVersions line 231

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:230 (same declaration text).

44. def OAI.PosteriorReplicas.haarRows line 256

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:255 (same declaration text).

45. def OAI.PosteriorReplicas.cmi line 259

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:258 (same declaration text).

46. def OAI.PosteriorReplicas.finiteEntropy line 264

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:263 (same declaration text).

47. def OAI.PosteriorReplicas.stateMessageKernel line 267

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:266 (same declaration text).

48. instance OAI.PosteriorReplicas.(instance at line 271) line 271
49. def OAI.PosteriorReplicas.stateMessageLaw line 276

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:275 (same declaration text).

50. instance OAI.PosteriorReplicas.(instance at line 281) line 281
51. def OAI.PosteriorReplicas.stateHaarSideLaw line 287

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:286 (same declaration text).

52. instance OAI.PosteriorReplicas.(instance at line 293) line 293
53. def OAI.PosteriorReplicas.terminalConditionalEntropy line 299

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:298 (same declaration text).

54. def OAI.PosteriorReplicas.HaarReplicaBlock line 303

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:302 (same declaration text).

55. abbrev OAI.PosteriorRegression.Vector line 328

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:327 (same declaration text).

56. abbrev OAI.PosteriorRegression.UnitSphere line 329

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:328 (same declaration text).

57. abbrev OAI.PosteriorRegression.State line 330

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:329 (same declaration text).

58. abbrev OAI.PosteriorRegression.Samples line 331

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:330 (same declaration text).

59. def OAI.PosteriorRegression.uniformSphere line 333

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:332 (same declaration text).

60. def OAI.PosteriorRegression.sampleLaw line 337

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:336 (same declaration text).

61. def OAI.PosteriorRegression.observationReference line 340

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:339 (same declaration text).

62. abbrev OAI.PosteriorRegression.Learner.RunStatus line 345

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:344 (same declaration text).

63. def OAI.PosteriorRegression.Learner.angularError line 347

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:346 (same declaration text).

64. abbrev OAI.PosteriorRegression.CompletedObservation line 360

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:359 (same declaration text).

65. abbrev OAI.PosteriorRegression.Destination line 361

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:360 (same declaration text).

66. structure OAI.PosteriorRegression.CompletedKernelLearner line 363

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:362 (same declaration text).

67. def OAI.PosteriorRegression.CompletedKernelLearner.destStatus line 376

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:375 (same declaration text).

68. def OAI.PosteriorRegression.CompletedKernelLearner.finishState line 379

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:378 (same declaration text).

69. def OAI.PosteriorRegression.CompletedKernelLearner.stepMeasure line 383

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:382 (same declaration text).

70. def OAI.PosteriorRegression.CompletedKernelLearner.runMeasure line 388

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:387 (same declaration text).

71. def OAI.PosteriorRegression.CompletedKernelLearner.terminalLaw line 394

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:393 (same declaration text).

72. def OAI.PosteriorRegression.CompletedKernelLearner.estimateLaw line 398

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:397 (same declaration text).

73. structure OAI.PosteriorRegression.JointKernelExperiment line 404

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:403 (same declaration text).

74. def OAI.PosteriorRegression.JointKernelExperiment.law line 416

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:415 (same declaration text).

75. def OAI.PosteriorRegression.JointKernelExperiment.uniformSuccess line 420

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:419 (same declaration text).

76. def OAI.PosteriorRegression.KernelSubquadraticMemory line 426

    Also declared: ComparatorChallenges/PosteriorReplicas.lean:425 (same declaration text).