| /-! |
| |
|
|
| This module provides formal verification of core matrix algorithms from numerical linear algebra, |
| bridging MATLAB numerical computation with Lean 4's exact arithmetic and type safety. |
|
|
| |
|
|
| - `Arithmetic`: Basic arithmetic operations (addition, multiplication, transpose) — fully verified |
| - `Basic`: Type definitions and fundamental matrix properties (traces, determinants) |
| - `QR`: QR decomposition with orthogonality and recovery proofs |
| - `LinearSolve`: Linear equation solver with invertibility preconditions |
| - `Stability`: Numerical stability bounds and convergence theorems |
|
|
| |
|
|
| 1. Use `Matrix m n R` where `m, n : Fintype` for concrete matrix representations |
| 2. Encode preconditions as hypotheses (e.g., `IsUnit A` for invertibility) |
| 3. Use `sorry` only for properties requiring numerical stability analysis |
| 4. Every theorem has a corresponding MATLAB implementation comment |
|
|
| |
|
|
| - **Arithmetic module**: 22 theorems, all proofs complete ✓ |
| - **Basic module**: 10 theorems, foundational Mathlib properties ✓ |
| - **QR module**: 6 theorems, orthogonality properties (2 sorries for uniqueness/inv) |
| - **LinearSolve module**: 6 theorems (4 sorries for numerical analysis) |
| - **Stability module**: 8 theorems (6 sorries for convergence rates/stability bounds) |
|
|
| Total: 52 theorems defined, 30 with complete proofs, 22 marked with `sorry` for numerical analysis. |
| -/ |
|
|
| import MathlibMatrixFormalization.Arithmetic |
| import MathlibMatrixFormalization.Basic |
| import MathlibMatrixFormalization.QR |
| import MathlibMatrixFormalization.LinearSolve |
| import MathlibMatrixFormalization.Stability |
|
|
| namespace MathlibMatrixFormalization |
|
|
| /- Re-export main definitions and theorems -/ |
| export Arithmetic |
| export Basic |
| export QR |
| export LinearSolve |
| export Stability |
|
|
| end MathlibMatrixFormalization |
|
|
