Revision #2351 → #3074 · back to history
4ac134c57f61| Field | From #2351 | To #3074 |
|---|---|---|
| mathlib.decl | PiLp.norm_eq_card | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.Analysis.Normed.Lp.PiLp | — |
| note | PiLp.norm_eq_card on PiLp 0 gives the cardinality of the nonzero support, matching the Donoho zero-norm informally (though it is not a true norm). | Mathlib does not define PiLp at p=0; the Donoho zero "norm" (support size) has no direct formalization as a norm-like object. |
| status | partial | not_formalized |
2e6501343e4f28c269ed8e4fb9429d2873829136188404bdaa197a52dbcfd94dc170f8cc066b231f2d59