OAI/Probability/ProjectionMoments/Model.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.NoiselessRegression.Vector line 17

   Also declared: ComparatorChallenges/MemoryPrecision.lean:133 (same declaration text), ComparatorChallenges/NoiselessRegression.lean:18 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:17 (same declaration text).

2. abbrev OAI.NoiselessRegression.UnitSphere line 19

   Also declared: ComparatorChallenges/MemoryPrecision.lean:134 (same declaration text), ComparatorChallenges/NoiselessRegression.lean:19 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:19 (same declaration text).

3. abbrev OAI.NoiselessRegression.State line 21

   Also declared: ComparatorChallenges/NoiselessRegression.lean:20 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:21 (same declaration text).

4. abbrev OAI.NoiselessRegression.Samples line 23

   Also declared: ComparatorChallenges/NoiselessRegression.lean:21 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:23 (same declaration text).

5. def OAI.NoiselessRegression.uniformSphere line 25

   Also declared: ComparatorChallenges/NoiselessRegression.lean:23 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:25 (same declaration text).

6. def OAI.NoiselessRegression.sampleLaw line 29

   Also declared: ComparatorChallenges/NoiselessRegression.lean:27 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:29 (same declaration text).

7. def OAI.NoiselessRegression.observationReference line 32

   Also declared: ComparatorChallenges/NoiselessRegression.lean:30 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:32 (same declaration text).

8. structure OAI.NoiselessRegression.Learner line 35

   Also declared: ComparatorChallenges/NoiselessRegression.lean:33 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:35 (same declaration text).

9. abbrev OAI.NoiselessRegression.Learner.RunStatus line 42

   Also declared: ComparatorChallenges/NoiselessRegression.lean:40 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:42 (same declaration text).

10. def OAI.NoiselessRegression.Learner.start line 44

    Also declared: ComparatorChallenges/NoiselessRegression.lean:42 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:44 (same declaration text).

11. def OAI.NoiselessRegression.Learner.run line 49

    Also declared: ComparatorChallenges/NoiselessRegression.lean:47 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:49 (same declaration text).

12. def OAI.NoiselessRegression.Learner.terminal line 62

    Also declared: ComparatorChallenges/NoiselessRegression.lean:60 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:62 (same declaration text).

13. def OAI.NoiselessRegression.Learner.estimate line 68

    Also declared: ComparatorChallenges/NoiselessRegression.lean:66 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:68 (same declaration text).

14. structure OAI.NoiselessRegression.Learner.Admissible line 73

    Also declared: ComparatorChallenges/NoiselessRegression.lean:71 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:73 (same declaration text).

15. def OAI.NoiselessRegression.Learner.angularError line 85

    Also declared: ComparatorChallenges/NoiselessRegression.lean:83 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:85 (same declaration text).

16. def OAI.NoiselessRegression.Learner.uniformSuccess line 88

    Also declared: ComparatorChallenges/NoiselessRegression.lean:91 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:88 (same declaration text).

17. def OAI.NoiselessRegression.sphereLaw line 106

    Also declared: ComparatorChallenges/ProjectionMoments.lean:106 (same declaration text).

18. def OAI.NoiselessRegression.ambientSphereLaw line 117

    Also declared: ComparatorChallenges/ProjectionMoments.lean:117 (same declaration text).

19. def OAI.ProjectionMoments.vectorSmoothing line 134

    Also declared: ComparatorChallenges/ProjectionMoments.lean:324 (same declaration text).

20. abbrev OAI.ProjectionMoments.Label line 142

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

21. def OAI.ProjectionMoments.ballKernel line 144

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

22. def OAI.ProjectionMoments.rowMap line 153

    Also declared: ComparatorChallenges/ProjectionMoments.lean:334 (same declaration text).

23. def OAI.ProjectionMoments.ballAverage line 157

    Also declared: ComparatorChallenges/ProjectionMoments.lean:338 (same declaration text).

24. def OAI.ProjectionMoments.lowerDensity line 161

    Also declared: ComparatorChallenges/ProjectionMoments.lean:342 (same declaration text).

25. def OAI.ProjectionMoments.AllBallMass line 169

    Also declared: ComparatorChallenges/ProjectionMoments.lean:345 (same declaration text).

26. abbrev OAI.ProjectionMoments.Rotation line 179

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

27. instance OAI.ProjectionMoments.rotationMeasurableSpace line 181

    Also declared: ComparatorChallenges/ProjectionMoments.lean:361 (same declaration text).

28. instance OAI.ProjectionMoments.rotationBorelSpace line 183

    Also declared: ComparatorChallenges/ProjectionMoments.lean:363 (same declaration text).

29. instance OAI.ProjectionMoments.rotationCompact line 185

    Also declared: ComparatorChallenges/ProjectionMoments.lean:365 (same declaration text).

30. def OAI.ProjectionMoments.rotationLaw line 197

    Also declared: ComparatorChallenges/ProjectionMoments.lean:377 (same declaration text).

