Revision #3490 → #4033 · back to history
modifiedSeriesae67a69972d0
| Field | From #3490 | To #4033 |
|---|
| mathlib.match_kind | — | generalization |
| provenance | ai | ai-moderated |
modifiedPartial sumsb5bda41be1ba
| Field | From #3490 | To #4033 |
|---|
| mathlib.match_kind | invocation | — |
| provenance | ai | ai-moderated |
modifiedSeries converging non-absolutely675743d8afef
| Field | From #3490 | To #4033 |
|---|
| mathlib.match_kind | — | invocation |
| provenance | ai | ai-moderated |
modifiedDini's theorem65b376e0a999
| Field | From #3490 | To #4033 |
|---|
| mathlib.decl | — | Monotone.tendstoUniformlyOn_of_forall_tendsto |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.UniformSpace.Dini |
| note | Dini's theorem (monotone pointwise convergence to a continuous limit on a compact set is uniform) does not appear to have a single named declaration in Mathlib. | Monotone.tendstoUniformlyOn_of_forall_tendsto in Mathlib.Topology.UniformSpace.Dini is Dini's theorem: monotone pointwise convergence to a continuous limit on a compact set is uniform. |
| status | partial | formalized |
modifiedLebesgue differentiation theoremc5d50fb93f9a
| Field | From #3490 | To #4033 |
|---|
| mathlib.decl | — | VitaliFamily.ae_tendsto_average |
| mathlib.match_kind | — | generalization |
| note | Mathlib has Vitali-family differentiation lemmas (tendsto_ae limits of averages over shrinking balls) but no single named 'Lebesgue differentiation theorem'. | VitaliFamily.ae_tendsto_average is the Vitali-family form of Lebesgue differentiation (averages over shrinking sets converge to f a.e.), with no standalone named 'Lebesgue differentiation theorem' for balls in ℝⁿ. |
modifiedPlancherel theoremc4a6c0c77986
| Field | From #3490 | To #4033 |
|---|
| mathlib.decl | — | MeasureTheory.Lp.norm_fourier_eq |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Fourier.LpSpace |
| note | Mathlib has partial Fourier-isometry results for L² but no single named Plancherel theorem declaration. | MeasureTheory.Lp.norm_fourier_eq is the Plancherel identity ‖ℱf‖ = ‖f‖ on L², with MeasureTheory.Lp.instFourierTransform giving the corresponding L² isometry. |
| status | partial | formalized |