Revision #3217 → #3736 · back to history
modifiedDecomposition into sinusoidal plane wavesd2a92d185293
| Field | From #3217 | To #3736 |
|---|
| note | Mathlib formalizes Fourier-series decomposition into exponentials/sinusoids (L² convergence), the rigorous analog, but not the physical plane-wave decomposition. | Mathlib formalizes Fourier-series decomposition into exponentials/sinusoids (L² convergence via hasSum_fourier_series_L2), the rigorous analog, but not the physical plane-wave decomposition. |
modifiedd'Alembert's formula8bae4362e3df
| Field | From #3217 | To #3736 |
|---|
| anchors | [{"section":"Wave in elastic medium","snippet":"more generally, by d'Alembert's formula"},{"type":"math_alttext","value":"{\\displaystyle u(x,t)=F(x-vt)+G(x+vt).}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{v^{2}}}{\\frac {\\partial ^{2}u}{\\partial t^{2}}}={\\frac {\\partial ^{2}u}{\\partial x^{2}}}.}"}] | — |
modifiedEnvelope of a wave54a30ea47181
| Field | From #3217 | To #3736 |
|---|
| anchors | [{"section":"Amplitude and modulation","snippet":"The outline of the variation in amplitude is called the envelope of the wave."},{"type":"math_alttext","value":"{\\displaystyle u(x,t)=A(x,t)\\sin \\left(kx-\\omega t+\\phi \\right),}"},{"type":"math_alttext","value":"{\\displaystyle u(x,t)=A(x-v_{g}t)\\sin \\left(kx-\\omega t+\\phi \\right),}"}] | — |
modifiedEnvelope moves with group velocity093761ab421b
| Field | From #3217 | To #3736 |
|---|
| anchors | [{"section":"Amplitude and modulation","snippet":"showing that the envelope moves with the group velocity and retains its shape"},{"type":"math_alttext","value":"{\\displaystyle u(x,t)=A(x,t)\\sin \\left(kx-\\omega t+\\phi \\right),}"},{"type":"math_alttext","value":"{\\displaystyle u(x,t)=A(x-v_{g}t)\\sin \\left(kx-\\omega t+\\phi \\right),}"}] | — |
modifiedPhase velocityd2183cb62e67
| Field | From #3217 | To #3736 |
|---|
| anchors | [{"section":"Phase velocity and group velocity","snippet":"Phase velocity is the rate at which the phase of the wave propagates in space"},{"type":"math_alttext","value":"{\\displaystyle v_{\\mathrm {p} }={\\frac {\\lambda }{T}}.}"}] | — |
modifiedLinear combination of sine wavescbc311faddca
| Field | From #3217 | To #3736 |
|---|
| mathlib.module | Mathlib.Analysis.Complex.Trigonometric | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic |
| provenance | ai | ai-moderated |
modifiedSum of counter-propagating waves7c0d8a3efe95
| Field | From #3217 | To #3736 |
|---|
| mathlib.module | Mathlib.Analysis.Complex.Trigonometric | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic |
| provenance | ai | ai-moderated |
modifiedPhase velocity formulaa68089abaa62
| Field | From #3217 | To #3736 |
|---|
| anchors | [{"section":"Wave velocity","snippet":"The phase velocity is given as"},{"type":"math_alttext","value":"{\\displaystyle v_{\\rm {p}}={\\frac {\\omega }{k}},}"}] | — |
modifiedDispersion relationship6754286504f8
| Field | From #3217 | To #3736 |
|---|
| anchors | [{"section":"Wave velocity","snippet":"both are related through the dispersion relationship"},{"type":"math_alttext","value":"{\\displaystyle \\omega =\\Omega (k).}"}] | — |
modifiedGroup velocity from dispersion gradiente2497ff6045f
| Field | From #3217 | To #3736 |
|---|
| anchors | [{"section":"Wave velocity","snippet":"is called the group velocity and is determined from the gradient of the dispersion relation"},{"type":"math_alttext","value":"{\\displaystyle v_{\\rm {g}}={\\frac {\\partial \\omega }{\\partial k}}}"}] | — |
addedWavelength–wavevector relationc3f3c6bbc02c
addedFourier transform scaling: spatial/frequency spread78ecafa74b17