Idris2Doc : Statistics.Confidence

Statistics.Confidence

(source)
Reexports
import public Data.Functor.TraverseSt
import public Data.Nat
import public Data.Vect
import public Statistics.Norm.Rough
import public Statistics.Probability
Definitions
wilsonBounds : InvNormCDF => Probability -> (count : Nat) -> {auto 0 _ : IsSucc count} -> Probability -> (Probability, Probability)
  Totality: total
  Visibility: export
record CoverageTest : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
Cover : (checkedProbability : (Probability, Probability)) -> {auto 0 _ : So (fst checkedProbability <= snd checkedProbability)} -> (a -> Bool) -> CoverageTest a

  Projections:
  
.checkedProbability : CoverageTest a -> (Probability, Probability)
  
.maximalProbability : CoverageTest a -> Probability
  
0 .minMaxCorrect : ({rec:0} : CoverageTest a) -> So (fst (checkedProbability {rec:0}) <= snd (checkedProbability {rec:0}))
  
.minimalProbability : CoverageTest a -> Probability
  
.successCondition : CoverageTest a -> a -> Bool
.checkedProbability : CoverageTest a -> (Probability, Probability)
  Totality: total
  Visibility: public export
checkedProbability : CoverageTest a -> (Probability, Probability)
  Totality: total
  Visibility: public export
0 .minMaxCorrect : ({rec:0} : CoverageTest a) -> So (fst (checkedProbability {rec:0}) <= snd (checkedProbability {rec:0}))
  Totality: total
  Visibility: public export
0 minMaxCorrect : ({rec:0} : CoverageTest a) -> So (fst (checkedProbability {rec:0}) <= snd (checkedProbability {rec:0}))
  Totality: total
  Visibility: public export
.successCondition : CoverageTest a -> a -> Bool
  Totality: total
  Visibility: public export
successCondition : CoverageTest a -> a -> Bool
  Totality: total
  Visibility: public export
minimalProbability : CoverageTest a -> Probability
  Totality: total
  Visibility: public export
.minimalProbability : CoverageTest a -> Probability
  Totality: total
  Visibility: public export
maximalProbability : CoverageTest a -> Probability
  Totality: total
  Visibility: public export
.maximalProbability : CoverageTest a -> Probability
  Totality: total
  Visibility: public export
DefaultTolerance : Probability
  Totality: total
  Visibility: public export
coverBetween : {default DefaultTolerance _ : Probability} -> Probability -> Probability -> (a -> Bool) -> CoverageTest a
  Totality: total
  Visibility: export
coverMin : {default DefaultTolerance _ : Probability} -> Probability -> (a -> Bool) -> CoverageTest a
  Totality: total
  Visibility: export
coverWith : {default DefaultTolerance _ : Probability} -> Probability -> (a -> Bool) -> CoverageTest a
  Totality: total
  Visibility: export
DefaultConfidence : Probability
  Totality: total
  Visibility: public export
record CoverageTestState : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCoverageTestState : (Probability, Probability) -> (Probability, Probability) -> CoverageTestState

  Projections:
  
.testedBounds : CoverageTestState -> (Probability, Probability)
  
.wilsonBounds : CoverageTestState -> (Probability, Probability)

  Hint: 
Interpolation CoverageTestState
.testedBounds : CoverageTestState -> (Probability, Probability)
  Totality: total
  Visibility: public export
testedBounds : CoverageTestState -> (Probability, Probability)
  Totality: total
  Visibility: public export
.wilsonBounds : CoverageTestState -> (Probability, Probability)
  Totality: total
  Visibility: public export
wilsonBounds : CoverageTestState -> (Probability, Probability)
  Totality: total
  Visibility: public export
checkCoverageConditions' : TraversableSt t => InvNormCDF => {default DefaultConfidence _ : Probability} -> Vect n (CoverageTest a) -> t a -> t (Vect n CoverageTestState)
  Totality: total
  Visibility: export
data SignificantBounds : Type
  Totality: total
  Visibility: public export
  Constructors:
  
BoundsOk : SignificantBounds
  
UpperBoundViolated : Probability -> SignificantBounds
  
LowerBoundViolated : Probability -> SignificantBounds

  Hint: 
Interpolation SignificantBounds
isOk : SignificantBounds -> Bool
  Totality: total
  Visibility: public export
CoverageTestResult : Type
  Totality: total
  Visibility: public export
coverageTestResult : CoverageTestState -> CoverageTestResult
  Totality: total
  Visibility: export
checkCoverageConditions : TraversableSt t => InvNormCDF => {default DefaultConfidence _ : Probability} -> Vect n (CoverageTest a) -> t a -> t (Vect n CoverageTestResult)
  Totality: total
  Visibility: export
checkCoverageCondition : TraversableSt t => InvNormCDF => {default DefaultConfidence _ : Probability} -> CoverageTest a -> t a -> t CoverageTestResult
  Totality: total
  Visibility: export