31. def OAI.ProjectionMoments.rotateRows line 204

    Also declared: ComparatorChallenges/ProjectionMoments.lean:384 (same declaration text).

32. def OAI.ProjectionMoments.coordinateMap line 215

    Also declared: ComparatorChallenges/ProjectionMoments.lean:395 (same declaration text).

33. def OAI.ProjectionMoments.coordinateDensity line 226

    Also declared: ComparatorChallenges/ProjectionMoments.lean:398 (same declaration text).

34. def OAI.ProjectionMoments.frameLaw line 236

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:401 (same statement text; different proof or body). Qualify references as OAI.ProjectionMoments.frameLaw@path.

35. def OAI.ProjectionMoments.rieszKernel line 246

    Also declared: ComparatorChallenges/ProjectionMoments.lean:408 (same declaration text).

36. def OAI.ProjectionMoments.rieszPotential line 248

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:410 (same statement text; different proof or body). Qualify references as OAI.ProjectionMoments.rieszPotential@path.

37. def OAI.ProjectionMoments.mixRows line 258

    Also declared: ComparatorChallenges/ProjectionMoments.lean:417 (same declaration text).

38. def OAI.ProjectionMoments.polarRadial line 261

    Also declared: ComparatorChallenges/ProjectionMoments.lean:420 (same declaration text).

39. def OAI.ProjectionMoments.rawPolarRows line 264

    Also declared: ComparatorChallenges/ProjectionMoments.lean:423 (same declaration text).

40. def OAI.ProjectionMoments.polarRows line 267

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:426 (same statement text; different proof or body). Qualify references as OAI.ProjectionMoments.polarRows@path.

41. def OAI.ProjectionMoments.unitBallVolume line 278

    Also declared: ComparatorChallenges/ProjectionMoments.lean:434 (same declaration text).

42. def OAI.ProjectionMoments.unitBallLaw line 280

    Also declared: ComparatorChallenges/ProjectionMoments.lean:436 (same declaration text).

43. def OAI.ProjectionMoments.normalizedDensity line 283

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:439 (same statement text; different proof or body). Qualify references as OAI.ProjectionMoments.normalizedDensity@path.

44. def OAI.ProjectionMoments.sphereWeightedRestriction line 287

    Also declared: ComparatorChallenges/ProjectionMoments.lean:447 (same declaration text).

45. def OAI.ProjectionMoments.capMeasure line 299

    Also declared: ComparatorChallenges/ProjectionMoments.lean:461 (same declaration text).

46. structure OAI.ProjectionMoments.CapDictionary line 303

    Also declared: ComparatorChallenges/ProjectionMoments.lean:465 (same declaration text).

47. def OAI.ProjectionMoments.radialLabel line 325

    Also declared: ComparatorChallenges/ProjectionMoments.lean:491 (same declaration text).

48. def OAI.ProjectionMoments.capKernelValue line 328

    Also declared: ComparatorChallenges/ProjectionMoments.lean:494 (same declaration text).

49. def OAI.ProjectionMoments.capReferenceLabel line 331

    Also declared: ComparatorChallenges/ProjectionMoments.lean:497 (same declaration text).

50. def OAI.ProjectionMoments.capReference line 334

    Also declared: ComparatorChallenges/ProjectionMoments.lean:500 (same declaration text).

51. def OAI.ProjectionMoments.fractionalBlock line 342

    Also declared: ComparatorChallenges/ProjectionMoments.lean:508 (same declaration text).

52. abbrev OAI.NoiselessRegression.Learner.TaggedState line 361

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:127 (different declaration text). Qualify references as OAI.NoiselessRegression.Learner.TaggedState@path.

53. instance OAI.NoiselessRegression.Learner.taggedMeasurableSpace line 363

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:129 (different declaration text). Qualify references as OAI.NoiselessRegression.Learner.taggedMeasurableSpace@path.

54. def OAI.NoiselessRegression.Learner.taggedStart line 365

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:131 (different declaration text). Qualify references as OAI.NoiselessRegression.Learner.taggedStart@path.

55. structure OAI.NoiselessRegression.Learner.MeasurableRules line 374

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:142 (different declaration text). Qualify references as OAI.NoiselessRegression.Learner.MeasurableRules@path.

56. structure OAI.NoiselessRegression.FiniteKernelLearner line 381

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

57. structure OAI.NoiselessRegression.FiniteKernelLearner.CompletedRules line 393

    Also declared: ComparatorChallenges/ProjectionMoments.lean:165 (same declaration text).

58. def OAI.NoiselessRegression.kernelRun line 403

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

59. abbrev OAI.NoiselessRegression.FiniteKernelLearner.Tape line 417

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:191 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.Tape@path.

60. def OAI.NoiselessRegression.FiniteKernelLearner.destination line 419

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:193 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.destination@path.

61. def OAI.NoiselessRegression.FiniteKernelLearner.taggedKernel line 422

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:196 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.taggedKernel@path.

