Revision #1518 → #1789 · back to history
modifiedUncertainty principle (overview)059886c2a444
| Field | From #1518 | To #1789 |
|---|
| note | No Heisenberg uncertainty relation exists in Mathlib (a grep for 'uncertainty' returns nothing). | No Heisenberg uncertainty relation appears in Mathlib. |
modifiedQuantum state as Hilbert space vector4914e8144485
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Basic | Mathlib.Analysis.InnerProductSpace.Defs |
| note | Mathlib has complex inner product spaces (and completeness for Hilbert spaces) but not the quantum 'state vector' notion specifically. | Mathlib has complex inner product spaces (and Hilbert-space completeness) but not the quantum 'state vector' notion per se. |
modifiedObservables as Hermitian operatorsbf9623d89fd2
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| note | Mathlib formalizes self-adjoint/Hermitian operators (IsSelfAdjoint, LinearMap.IsSymmetric) but not their physical role as observables. | Self-adjoint/Hermitian operators are formalized (IsSelfAdjoint, LinearMap.IsSymmetric) but not labelled as observables. |
modifiedEigenstate6a7108d1504e
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| note | Eigenvectors/eigenvalues of operators are fully formalized; 'eigenstate' is the physics application of this. | Eigenvectors/eigenvalues of operators are fully formalized; 'eigenstate' is the physics application. |
modifiedQuantum superposition29618ef7e65e
| Field | From #1518 | To #1789 |
|---|
| note | Superposition is interpreted as a linear combination in a vector space; there is no specific Mathlib decl for it. | Superposition is a linear combination in a vector space; there is no specific Mathlib decl for the QM notion. |
modifiedTime-evolution operator is unitary5efb303347d7
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| note | Unitary elements/groups are formalized, but the time-evolution operator and Stone's theorem are not present. | Unitary elements/groups are formalized, but the time-evolution operator e^{-iHt/ℏ} and Stone's theorem are not. |
modifiedCanonical commutation relation784fe9cacbc9
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
modifiedUncertainty principlede2478cf4c98
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| note | The Cauchy–Schwarz inequality underlying the Robertson uncertainty relation is in Mathlib, but the uncertainty principle itself is not formalized. | Cauchy–Schwarz (the underlying Robertson uncertainty ingredient) is in Mathlib, but the uncertainty principle itself is not formalized. |
modifiedGeneralized uncertainty relationd4bb1f45b389
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| note | Cauchy–Schwarz (the key ingredient) is formalized, but the Robertson–Schrödinger relation for self-adjoint operators is not. | Cauchy–Schwarz is formalized, but the Robertson–Schrödinger relation for self-adjoint operators is not. |
modifiedPosition–momentum Fourier dualityd5646be7b435
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
modifiedTensor product of Hilbert spaces7e180ec8a52f
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Defs |
| note | Mathlib has the algebraic tensor product of modules but not the completed Hilbert-space tensor product used for composite quantum systems. | Mathlib has the algebraic tensor product of modules but not the completed Hilbert-space tensor product needed for composite quantum systems. |
modifiedProduct state of composite systemdc2f362b0f86
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Defs |
| note | Pure tensors (⊗ₜ) formalize the algebraic product state, but the quantum composite-state interpretation is not present. | Pure tensors (⊗ₜ) realize the algebraic product state, but the QM composite-state interpretation is not present. |
modifiedReduced density matrices0589d702b56b
| Field | From #1518 | To #1789 |
|---|
| note | Density matrices and partial trace are not formalized in Mathlib (no matches found). | Density matrices and partial trace are not formalized in Mathlib. |
modifiedNoether's theorem (quantum)aa95c42d5b9f
| Field | From #1518 | To #1789 |
|---|
| note | Mathlib has no Noether's theorem (all 'Noether' hits are Noetherian rings/spaces). | Mathlib has no Noether's theorem (all 'Noether' hits refer to Noetherian rings/spaces). |
modifiedGaussian wave packet85616392193b
| Field | From #1518 | To #1789 |
|---|
| note | Mathlib formalizes Gaussian functions/measures but not the QM Gaussian wave packet as a state. | Mathlib has Gaussian functions/measures but not the QM Gaussian wave packet as a state. |
modifiedHarmonic oscillator eigenstates and energy levels245246bdc496
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
addedHermite polynomials (Rodrigues formula)4fd0c2f30b69
modifiedMZI detection probabilities91cfe5588405
| Field | From #1518 | To #1789 |
|---|
| anchors | [{"section":"Mach–Zehnder interferometer","snippet":"and the probabilities that it will be detected at the right or at the top are given respectively by"},{"type":"math_alttext","value":"{\\displaystyle BPB\\psi _{l}=ie^{i\\Delta \\Phi /2}{\\begin{pmatrix}-\\sin(\\Delta \\Phi /2)\\\\\\cos(\\Delta \\Phi /2)\\end{pmatrix}},}"},{"type":"math_alttext","value":"{\\displaystyle p(u)=|\\langle \\psi _{u},BPB\\psi _{l}\\rangle |^{2}=\\cos ^{2}{\\frac {\\Delta \\Phi }{2}},}"},{"type":"math_alttext","value":"{\\displaystyle p(l)=|\\langle \\psi _{l},BPB\\psi _{l}\\rangle |^{2}=\\sin ^{2}{\\frac {\\Delta \\Phi }{2}}.}"}] | [{"section":"Mach–Zehnder interferometer","snippet":"and the probabilities that it will be detected at the right or at the top are given respectively by"},{"type":"math_alttext","value":"{\\displaystyle BPB\\psi _{l}=ie^{i\\Delta \\Phi /2}{\\begin{pmatrix}-\\sin(\\Delta \\Phi /2)\\\\\\cos(\\Delta \\Phi /2)\\end{pmatrix}},"},{"type":"math_alttext","value":"{\\displaystyle p(u)=|\\langle \\psi _{u},BPB\\psi _{l}\\rangle |^{2}=\\cos ^{2}{\\frac {\\Delta \\Phi }{2}},}"},{"type":"math_alttext","value":"{\\displaystyle p(l)=|\\langle \\psi _{l},BPB\\psi _{l}\\rangle |^{2}=\\sin ^{2}{\\frac {\\Delta \\Phi }{2}}.}"}] |
modifiedEigenstates not square-integrable0e847e7c2487
| Field | From #1518 | To #1789 |
|---|
| mathlib.match_kind | — | generalization |
addedComplex projective space of statesaff8d071b661
addedL² space for position/momentum043e5cd1d07b
addedDirac delta as position eigenstate4d82e805fb2f