Remove sampleSpace variables #112
Conversation
| b := BernoulliExpNegSampleCaseLe1(Rationals.Int(1)); | ||
| gamma' := Rationals.Rational(gamma'.numer - gamma'.denom, gamma'.denom); | ||
| assert Model.GammaReductionLoop((true, prevGamma))(prevS) == Model.GammaReductionLoop((b, gamma'))(s); |
There was a problem hiding this comment.
This file seems to be unrelated to the rest of the PR.
There was a problem hiding this comment.
The changes I made caused the resource usage of this proof to increase, which is why I had to modify it.
| @@ -26,20 +33,12 @@ module Measures { | |||
| f(i) + CountableSum(f, i+1) | |||
| } | |||
|
|
|||
| ghost function Powerset<A(!new)>(): iset<A> { | |||
There was a problem hiding this comment.
Good you remove this one. I don't think the naming was right.
| iset x: T | x !in event | ||
| } | ||
|
|
||
| ghost function SampleSpace<T(!new)>(): iset<T> { |
There was a problem hiding this comment.
This function seems very useful, even if we'd keep the generality elsewhere.
src/Math/Measures.dfy
Outdated
| Complement(iset{}) | ||
| } | ||
|
|
||
| ghost predicate IsSigmaAlgebra<T(!new)>(eventSpace: iset<iset<T>>) { |
There was a problem hiding this comment.
I don't think we should remove sampleSpace here (and elsewhere). Imo it's confusing for people that read this section for the first time, and it doesn't seem to save us from writing too much code elsewhere.
|
I find it redundant to carry around a |
|
Could you add one comment in |
|
Added some comments around σ-algebras. |
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.