OAI/Probability/SphericalField/Model.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SphericalPerceptron.Time line 11

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

2. abbrev OAI.SphericalPerceptron.Spin line 13

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

3. def OAI.SphericalPerceptron.unitSphereLaw line 15

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

4. structure OAI.SphericalPerceptron.Trial line 19

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

5. instance OAI.SphericalPerceptron.(instance at line 26) line 26
6. def OAI.SphericalPerceptron.timeLaw line 28

   Also declared: ComparatorChallenges/SphericalField.lean:28 (same declaration text).

7. def OAI.SphericalPerceptron.tailIntegral line 30

   Also declared: ComparatorChallenges/SphericalField.lean:30 (same declaration text).

8. def OAI.SphericalPerceptron.entropy line 33

   Also declared: ComparatorChallenges/SphericalField.lean:33 (same declaration text).

9. theorem OAI.SphericalPerceptron.timeLaw_eq_volume line 37

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

10. instance OAI.SphericalPerceptron.(instance at line 39) line 39
11. def OAI.SphericalPerceptron.finitePointMeasure line 43

    Also declared: ComparatorChallenges/SphericalField.lean:43 (same declaration text).

12. lemma OAI.SphericalPerceptron.finitePointMeasure_measurable line 46

    Also declared: ComparatorChallenges/SphericalField.lean:46 (same declaration text).

13. def OAI.SphericalPerceptron.finitePoissonLaw line 51

    Also declared: ComparatorChallenges/SphericalField.lean:51 (same declaration text).

14. instance OAI.SphericalPerceptron.finitePoissonLaw_probability line 56

    Also declared: ComparatorChallenges/SphericalField.lean:56 (same declaration text).

15. lemma OAI.SphericalPerceptron.measureSum_measurable line 70

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

16. def OAI.SphericalPerceptron.countablePoissonLaw line 77

    Also declared: ComparatorChallenges/SphericalField.lean:77 (same declaration text).

17. instance OAI.SphericalPerceptron.countablePoissonLaw_probability line 81

    Also declared: ComparatorChallenges/SphericalField.lean:81 (same declaration text).

18. def OAI.SphericalPerceptron.finiteIntensityMarks line 87

    Also declared: ComparatorChallenges/SphericalField.lean:87 (same declaration text).

19. instance OAI.SphericalPerceptron.finiteIntensityMarks_probability line 90

    Also declared: ComparatorChallenges/SphericalField.lean:90 (same declaration text).

20. def OAI.SphericalPerceptron.poissonRandomMeasureLaw line 98

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

21. instance OAI.SphericalPerceptron.poissonRandomMeasureLaw_probability line 103

    Also declared: ComparatorChallenges/SphericalField.lean:103 (same declaration text).

22. def OAI.SphericalPerceptron.stableLogIntensity line 108

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

23. instance OAI.SphericalPerceptron.stableLogIntensity_sigmaFinite line 111

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

24. def OAI.SphericalPerceptron.normalizedMeasure line 115

    Also declared: ComparatorChallenges/SphericalField.lean:115 (same declaration text).

25. lemma OAI.SphericalPerceptron.measurable_measure_withDensity_fixed line 118

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

26. lemma OAI.SphericalPerceptron.normalizedMeasure_measurable line 124

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

27. def OAI.SphericalPerceptron.markedStableTotalE line 133

    Also declared: ComparatorChallenges/SphericalField.lean:133 (same declaration text).

28. lemma OAI.SphericalPerceptron.markedStableTotalE_measurable line 136

    Also declared: ComparatorChallenges/SphericalField.lean:136 (same declaration text).

29. def OAI.SphericalPerceptron.markedStableTotal line 139

    Also declared: ComparatorChallenges/SphericalField.lean:139 (same declaration text).

30. lemma OAI.SphericalPerceptron.markedStableTotal_measurable line 141

    Also declared: ComparatorChallenges/SphericalField.lean:141 (same declaration text).

31. def OAI.SphericalPerceptron.markedStableMassKernel line 144

    Also declared: ComparatorChallenges/SphericalField.lean:144 (same declaration text).

