Module formal_model
Functionsยง
- circular_
backward_ index - circular_
forward_ index - clamp_
index - downsample_
len - dwt_
output_ len - law_
circular_ backward_ index_ in_ range - law_
circular_ forward_ index_ in_ range - law_
circular_ indices_ inverse - law_
clamp_ index_ in_ range - law_
downsample_ halves - law_
dwt_ output_ len_ covers - law_
dwt_ output_ len_ no_ grow - law_
lifting_ remainder_ le_ one - law_
lifting_ split_ exact - law_
mirror_ index_ in_ range - law_
pad_ to_ even_ ok - law_
periodic_ left_ source_ in_ range - law_
periodic_ right_ source_ in_ range - law_
ring_ push_ len_ bounded - law_
sample_ count_ due_ is_ multiple - law_
swt_ effective_ support_ bounds - law_
symmetric_ reflect_ in_ range - law_
upsample_ doubles - lifting_
pairs - lifting_
remainder - mirror_
index - pad_
to_ even - periodic_
left_ source - periodic_
right_ source - ring_
push_ len - sample_
count_ due - swt_
effective_ support - symmetric_
reflect - upsample_
len