0 | module Statistics.Confidence
2 | import public Data.Functor.TraverseSt
5 | import public Data.Nat
7 | import public Data.Vect
9 | import public Statistics.Norm.Rough
10 | import public Statistics.Probability
21 | (confidence : Probability) ->
23 | (0 _ : IsSucc count) =>
24 | (successes : Probability) ->
25 | (Probability, Probability)
26 | wilsonBounds confidence count successes =
29 | p = successes.asDouble
30 | z = cast $
invnormcdf $
inv $
confidence / 2
33 | midpoint = p + zz_n / 2
35 | offset = z / (1 + zz_n) * sqrt (p * (1 - p) / n + zz_n / (4 * n))
37 | denominator = 1 + zz_n
39 | low = (midpoint - offset) / denominator
40 | high = (midpoint + offset) / denominator
42 | in if low == low && high == high
43 | then mapHom (P . roughlyFit) (low, high)
49 | record CoverageTest a where
51 | checkedProbability : (Probability, Probability)
52 | {auto 0 minMaxCorrect : So $
fst checkedProbability <= snd checkedProbability}
53 | successCondition : a -> Bool
55 | namespace CoverageTest
57 | public export %inline
58 | minimalProbability : CoverageTest a -> Probability
59 | minimalProbability = fst . checkedProbability
61 | public export %inline
62 | (.minimalProbability) : CoverageTest a -> Probability
63 | (.minimalProbability) = minimalProbability
65 | public export %inline
66 | maximalProbability : CoverageTest a -> Probability
67 | maximalProbability = snd . checkedProbability
69 | public export %inline
70 | (.maximalProbability) : CoverageTest a -> Probability
71 | (.maximalProbability) = maximalProbability
73 | namespace CoverageTest
75 | public export %inline
76 | DefaultTolerance : Probability
77 | DefaultTolerance = 95.percent
80 | coverBetween : {default DefaultTolerance tolerance : Probability} ->
81 | (minP, maxP : Probability) ->
82 | (successCondition : a -> Bool) ->
84 | coverBetween minP maxP = do
85 | let (minP, maxP) = (min minP maxP, max minP maxP)
86 | let minP = minP * tolerance
87 | let maxP = inv $
maxP.inv * tolerance
88 | let maxP = if maxP <= minP then minP else maxP
89 | Cover (minP, maxP) @{believe_me Oh}
92 | coverMin : {default DefaultTolerance tolerance : Probability} ->
93 | (minP : Probability) ->
94 | (successCondition : a -> Bool) ->
96 | coverMin minP = coverBetween {tolerance} minP 1
99 | coverWith : {default DefaultTolerance tolerance : Probability} ->
100 | (singleP : Probability) ->
101 | (successCondition : a -> Bool) ->
103 | coverWith singleP = coverBetween {tolerance} singleP singleP
106 | DefaultConfidence : Probability
107 | DefaultConfidence = 1/1000000000
112 | record CoverageTestState where
113 | constructor MkCoverageTestState
114 | testedBounds : (Probability, Probability)
115 | wilsonBounds : (Probability, Probability)
118 | [NoAnalysis] Interpolation CoverageTestState where
119 | interpolate $
MkCoverageTestState (minP, maxP) (wLow, wHigh) = do
120 | let ss = if minP == maxP && wLow /= minP && wHigh /= maxP
121 | then [ (wLow , "[\{show wLow}")
122 | , (minP , "(\{show minP})")
123 | , (wHigh, "\{show wHigh}]")
125 | else [ (minP , "(\{show minP}")
126 | , (wLow , "[\{show wLow}")
127 | , (wHigh, "\{show wHigh}]")
128 | , (maxP , "\{show maxP})")
130 | unwords $
map snd $
sortBy (comparing fst) ss
133 | [Means] Interpolation CoverageTestState where
134 | interpolate $
MkCoverageTestState expected wilson = "expected: \{interpolatePair expected}, wilson: \{interpolatePair wilson}" where
135 | interpolatePair : (Probability, Probability) -> String
136 | interpolatePair (lo, hi) = do
139 | if lo == hi then "\{show lo}" else with Bounded.(+) with Bounded.(/) with Bounded.(-) do
140 | let mi = (lo + hi) / 2
142 | "\{show mi} ± \{show di}"
145 | checkCoverageConditions' :
148 | {default DefaultConfidence confidence : Probability} ->
149 | Vect n (CoverageTest a) ->
151 | t $
Vect n CoverageTestState
153 | checkCoverageConditions' coverageTests = traverseSt initialResults checkCoverageOnce where
155 | data PastResults : Type where
156 | R : (attempts : Nat) -> (successes : Vect n $
Subset Nat (`LTE` attempts)) -> PastResults
158 | initialResults : PastResults
159 | initialResults = R 0 $
coverageTests <&> const (0 `Element` LTEZero)
161 | checkCoverageOnce : PastResults -> a -> (PastResults, Vect n CoverageTestState)
162 | checkCoverageOnce (R prevAttempts prevResults) x = do
163 | let %inline currAttempts : Nat;
currAttempts = S prevAttempts
164 | mapFst (R currAttempts) $
unzip $
coverageTests `zip` prevResults <&>
165 | \(Cover checkedP@(minP, maxP) cond, Element prevSucc _) => do
166 | let pr@(Element currSucc _) = if cond x
167 | then S prevSucc `Element` LTESucc %search
168 | else prevSucc `Element` lteSuccRight %search
169 | (pr, MkCoverageTestState checkedP $
wilsonBounds confidence currAttempts $
ratio currSucc currAttempts)
174 | data SignificantBounds
176 | | UpperBoundViolated Probability
177 | | LowerBoundViolated Probability
180 | isOk : SignificantBounds -> Bool
181 | isOk BoundsOk = True
185 | Interpolation SignificantBounds where
186 | interpolate BoundsOk = "ok"
187 | interpolate $
UpperBoundViolated x = "(..., ...) --> \{show x}"
188 | interpolate $
LowerBoundViolated x = "\{show x} <-- (..., ...)"
191 | public export %inline
192 | CoverageTestResult : Type
193 | CoverageTestResult = Maybe SignificantBounds
196 | coverageTestResult : CoverageTestState -> CoverageTestResult
197 | coverageTestResult $
MkCoverageTestState (minP, maxP) (wLow, wHigh) =
198 | if wLow >= minP && wHigh <= maxP then Just BoundsOk
199 | else if wLow > maxP then Just $
UpperBoundViolated wLow
200 | else if wHigh < minP then Just $
LowerBoundViolated wHigh
204 | Interpolation CoverageTestState where
205 | interpolate cts@(MkCoverageTestState (minP, maxP) (wLow, wHigh)) = case coverageTestResult cts of
206 | Just BoundsOk => "ok"
207 | Just (UpperBoundViolated _) => "(..., \{show maxP}) --> \{show wLow}"
208 | Just (LowerBoundViolated _) => "\{show wLow} <-- (\{show minP}, ...)"
209 | Nothing => "\{show wLow} .. \{show wHigh} still covers (\{show minP}, \{show maxP})"
212 | checkCoverageConditions :
215 | {default DefaultConfidence confidence : Probability} ->
216 | Vect n (CoverageTest a) ->
218 | t $
Vect n CoverageTestResult
219 | checkCoverageConditions = map @{Compose} coverageTestResult .: checkCoverageConditions' {confidence}
222 | checkCoverageCondition :
225 | {default DefaultConfidence confidence : Probability} ->
228 | t CoverageTestResult
229 | checkCoverageCondition ct = map head . checkCoverageConditions {confidence} [ct]