OAI/Probability/GaussianReplacement/Basic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentProjection.Vector line 10

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

2. abbrev OAI.CurrentProjection.Sphere line 11

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

3. abbrev OAI.CurrentProjection.Rows line 12

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

4. def OAI.CurrentProjection.uniformSphere line 15

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

5. def OAI.CurrentProjection.gaussianRows line 20

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

6. def OAI.CurrentProjection.label line 23

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

7. def OAI.CurrentProjection.LocalGrowth line 27

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

8. def OAI.CurrentProjection.cubeAverage line 32

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

9. def OAI.CurrentProjection.exactDensity line 38

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

10. def OAI.CurrentProjection.AdmissibleDimensions line 45

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

11. def OAI.CurrentProjection.momentConstant line 48

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

12. def OAI.CurrentProjection.MixedMomentMain line 53

    Also declared: ComparatorChallenges/GaussianReplacement.lean:49 (same declaration text).