62. def OAI.NoiselessRegression.FiniteKernelLearner.terminalOutput line 428

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:202 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.terminalOutput@path.

63. abbrev OAI.NoiselessRegression.FiniteKernelLearner.Result line 438

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:216 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.Result@path.

64. def OAI.NoiselessRegression.FiniteKernelLearner.terminalTag line 440

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:218 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.terminalTag@path.

65. def OAI.NoiselessRegression.FiniteKernelLearner.terminalJointOutput line 444

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:222 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.terminalJointOutput@path.

66. def OAI.NoiselessRegression.FiniteKernelLearner.jointExperimentLaw line 447

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:225 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.jointExperimentLaw@path.

67. def OAI.NoiselessRegression.FiniteKernelLearner.uniformSuccess line 450

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:228 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.uniformSuccess@path.

68. def OAI.NoiselessRegression.FiniteKernelLearner.uniformFixedSuccess line 455

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:233 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.uniformFixedSuccess@path.

69. def OAI.NoiselessRegression.Learner.uniformFixedSuccess line 473

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:251 (different declaration text). Qualify references as OAI.NoiselessRegression.Learner.uniformFixedSuccess@path.

70. def OAI.NoiselessRegression.FiniteKernelLearner.seededSuccess line 490

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:262 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.seededSuccess@path.

71. def OAI.NoiselessRegression.FiniteKernelLearner.seededFixedSuccess line 494

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:266 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.seededFixedSuccess@path.

72. def OAI.NoiselessRegression.FiniteKernelLearner.FixedQuadraticMemory line 498

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:270 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.FixedQuadraticMemory@path.

73. def OAI.NoiselessRegression.FiniteKernelLearner.conditionalSuccess line 513

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:287 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.conditionalSuccess@path.

74. def OAI.NoiselessRegression.FiniteKernelLearner.seededPointwiseSuccess line 517

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:291 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.seededPointwiseSuccess@path.

75. def OAI.NoiselessRegression.FiniteKernelLearner.JointSuccessMeasurable line 521

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:295 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.JointSuccessMeasurable@path.

76. def OAI.NoiselessRegression.FiniteKernelLearner.SubquadraticMemoryWithPointwise line 526

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:300 (different declaration text). Qualify references as OAI.NoiselessRegression.FiniteKernelLearner.SubquadraticMemoryWithPointwise@path.

77. def OAI.ProjectionMoments.IntegratedFrameMoment line 551

    Also declared: ComparatorChallenges/ProjectionMoments.lean:514 (same declaration text).

78. def OAI.ProjectionMoments.NormalizedUnitBallMoment line 571

    Also declared: ComparatorChallenges/ProjectionMoments.lean:534 (same declaration text).

79. def OAI.ProjectionMoments.AllRadiiSphereMoment line 591

    Also declared: ComparatorChallenges/ProjectionMoments.lean:554 (same declaration text).

80. def OAI.ProjectionMoments.PositiveCapDomination line 613

    Also declared: ComparatorChallenges/ProjectionMoments.lean:576 (same declaration text).

81. def OAI.ProjectionMoments.DeterministicOffsetDensity line 629

    Also declared: ComparatorChallenges/ProjectionMoments.lean:592 (same declaration text).

82. def OAI.ProjectionMoments.AllRadiiBlockBound line 647

    Also declared: ComparatorChallenges/ProjectionMoments.lean:610 (same declaration text).

83. def OAI.ProjectionMoments.HaarStreamingCost line 660

    Also declared: ComparatorChallenges/ProjectionMoments.lean:623 (same declaration text).

84. def OAI.ProjectionMoments.RieszStreamingCost line 670

    Also declared: ComparatorChallenges/ProjectionMoments.lean:633 (same declaration text).

85. def OAI.ProjectionMoments.CapFixedStoppingCost line 680

    Also declared: ComparatorChallenges/ProjectionMoments.lean:643 (same declaration text).

86. def OAI.ProjectionMoments.CapTotalStoppingCost line 691

    Also declared: ComparatorChallenges/ProjectionMoments.lean:654 (same declaration text).

87. def OAI.ProjectionMoments.CapFixedStoppingAsymptotic line 702

    Also declared: ComparatorChallenges/ProjectionMoments.lean:665 (same declaration text).

88. def OAI.ProjectionMoments.CapTotalStoppingAsymptotic line 715

    Also declared: ComparatorChallenges/ProjectionMoments.lean:678 (same declaration text).

89. def OAI.ProjectionMoments.KernelModelBridge line 725

    Also declared: ComparatorChallenges/ProjectionMoments.lean:688 (same declaration text).

90. def OAI.ProjectionMoments.MainStatement line 732

    Distinct definitions of this name: ComparatorChallenges/ProjectionMoments.lean:695 (same statement text; different proof or body). Qualify references as OAI.ProjectionMoments.MainStatement@path.