Revision #2293 → #2963 · back to history
modifiedDistributions (generalized functions)23047b3379d8
| Field | From #2293 | To #2963 |
|---|
| mathlib.decl | Distribution | SchwartzMap |
| mathlib.match_kind | exact | generalization |
| mathlib.module | Mathlib.Analysis.Distribution.Distribution | Mathlib.Analysis.Distribution.SchwartzSpace |
| note | Distribution (continuous linear functionals on compactly supported test functions) and TemperedDistribution formalize generalized functions. | Mathlib has Schwartz test functions (SchwartzMap) and tempered distributions built from them, but no fully-developed general distribution theory (compactly supported test functions/D'). |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedDistributional derivative of locally integrable functionsfcb3fb13c265
| Field | From #2293 | To #2963 |
|---|
| mathlib.decl | TemperedDistribution.derivCLM | — |
| mathlib.module | Mathlib.Analysis.Distribution.TemperedDistribution | — |
| note | Distributions always have derivatives (derivCLM) and suitable functions embed via toTemperedDistribution, but the exact statement for arbitrary locally integrable functions is not a single declaration. | Mathlib does not yet formalize the distributional derivative of an arbitrary locally integrable function as a single named result. |
| provenance | ai | ai-moderated |
addedCauchy integral formula4805353ff04c
addedFundamental theorem of algebra82fd59ca59d2
addedPower seriesf00c8aed16df
addedField structure on ℝ30c26b1be0a1
addedDistance function on ℝ4f4f105b7d21
addedComplete metric space (reals)f8949fe30943
addedDerivative function42119e5df7cb
addedContinuously differentiable (C¹) functions2ac7dcea800b