Paper VIIIStatements and proofs
Statements and proofs
Find a statement anywhere in this work by title, printed number, type or source label. Entries follow the chapter order. Each proof link opens the written proof passage.
Statements by chapter
Packet operator representations
- Definition 2.1: Packet layout
- Definition 2.2: Packet operator representation
- Theorem 2.3: Exact evaluation Read proof
- Definition 2.4: Support graph
- Theorem 2.5: Block composition Read proof
- Corollary 2.6: Adjoint and tensor semantics Read proof
- Definition 2.7: Output contract
- Definition 2.8: Timing scope
- Proposition 2.9: Contract conversion Read proof
- Remark 2.10
Arithmetic, storage, and data movement
- Theorem 3.1: Dense and packet application counts Read proof
- Corollary 3.2: Equal diagonal packets Read proof
- Definition 3.3: Block diagonal plus low rank operator
- Theorem 3.4: BDLR application and storage Read proof
- Definition 3.5: One pass streaming model
- Proposition 3.6: Streaming byte count Read proof
- Definition 3.7: Arithmetic intensity
- Theorem 3.8: Roofline lower bound Read proof
- Corollary 3.9: Capacity threshold Read proof
- Proposition 3.10: Materialization cost Read proof
Structured packet primitives
- Proposition 4.1: Equal block banded count Read proof
- Proposition 4.2: Sparse plus low rank application Read proof
- Theorem 4.3: Circulant spectral representation Read proof
- Corollary 4.4: Toeplitz circulant embedding Read proof
- Theorem 4.5: Kronecker modewise application Read proof
- Corollary 4.6: Equal tensor factors Read proof
- Theorem 4.7: Walsh Hadamard recursion Read proof
Exact low rank algebra and recompression
- Theorem 5.1: Exact BDLR product Read proof
- Corollary 5.2: Rank growth in a product chain Read proof
- Theorem 5.3: Woodbury inversion Read proof
- Corollary 5.4: Inverse norm bound Read proof
- Standard fact 5.5: Eckart Young Mirsky theorem
- Theorem 5.6: Small core recompression Read proof
- Remark 5.7
- Theorem 5.8: Product chain perturbation Read proof
- Theorem 5.9: Certified repeated recompression Read proof
Sparse transfer graphs and schedules
- Theorem 6.1: Path support of powers Read proof
- Corollary 6.2: Polynomial support Read proof
- Corollary 6.3: Acyclic transfer nilpotence Read proof
- Definition 6.4: Topological level
- Theorem 6.5: Level schedule for a triangular solve Read proof
- Corollary 6.6: Sequential depth Read proof
- Theorem 6.7: Inverse support lies in the transitive closure Read proof
- Proposition 6.8: Schur support inclusion Read proof
Krylov methods and packet preconditioning
- Definition 7.1: Krylov space
- Proposition 7.2: Invariant packet Krylov decomposition Read proof
- Theorem 7.3: Approximate packet Krylov bound Read proof
- Theorem 7.4: Block Jacobi condition bound Read proof
- Standard fact 7.5: Preconditioned conjugate gradient convergence
- Corollary 7.6: Certified packet preconditioning Read proof
Packetwise mixed precision
- Theorem 8.1: Packet perturbation certificate Read proof
- Standard fact 8.2: Floating point matrix product model
- Corollary 8.3: Mixed precision product chain Read proof
- Theorem 8.4: Continuous precision allocation Read proof
- Theorem 8.5: Clipped precision allocation Read proof
- Definition 8.6: Discrete precision option
- Theorem 8.7: Exact discrete precision program Read proof
- Remark 8.8
Discovery and exact packet compilation
- Standard fact 9.1: Simultaneous spectral decomposition
- Proposition 9.2: Exact block discovery certificate Read proof
- Definition 9.3: Candidate representation tree
- Theorem 9.4: Exact Lagrangian packet compiler Read proof
- Corollary 9.5: Shared compilation for an operator family Read proof
- Proposition 9.6: Monotone Lagrangian frontier Read proof
- Corollary 9.7: Supported Pareto points Read proof
- Theorem 9.8: Quantized budget dynamic program Read proof
- Corollary 9.9: Pseudo polynomial complexity Read proof
- Definition 9.10: Decision gap
- Theorem 9.11: Compiler stability Read proof
- Theorem 9.12: Local recompilation Read proof
- Remark 9.13: Boundary of the compiler theorem