32. instance OAI.SphericalPerceptron.markedStableMassKernel_finite line 148

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

33. def OAI.SphericalPerceptron.markedStableCountKernel line 155

    Also declared: ComparatorChallenges/SphericalField.lean:155 (same declaration text).

34. def OAI.SphericalPerceptron.DecoratedCascade line 160

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

35. instance OAI.SphericalPerceptron.decoratedCascadeNonempty line 164

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

36. def OAI.SphericalPerceptron.decoratedCascadeLaw line 170

    Also declared: ComparatorChallenges/SphericalField.lean:170 (same declaration text).

37. def OAI.SphericalPerceptron.decoratedTerminalTotalE line 177

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

38. def OAI.SphericalPerceptron.decoratedTerminalTotal line 183

    Also declared: ComparatorChallenges/SphericalField.lean:183 (same declaration text).

39. def OAI.SphericalPerceptron.gaussianShiftStep line 187

    Also declared: ComparatorChallenges/SphericalField.lean:187 (same declaration text).

40. def OAI.SphericalPerceptron.standardGaussianMark line 190

    Also declared: ComparatorChallenges/SphericalField.lean:190 (same declaration text).

41. def OAI.SphericalPerceptron.piMarkLaw line 192

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

42. def OAI.SphericalPerceptron.canonicalCoordinateStep line 196

    Also declared: ComparatorChallenges/SphericalField.lean:196 (same declaration text).

43. def OAI.SphericalPerceptron.decoratedLeafIntegral line 200

    Also declared: ComparatorChallenges/SphericalField.lean:200 (same declaration text).

44. def OAI.SphericalPerceptron.decoratedFieldFactor line 209

    Also declared: ComparatorChallenges/SphericalField.lean:209 (same declaration text).

45. def OAI.SphericalPerceptron.decoratedAngularFactor line 214

    Also declared: ComparatorChallenges/SphericalField.lean:214 (same declaration text).

46. def OAI.SphericalPerceptron.coordinateLeafField line 220

    Also declared: ComparatorChallenges/SphericalField.lean:220 (same declaration text).

47. def OAI.SphericalPerceptron.coordinateCascadeLaw line 223

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

48. def OAI.SphericalPerceptron.coordinateAngularLog line 228

    Also declared: ComparatorChallenges/SphericalField.lean:228 (same declaration text).

49. def OAI.SphericalPerceptron.normalizedCoordinateSphereLog line 234

    Also declared: ComparatorChallenges/SphericalField.lean:234 (same declaration text).

50. def OAI.SphericalPerceptron.expectedCoordinateSphereLog line 238

    Also declared: ComparatorChallenges/SphericalField.lean:238 (same declaration text).

51. def OAI.SphericalPerceptron.weightedStepTrial line 241

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

52. def OAI.SphericalPerceptron.stepCumulative line 268

    Also declared: ComparatorChallenges/SphericalField.lean:268 (same declaration text).

53. def OAI.SphericalPerceptron.stepFieldIncrement line 271

    Also declared: ComparatorChallenges/SphericalField.lean:271 (same declaration text).

54. def OAI.SphericalPerceptron.finiteSphericalFieldValue line 275

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

55. def OAI.SphericalPerceptron.finiteSphericalDualObjective line 279

    Also declared: ComparatorChallenges/SphericalField.lean:279 (same declaration text).

56. def OAI.SphericalPerceptron.finiteSphericalDualValues line 283

    Also declared: ComparatorChallenges/SphericalField.lean:283 (same declaration text).

57. structure OAI.SphericalPerceptron.FiniteFieldModel line 288

    Also declared: ComparatorChallenges/SphericalField.lean:288 (same declaration text).

58. def OAI.SphericalPerceptron.FiniteFieldModel.weight line 297

    Also declared: ComparatorChallenges/SphericalField.lean:297 (same declaration text).

59. def OAI.SphericalPerceptron.FiniteFieldModel.pressure line 300

    Also declared: ComparatorChallenges/SphericalField.lean:300 (same declaration text).

60. theorem OAI.SphericalPerceptron.exists_finiteFieldModel line 303

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

