Revision #1564 → #2457 · back to history
addedSignal processing6dca88a96db4
modifiedSignal as a function of time08f89e63667b
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | A signal as a real-valued function of time is not a distinguished Mathlib concept (it is just a function). |
| status | — | not_formalized |
modifiedDeterministic signal52e557e986f0
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no notion labeling a function as a deterministic signal. |
| status | — | not_formalized |
modifiedStochastic signal as path of a stochastic processc49eeeedcfda
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Probability.Process |
| note | — | Mathlib has stochastic process infrastructure (filtrations, stopping, Kolmogorov) but no explicit `stochasticProcess`/signal-realization definition. |
| status | — | partial |
modifiedAnalog signal processing997cf6a546e7
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Analog signal processing is an engineering technology outside Mathlib's scope. |
| status | — | not_formalized |
modifiedContinuous-time signal processingfb78160236a7
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Continuous-time signal processing is an engineering discipline, not a Mathlib definition. |
| status | — | not_formalized |
modifiedLTI filter output via convolution8ee7b7d9d048
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | convolution |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Analysis.Convolution |
| note | — | Mathlib defines `convolution` and many properties, but does not package the LTI-system/impulse-response equation as a distinguished result. |
| status | — | partial |
modifiedImpulse response of the systemf07182a955d2
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no notion of an impulse response for an LTI system. |
| status | — | not_formalized |
addedConvolution of input and system163406505b3e
modifiedDiscrete-time signal processing269a3bfd5ab7
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Discrete-time signal processing is an engineering discipline, not a Mathlib definition. |
| status | — | not_formalized |
modifiedAnalog discrete-time signal processing0fb42d540c17
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | This describes analog hardware technology, outside Mathlib's scope. |
| status | — | not_formalized |
modifiedDiscrete-time signal processing as theoretical discipline0f8cc67e7364
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib definition captures this meta-level discipline. |
| status | — | not_formalized |
modifiedDigital signal processingc9391828a310
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Digital signal processing is an engineering discipline, not a Mathlib concept. |
| status | — | not_formalized |
modifiedNonlinear signal processingdf65022ad7a3
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not define nonlinear signal processing as such. |
| status | — | not_formalized |
modifiedPolynomial signal processing335c149433f3
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no notion of polynomial signal processing. |
| status | — | not_formalized |
modifiedStatistical signal processinge9d45827c74b
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has probability infrastructure but no notion labeled statistical signal processing. |
| status | — | not_formalized |
modifiedNoise model for image denoisinge708e1c27073
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Image noise modeling is not a Mathlib formalizable statement. |
| status | — | not_formalized |
modifiedGraph signal processing340b4369f5a6
| Field | From #1564 | To #2457 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has graph theory but no graph signal processing definition. |
| status | — | not_formalized |