Revision #3170 → #3661 · back to history
modifiedGibbs phenomenonccea874fdc3e
| Field | From #3170 | To #3661 |
|---|
| note | Grep for 'Gibbs' in Mathlib returns only Kullback–Leibler/CondVar hits; the Gibbs phenomenon is not defined. | Grep for 'Gibbs' in Mathlib returns only Kullback–Leibler/CondVar hits; the Gibbs phenomenon itself is not defined. |
modified9% overshoot around jumpaace988375be
| Field | From #3170 | To #3661 |
|---|
| note | No quantitative overshoot/Wilbraham–Gibbs constant statement is present in Mathlib. | No quantitative overshoot / Wilbraham–Gibbs constant statement is present in Mathlib. |
modifiedFourier series equals midpoint at jumpa0f00355fe01
| Field | From #3170 | To #3661 |
|---|
| note | Mathlib's Fourier theory in Analysis/Fourier/AddCircle has only L²/summable convergence, no Dirichlet-style pointwise midpoint result at jumps. | Mathlib's Fourier theory in Analysis/Fourier/AddCircle has only L²/summable convergence; no Dirichlet-style pointwise midpoint result at jumps. |
modifiedSquare wave Gibbs phenomenon6be3034be52d
| Field | From #3170 | To #3661 |
|---|
| note | Grep for 'square wave' returns no Mathlib hits and there is no square-wave Fourier series example. | Case-insensitive grep for 'square wave' returns no Mathlib hits and no square-wave Fourier series example exists. |
addedFourier coefficient decay rate for square vs triangle wave5c6c90c8fdb3
addedN-th partial Fourier series operator S_Nd9afb6e5c13d
addedPiecewise C¹ decomposition into continuous plus step-function sum6d4385af3c41
addedOvershoot equals right-tail sinc integral (step-function case)4b8753676548