Paper V · Lean sources
Polyphase Signal Calculus
Inherited / related evidence Coverage and evidence
The edition relies on earlier or related formal evidence. That evidence is not a fresh full-edition replay.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Source files 25
Source locations and editions
Files are shown relative to source/complete/original_snapshot/formalization/lean/.
Historical editions keep their original paths. Package caches and build files are omitted.
25 files
BinaryAdaptive.leanKomorebiPaperV/CRT.leanKomorebiPaperV/CompletePrunings.leanKomorebiPaperV/CyclicSeries.leanKomorebiPaperV/FIRTransfer.leanKomorebiPaperV/FilterBank.leanKomorebiPaperV/FiniteAdaptive.leanKomorebiPaperV/FiniteSelection.leanKomorebiPaperV/FiniteTransforms.leanKomorebiPaperV/HaarChannels.leanKomorebiPaperV/HaarHilbert.leanKomorebiPaperV/HilbertPackets.leanKomorebiPaperV/IntegerPolyphase.leanKomorebiPaperV/KnownEdge.leanKomorebiPaperV/Lifting.leanKomorebiPaperV/MaskPerturbation.leanKomorebiPaperV/Packets.leanKomorebiPaperV/PruningAlgorithm.leanKomorebiPaperV/PruningSums.leanKomorebiPaperV/SmithAction.leanKomorebiPaperV/SmithCyclic.leanKomorebiPaperV/WaveletPackets.leanKomorebiPaperV/ZTransform.leanKomorebiPaperV/