OAI/Probability/SKValue/Model.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.standardGaussian line 10

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

2. instance OAI.SKValue.(instance at line 12) line 12
3. def OAI.SKValue.gaussianProduct line 14

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

4. instance OAI.SKValue.gaussianProduct_probability line 16

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

5. def OAI.SKValue.coordinate line 21

   Also declared: ComparatorChallenges/SKValue.lean:21 (same declaration text).

6. def OAI.SKValue.stepSize line 24

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

7. def OAI.SKValue.meshTime line 25

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

8. def OAI.SKValue.euler line 27

   Also declared: ComparatorChallenges/SKValue.lean:27 (same declaration text).

9. structure OAI.SKValue.OrderParameter line 33

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

10. structure OAI.SKValue.BrownianSpace line 40

    Also declared: ComparatorChallenges/SKValue.lean:40 (same declaration text).

11. def OAI.SKValue.BrownianSpace.filtration line 51

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

12. def OAI.SKValue.shiftedFiltration line 54

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

13. def OAI.SKValue.Admissible line 59

    Also declared: ComparatorChallenges/SKValue.lean:59 (same declaration text).

14. def OAI.SKValue.controlPayoff line 62

    Also declared: ComparatorChallenges/SKValue.lean:62 (same declaration text).

15. def OAI.SKValue.phi line 68

    Also declared: ComparatorChallenges/SKValue.lean:68 (same declaration text).

16. def OAI.SKValue.gradient line 71

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

17. def OAI.SKValue.curvature line 74

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

18. def OAI.SKValue.parisi line 77

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

19. def OAI.SKValue.IsMinimizer line 80

    Also declared: ComparatorChallenges/SKValue.lean:80 (same declaration text).

20. def OAI.SKValue.IsDiffusion line 83

    Also declared: ComparatorChallenges/SKValue.lean:83 (same declaration text).

21. def OAI.SKValue.spin line 90

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

22. def OAI.SKValue.hamiltonian line 92

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

23. def OAI.SKValue.groundStateSequence line 97

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

24. def OAI.SKValue.groundStateValue line 100

    Also declared: ComparatorChallenges/SKValue.lean:100 (same declaration text).

25. def OAI.SKValue.gradientStopped line 102

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

26. def OAI.SKValue.ScalarValueConclusion line 106

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

27. def OAI.SKValue.eulerPath line 120

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

28. def OAI.SKValue.rawCoefficient line 124

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

29. def OAI.SKValue.normalizer line 128

    Also declared: ComparatorChallenges/SKValue.lean:128 (same declaration text).

30. def OAI.SKValue.gaussianIncrement line 132

    Also declared: ComparatorChallenges/SKValue.lean:132 (same declaration text).

31. def OAI.SKValue.roundedSign line 136

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

32. def OAI.SKValue.coefficientA line 141

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

33. def OAI.SKValue.coefficientB line 147

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

34. def OAI.SKValue.shiftedCoefficientSum line 151

    Also declared: ComparatorChallenges/SKValue.lean:151 (same declaration text).

35. def OAI.SKValue.FiniteGaussianConclusion line 155

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