Frexlet.Monoid.Commutative.NatSemiLinear.Dirac

Properties relating to Kronecker's delta function, also known as
Dirac's delta distribution

Definitions

easyDec : {auto {conArg:1065} : DecEq a} -> (x : a) -> decEq x x = Yes Refl

Totality: total
Visibility: export

dirac : Fin n -> Fin n -> Nat

Totality: total
Visibility: public export

diracOnDiagonal : (i : Fin n) -> dirac i i = 1

Totality: total
Visibility: export

diracOffDiagonal : (i : Fin n) -> (j : Fin n) -> Not (i = j) -> dirac i j = 0

Totality: total
Visibility: export

convolveDirac : (a : CommutativeMonoid) -> (f : (Fin n -> U a)) -> (i : Fin n) -> a .rel (a .sum (tabulate (\j => dirac i j *. f j))) (f i)

Totality: total
Visibility: public export

diracSym : (i : Fin n) -> (j : Fin n) -> dirac i j = dirac j i

Totality: total
Visibility: export