covstream 0.1.2

Lean-backed fixed-dimension streaming covariance and Ledoit-Wolf shrinkage
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

import Covstream.Welford
import Covstream.LedoitWolf
import Covstream.FrobeniusLoss
import Covstream.Contract
import Covstream.ErrorBounds
import Covstream.Examples

/-!
Top-level umbrella import for the `Covstream` formalization.

The development is organized in six reader-facing modules:

1. `Covstream.Welford`
   The exact Real-valued streaming covariance specification and its correspondence
   with the classical batch covariance formula.
2. `Covstream.LedoitWolf`
   The structural shrinkage layer: target matrix, convex shrinkage, and
   symmetry / PSD preservation.
3. `Covstream.FrobeniusLoss`
   The optimization layer: Frobenius loss expansion and oracle shrinkage
   coefficients.
4. `Covstream.Contract`
   A runtime-facing checked API contract for Rust/C++ implementations.
5. `Covstream.ErrorBounds`
   Abstract perturbation lemmas for future floating-point refinement work.
6. `Covstream.Examples`
   Small concrete 2D examples of the checked API.

The internal optimization code is split between:

* `Covstream.FrobeniusBasic`
* `Covstream.ShrinkageOptimization`
-/