Distribution

Probability distributions.

Definitions

interface Distribution : ((0 _ : Shape) -> (0 _ : Nat) -> Type) -> Type

  A joint, or multivariate distribution over a tensor of floating point values, where the first
  two central moments (mean and covariance) are known. Every sub-event is assumed to have the
  same shape.
  
  @dist Constructs the distribution from the shape of each sub-event and the number of events in
    the distribution.

Parameters: dist
Methods:

mean : dist event dim -> Tag (Tensor (dim :: event) F64)

  The mean of the distribution.

cov : dist event dim -> Tag (Tensor (dim :: (dim :: event)) F64)

  The covariance, or correlation, between sub-events.

Implementation: 

Distribution Gaussian

mean : Distribution dist => dist event dim -> Tag (Tensor (dim :: event) F64)

  The mean of the distribution.

Totality: total
Visibility: public export

cov : Distribution dist => dist event dim -> Tag (Tensor (dim :: (dim :: event)) F64)

  The covariance, or correlation, between sub-events.

Totality: total
Visibility: public export

variance : Distribution dist => dist event 1 -> Tag (Tensor (1 :: event) F64)

  The variance of a single random variable.

Totality: total
Visibility: export

interface ClosedFormDistribution : Shape -> ((0 _ : Shape) -> (0 _ : Nat) -> Type) -> Type

  A joint, or multivariate distribution over a tensor of floating point values, where the density
  function and corresponding cumulative density function are known (either analytically or via
  approximation). Every sub-event is assumed to have the same shape.
  
  @event The shape of each sub-event.
  @dist Constructs the distribution from the shape of each sub-event and the number of events in
    the distribution.

Parameters: event, dist
Constraints: Distribution dist
Methods:

pdf : dist event (S d) -> Tensor (S d :: event) F64 -> Tag (Tensor [] F64)

  The probability density function of the distribution at the specified point.

cdf : dist event (S d) -> Tensor (S d :: event) F64 -> Tag (Tensor [] F64)

  The cumulative distribution function of the distribution at the specified point (that is,
  the probability the random variable takes a value less than or equal to the given point).

Implementation: 

ClosedFormDistribution [1] Gaussian

pdf : ClosedFormDistribution event dist => dist event (S d) -> Tensor (S d :: event) F64 -> Tag (Tensor [] F64)

  The probability density function of the distribution at the specified point.

Totality: total
Visibility: public export

cdf : ClosedFormDistribution event dist => dist event (S d) -> Tensor (S d :: event) F64 -> Tag (Tensor [] F64)

  The cumulative distribution function of the distribution at the specified point (that is,
  the probability the random variable takes a value less than or equal to the given point).

Totality: total
Visibility: public export

data Gaussian : (0 _ : Shape) -> (0 _ : Nat) -> Type

  A joint Gaussian distribution.
  
  @event The shape of each sub-event.
  @dim The number of sub-events.

Totality: total
Visibility: public export
Constructor: 

MkGaussian : Tensor (S d :: event) F64 -> Tensor (S d :: (S d :: event)) F64 -> Gaussian event (S d)

  @mean The mean of the events.
  @cov The covariance between events.

Hints:

ClosedFormDistribution [1] Gaussian

Distribution Gaussian

Taggable (Gaussian event dim)