Revision #1379 → #1840 · back to history
modifiedp-norm satisfies norm properties4a76e3074480
| Field | From #1379 | To #1840 |
|---|
| mathlib.decl | PiLp.instNormedAddCommGroup | PiLp.normedAddCommGroup |
| note | PiLp p β under [Fact (1 ≤ p)] carries a NormedAddCommGroup instance encoding the norm axioms. | PiLp.normedAddCommGroup endows PiLp p α with a NormedAddCommGroup under [Fact (1 ≤ p)], packaging all the norm axioms. |
modifiedL^0 norm (Banach F-norm)b6779ed2088f
| Field | From #1379 | To #1840 |
|---|
| mathlib.module_note | — | — |
| provenance | ai | ai-moderated |
modifiedZero "norm" (Donoho)4ac134c57f61
| Field | From #1379 | To #1840 |
|---|
| note | PiLp.norm_eq_card defines ‖f‖ on PiLp 0 as the cardinality of the nonzero-coordinate set. | 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). |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedEqual almost everywhere593212f8c33c
| Field | From #1379 | To #1840 |
|---|
| mathlib.module | Mathlib.Order.Filter.Germ.Basic | Mathlib.Order.Filter.Defs |
modifiedSeminorm property of L^p-seminorm08274f415d04
| Field | From #1379 | To #1840 |
|---|
| mathlib.decl | MeasureTheory.Lp.instSeminormedAddCommGroup | MeasureTheory.Lp.instNormedAddCommGroup |
| note | Lp E p μ is shown to be a SeminormedAddCommGroup, packaging all seminorm axioms. | Lp E p μ carries a NormedAddCommGroup instance, which packages absolute homogeneity, triangle inequality, and non-negativity (the seminorm axioms) on the quotient. |
modifiedDensity of continuous integrable functions95d0536d614b
| Field | From #1379 | To #1840 |
|---|
| mathlib.decl | MeasureTheory.ContinuousMap.toLp_denseRange | ContinuousMap.toLp_denseRange |
| note | ContinuousMap.toLp_denseRange shows continuous functions are dense in Lp under suitable regularity assumptions. | ContinuousMap.toLp_denseRange shows continuous functions are dense in Lp under suitable regularity assumptions on a compact normal space. |
modifiedContinuous compactly supported functions dense in L^p(R^n)604f8b55f218
| Field | From #1379 | To #1840 |
|---|
| mathlib.decl | MeasureTheory.BoundedContinuousFunction.toLp_denseRange | BoundedContinuousFunction.toLp_denseRange |
| note | BoundedContinuousFunction.toLp_denseRange gives density of continuous (bounded) functions in Lp for weakly regular finite measures, e.g. Lebesgue measure on compact sets. | BoundedContinuousFunction.toLp_denseRange gives density of bounded continuous functions in Lp for weakly regular finite measures, e.g. Lebesgue measure on compact sets. |
addedHamming distance is a valid metric845b7cfb9bc7
addedBochner L^p generalizationad6dfa0f6a4a