OAI/Probability/Subsphere/Model.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SubsphereCurrent.Vector line 10

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:10 (same declaration text).

2. abbrev OAI.SubsphereCurrent.UnitSphere line 11

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:11 (same declaration text).

3. abbrev OAI.SubsphereCurrent.State line 12

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:12 (same declaration text).

4. abbrev OAI.SubsphereCurrent.Samples line 13

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:13 (same declaration text).

5. def OAI.SubsphereCurrent.uniformSphere line 15

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

6. def OAI.SubsphereCurrent.sampleLaw line 19

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:19 (same declaration text).

7. def OAI.SubsphereCurrent.observationReference line 22

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:22 (same declaration text).

8. structure OAI.SubsphereCurrent.KernelLearner line 25

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:25 (same declaration text).

9. abbrev OAI.SubsphereCurrent.KernelLearner.RunStatus line 32

   Also declared: ComparatorChallenges/SubsphereCurrent.lean:32 (same declaration text).

10. def OAI.SubsphereCurrent.KernelLearner.tagged line 34

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

11. def OAI.SubsphereCurrent.KernelLearner.run line 37

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:37 (same declaration text).

12. def OAI.SubsphereCurrent.KernelLearner.terminal line 47

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:47 (same declaration text).

13. def OAI.SubsphereCurrent.KernelLearner.estimateLaw line 54

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:54 (same declaration text).

14. def OAI.SubsphereCurrent.KernelLearner.angularError line 58

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:58 (same declaration text).

15. def OAI.SubsphereCurrent.KernelLearner.conditionalSuccess line 61

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

16. def OAI.SubsphereCurrent.KernelLearner.CompletedRules line 65

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:65 (same declaration text).

17. structure OAI.SubsphereCurrent.SeededLearner line 70

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:70 (same declaration text).

18. structure OAI.SubsphereCurrent.SeededLearner.Admissible line 75

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:75 (same declaration text).

19. def OAI.SubsphereCurrent.SeededLearner.success line 86

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:86 (same declaration text).

20. def OAI.SubsphereCurrent.SeededLearner.uniformSuccess line 91

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:91 (same declaration text).

21. def OAI.SubsphereCurrent.ExplicitPrecision line 98

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:98 (same declaration text).

22. abbrev OAI.SubsphereCurrent.Affine.Vector line 117

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

23. abbrev OAI.SubsphereCurrent.Affine.Sphere line 118

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:118 (same declaration text).

24. def OAI.SubsphereCurrent.Affine.sphereLaw line 120

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:120 (same declaration text).

25. structure OAI.SubsphereCurrent.Affine.Test line 125

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:125 (same declaration text).

26. def OAI.SubsphereCurrent.Affine.Test.point line 134

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

27. abbrev OAI.SubsphereCurrent.Weighted.Vector line 145

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:145 (same declaration text).

28. abbrev OAI.SubsphereCurrent.Weighted.Sphere line 146

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:146 (same declaration text).

29. abbrev OAI.SubsphereCurrent.Weighted.Rows line 147

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

30. abbrev OAI.SubsphereCurrent.Weighted.Observation line 148

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:148 (same declaration text).

31. def OAI.SubsphereCurrent.Weighted.onTest line 150

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

32. def OAI.SubsphereCurrent.Weighted.norm line 163

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:163 (same declaration text).

33. def OAI.SubsphereCurrent.Weighted.blockInput line 167

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:167 (same declaration text).

34. def OAI.SubsphereCurrent.Weighted.terminalInput line 173

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

35. def OAI.SubsphereCurrent.Weighted.RadiusWeightedFullEstimate line 185

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:185 (same declaration text).

36. def OAI.SubsphereCurrent.HalfPrecision line 210

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:210 (same declaration text).

37. abbrev OAI.SubsphereCurrent.Fixed.Vector line 229

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:229 (same declaration text).

38. abbrev OAI.SubsphereCurrent.Fixed.Sphere line 230

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

39. def OAI.SubsphereCurrent.Fixed.sphereLaw line 232

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:232 (same declaration text).

40. def OAI.SubsphereCurrent.Fixed.rowsLaw line 237

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:237 (same declaration text).

41. structure OAI.SubsphereCurrent.Fixed.Stream line 241

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:241 (same declaration text).

42. def OAI.SubsphereCurrent.Fixed.Stream.run line 252

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:252 (same declaration text).

43. def OAI.SubsphereCurrent.Fixed.Stream.estimateLaw line 258

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

44. def OAI.SubsphereCurrent.Fixed.Stream.euclideanSuccess line 261

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:261 (same declaration text).

45. def OAI.SubsphereCurrent.Fixed.Stream.angularSuccess line 264

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:264 (same declaration text).

46. def OAI.SubsphereCurrent.Fixed.Stream.BorelRules line 267

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:267 (same declaration text).

47. def OAI.SubsphereCurrent.Fixed.Stream.suffix line 270

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:270 (same declaration text).

48. def OAI.SubsphereCurrent.Fixed.DimensionEstimate line 278

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:278 (same declaration text).

49. def OAI.SubsphereCurrent.Affine.AllAffineFullEstimate line 303

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:303 (same declaration text).

50. def OAI.SubsphereRegression.sphereLaw line 330

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

51. def OAI.SubsphereRegression.ambientSphereLaw line 339

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

52. abbrev OAI.SubsphereCurrent.Mixture.Orthogonal line 349

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:349 (same declaration text).

53. instance OAI.SubsphereCurrent.Mixture.orthogonal_compact line 352

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:352 (same declaration text).

54. def OAI.SubsphereCurrent.Mixture.orthogonalLaw line 361

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

55. def OAI.SubsphereCurrent.Mixture.blockIso line 372

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:372 (same declaration text).

56. def OAI.SubsphereCurrent.Mixture.directionLaw line 386

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:386 (same declaration text).

57. def OAI.SubsphereCurrent.Mixture.directionJointLaw line 390

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:390 (same declaration text).

58. def OAI.SubsphereCurrent.Mixture.latitudeSpace line 395

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

59. def OAI.SubsphereCurrent.Mixture.latitudeLaw line 398

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

60. def OAI.SubsphereCurrent.Mixture.MixtureEstimate line 404

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:404 (same declaration text).

61. def OAI.SubsphereCurrent.CurrentMainScope line 426

    Also declared: ComparatorChallenges/SubsphereCurrent.lean:426 (same declaration text).