61. structure OAI.SphericalPerceptron.BoundedField line 354

    Also declared: ComparatorChallenges/SphericalField.lean:354 (same declaration text).

62. instance OAI.SphericalPerceptron.(instance at line 360) line 360
63. lemma OAI.SphericalPerceptron.BoundedField.measurable line 362

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

64. def OAI.SphericalPerceptron.roundLower line 364

    Also declared: ComparatorChallenges/SphericalField.lean:364 (same declaration text).

65. lemma OAI.SphericalPerceptron.roundLower_nonneg line 366

    Also declared: ComparatorChallenges/SphericalField.lean:366 (same declaration text).

66. lemma OAI.SphericalPerceptron.roundLower_monotone line 368

    Also declared: ComparatorChallenges/SphericalField.lean:368 (same declaration text).

67. lemma OAI.SphericalPerceptron.roundLower_le line 373

    Also declared: ComparatorChallenges/SphericalField.lean:373 (same declaration text).

68. def OAI.SphericalPerceptron.BoundedField.round line 378

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

69. lemma OAI.SphericalPerceptron.BoundedField.round_finite line 384

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

70. def OAI.SphericalPerceptron.BoundedField.roundModel line 394

    Also declared: ComparatorChallenges/SphericalField.lean:394 (same declaration text).

71. def OAI.SphericalPerceptron.quantileTrial line 397

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

72. def OAI.SphericalPerceptron.quantileTail line 411

    Also declared: ComparatorChallenges/SphericalField.lean:411 (same declaration text).

73. lemma OAI.SphericalPerceptron.quantileTail_integrable line 414

    Also declared: ComparatorChallenges/SphericalField.lean:414 (same declaration text).

74. lemma OAI.SphericalPerceptron.quantileTail_lower line 431

    Also declared: ComparatorChallenges/SphericalField.lean:431 (same declaration text).

75. lemma OAI.SphericalPerceptron.quantileTail_lipschitz line 438

    Also declared: ComparatorChallenges/SphericalField.lean:438 (same declaration text).

76. def OAI.SphericalPerceptron.boundedSphericalFieldValue line 457

    Also declared: ComparatorChallenges/SphericalField.lean:457 (same declaration text).

77. def OAI.SphericalPerceptron.BoundedField.toQuantile line 460

    Also declared: ComparatorChallenges/SphericalField.lean:460 (same declaration text).

78. lemma OAI.SphericalPerceptron.BoundedField.toQuantile_measurable line 463

    Also declared: ComparatorChallenges/SphericalField.lean:463 (same declaration text).

79. def OAI.SphericalPerceptron.quantileA line 466

    Also declared: ComparatorChallenges/SphericalField.lean:466 (same declaration text).

80. lemma OAI.SphericalPerceptron.quantileA_integrand_continuous line 469

    Also declared: ComparatorChallenges/SphericalField.lean:469 (same declaration text).

81. lemma OAI.SphericalPerceptron.quantileA_integrand_bound line 476

    Also declared: ComparatorChallenges/SphericalField.lean:476 (same declaration text).

82. lemma OAI.SphericalPerceptron.quantileA_nonneg line 483

    Also declared: ComparatorChallenges/SphericalField.lean:483 (same declaration text).

83. lemma OAI.SphericalPerceptron.quantileA_mono line 486

    Also declared: ComparatorChallenges/SphericalField.lean:486 (same declaration text).

84. lemma OAI.SphericalPerceptron.quantileA_bound line 494

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

85. def OAI.SphericalPerceptron.BoundedField.stationary line 505

    Also declared: ComparatorChallenges/SphericalField.lean:505 (same declaration text).

86. def OAI.SphericalPerceptron.clippedQuantile line 520

    Also declared: ComparatorChallenges/SphericalField.lean:520 (same declaration text).

87. def OAI.SphericalPerceptron.stationaryQuantileField line 526

    Also declared: ComparatorChallenges/SphericalField.lean:526 (same declaration text).

88. def OAI.SphericalPerceptron.SphericalLinearFieldFormula line 529

    Also declared: ComparatorChallenges/SphericalField.lean:529 (same declaration text).