Revision #1658 → #1812 · back to history
7e5773a86e68| Field | From #1658 | To #1812 |
|---|---|---|
| mathlib.decl | gaussianPDFReal | ProbabilityTheory.gaussianPDFReal |
| note | The Gaussian function itself is formalized (gaussianPDFReal, and complex Gaussians in the Fourier file), but the physics wave-packet object is not. | The Gaussian function itself is formalized (ProbabilityTheory.gaussianPDFReal, and complex Gaussians in the Fourier file), but the physics wave-packet object is not. |
5dff81e1d01f