TODO List

Create a new file for the geometric model which properly models the position as a configuration space and velocity as its tangent space, see the HarmonicOscillator file.

Define and prove properties of the quality factor Q.

Define and prove properties of the relaxation time τ.

Create a new file for the geometric model which properly models the position as a configuration space and velocity as its tangent space, then show explicitly how this coordinate model is a simplification of the geometric model. A nice reference for such an analysis is: https://web.williams.edu/Mathematics/it3/texts/var_noether.pdf

The API around the configuration space should be improved to allow further development of a proper geometric model of the Harmonic Oscillator.

Split this file into smaller modules, keeping `Solution.lean` as an umbrella import. The intended organization is: - `Solution.Basic` for trajectory construction and equation-of-motion facts; - `Solution.Energy` for energy-related lemmas; - `Solution.InitialData` for alternative initial-condition parametrizations; - `Solution.AmplitudePhase` for the amplitude-phase normal form; - `Solution.SpecialTimes` for velocity-zero times, turning points, and zero crossings; - `Solution.Periodicity` for period and recurrence facts.

The definition of a rigid body is currently defined via linear maps from the space of smooth functions to ℝ. When possible, it should be change to *continuous* linear maps.

Move `cmap` and `cmap_apply` to a more general location, such as a file in `SpaceAndTime/Space/` or `Mathematics/`. Alternatively, define a version of `ρ` taking an unbundled `(f : Space d → ℝ) (hf : ContDiff ℝ ⊤ f)` in place of a `ContMDiffMap`.

One can describe the motion of rigid body with a fixed (inertial) coordinate system (X,Y,Z) and a moving system (x₁,x₂,x₃) rigidly attached to the body.

A rigid body in three-dimensional space has six degrees of freedom: three translational (for the position of its centre of mass) and three rotational (for its orientation).

The velocity v of any point in a rigid body is v = V + Ω × r, where V is the velocity of the origin of the moving system and Ω is the angular velocity.

The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen.

The motion of a rigid body can be decomposed into a translation of some reference point plus a rotation about that point. There exists a time-dependent vector V(t) and angular velocity ω(t) such that v(r) = V + ω × r, where r is measured from the reference point.

The centre of mass of a rigid body moves as if all mass were concentrated at that point and acted upon by the resultant external force: M a_CM = ∑ F_ext.

The total angular momentum about a point O is L = ∫ r × v dm. With v = V + ω × r about the centre of mass, L = R × (M V) + I_CM ω, where R is the centre of mass position.

In the inertial frame, the translational equation of motion of a rigid body is given by dP/dt = F, where `P` is the total linear momentum and `F` is the total external force acting on the body.

In the inertial frame, the rotational equation of motion of a rigid body about the center of mass is given by dM/dt = K, where `M` is the total angular momentum and `K` is the total external torque.

The kinetic energy decomposes into translational and rotational parts: T = (1/2) M |V|² + (1/2) ω ⋅ I_CM ω. Here V is the velocity of the centre of mass and I_CM is the inertia tensor about that point.

If I_O is the inertia tensor about a point O, then the inertia tensor about a parallel point O' displaced by a is I_{O'} = I_O + M(|a|² 1 − a ⊗ a). This is the parallel-axis theorem.

Because the inertia tensor is real symmetric, there exists an orthonormal basis of principal axes in which it is diagonal. The corresponding directions are the principal axes of inertia.

None of the principal moments of inertia can exceed the sum of other two.

An asymmetrical top is when none of the principal moments of inertia are equal.

A symmetrical top is when only two of the principal moments of inertia are equal.

A spherical top is when all three of the principal moments of inertia are equal.

A rotating body-fixed frame is a coordinate system attached to the body that rotates with the body relative to an inertial (fixed) frame. The frame is characterised by its angular velocity vector Ω(t).

The time derivative in the rotating frame, d'/dt, is the derivative of the components of a vector with respect to time when expressed in the rotating (body-fixed) frame.

For any vector field A(t), its inertial-frame time derivative equals the rotating-frame derivative plus the contribution from the frame rotation: (dA/dt)_inertial = (dA/dt)_rotating + Ω × A. Here Ω is the angular velocity of the rotating frame.

For linear momentum, the relation between inertial and rotating derivatives is (dP/dt)_inertial = d'P/dt + Ω × P. So, d'P/dt + Ω × P = F which is the linear-momentum equation in the rotating frame.

For angular momentum, the relation between inertial and rotating derivatives is (dM/dt)_inertial = d'M/dt + Ω × M, and with the rotational form of Newton's law M_tot = (dM/dt)_inertial this yields d'M/dt + Ω × M = K, the angular-momentum equation in the rotating frame.

When motion is described in body-fixed principal axes (I₁, I₂, I₃ diagonal), the equations of rotational motion (Euler’s equations) are: I₁ dω₁/dt + (I₃ − I₂) ω₂ ω₃ = M₁, with cyclic permutations. M is the external torque about the centre of mass.

A rigid body can perform steady (uniform) rotation about any principal axis if the torque about that axis vanishes. Stability depends on the ordering of principal moments.

Rotations about the largest and smallest principal axes are stable under small perturbations; rotation about the intermediate axis is unstable (tennis-racket effect).

If a rigid body is confined to planar motion, its dynamics reduce to a two-dimensional problem: the inertia reduces to a scalar moment and rotation is described by a single angular velocity.

The power delivered to a rigid body by forces is P = ∑ Fᵢ ⋅ vᵢ = F_tot ⋅ V + M ⋅ ω, where F_tot is total force, V the reference point velocity, and M the torque. Translational and rotational contributions separate.

Small oscillations about a stable equilibrium orientation are governed by linearised equations obtained by expanding energy to second order in angular displacements. Normal modes and frequencies depend on inertia and restoring torques.

Define an action of the rotation and translation groups on `RigidBodyMotion`, and recover `displacement` as the composite of those group actions.

Derive the scattering cross section of a perfectly rigid sphere.

Derive the frequencies of vibaration of a symmetric linear triatomic molecule.

Show that the wave equation is invariant under rotations and any direction `s` can be rotated to `EuclideanSpace.single 2 1` if only one wave is concerned.

Show that any disturbance (subject to certain conditions) can be expressed as a superposition of harmonic plane waves via Fourier integral.

Replace the placeholder `FLRW` type with a concrete structure bundling a positive scale factor `a : Time → ℝ` (smooth, or at least twice differentiable) together with an element of `SpatialGeometry`.

Define the Hubble constant `H₀ = H(t₀)`, the present-day value of the Hubble parameter `hubbleConstant`, and the present Hubble radius `R_H = c / H₀`. Keep `parameter` (the time-dependent `H(t)`) distinct from `constant` (the number `H₀`).

Express the Hubble parameter as a function of the scale factor, `H(a)`, and of the redshift, `H(z)`, using `a = 1 / (1 + z)` with the normalization `a₀ = 1`; define the reduced Hubble function `E(z) = H(z) / H₀`.

Prove the change-of-variable relations underlying the age and distance integrals: `∂ₜ a = a * hubbleConstant a`, `dt = − dz / ((1 + z) * H)` and `dχ = c * dz / H`.

Define the conformal time `η` of an FLRW model by `a dη = dt`, that is `η(t) = ∫ dt'/a(t')`.

Define the conformal Hubble factor `ℋ = a'/a` (the prime denotes the derivative with respect to conformal time) and prove `ℋ = a * H`, relating it to the Hubble parameter `H = ∂ₜ a / a`.

State the FLRW metric in conformal time as `a(η)²` times a static metric, making its conformal flatness manifest.

State the Friedmann and acceleration equations in conformal time: `ℋ² = (8πG/3) ρ a² + (Λc²/3) a² − K c²` and `a''/a = (4πG/3)(ρ − 3 P/c²) a² + (2Λc²/3) a² − K c²`.

Prove the cosmic-to-conformal change of variables `f' = a * ∂ₜ f` (from `dt = a dη`) and use it to derive the conformal-time Friedmann and acceleration equations from their cosmic-time forms.

Define the critical density `ρ_cr = 3 H² / (8 π G)`.

Define the density parameter `Ω = ρ / ρ_cr` and the curvature density parameter `Ω_K = − K c² / (H² a²)`.

Prove the closure relation `Ω + Ω_K = 1` as a rearrangement of the Friedmann equation.

Define the reduced Hubble function `E(a) = H / H₀` and the normalized Friedmann equation `E(a)² = Σ_x Ω_{x0} f_x(a) + Ω_{K0} / a²`.

Define the Friedmann equation of the standard cosmological model `E(a)² = Ω_Λ + Ω_{m0} a⁻³ + Ω_{r0} a⁻⁴ + Ω_{K0} a⁻²`.

Define the age of the universe `t₀ = H₀⁻¹ ∫₀¹ da / (a E(a))` and prove `t₀ ∝ 1 / H₀`.

Define the radiation-matter and matter-Λ equality scale factors `a_eq = Ω_{r0} / Ω_{m0}` and `a_Λ = (Ω_{m0} / Ω_Λ)^(1/3)`.

Define the line-of-sight comoving distance `χ = c ∫ dt/a`, equivalently `χ(z) = ∫₀ᶻ c dz'/H(z')`.

Define the proper distance `D = a * χ` and prove the Hubble-Lemaître law `∂ₜ D = H * D` at fixed comoving distance `χ`.

Define the Hubble radius `R_H = c / H`, the distance at which the recession velocity equals the speed of light.

Relate the transverse comoving distance `r(χ)` to the existing `Cosmology.SpatialGeometry.S`, with curvature radius `k = 1/√|K|`.

Define the redshift by `1 + z = a₀ / a` and prove the cosmological redshift law `E ∝ 1/a` for a photon from the null geodesic equation.

Define the particle (comoving) horizon `χ_p = c ∫₀ᵗ dt'/a` and the event horizon `χ_e = c ∫_t^∞ dt'/a`.

Define the lookback time `t₀ - t` and prove its model-independent expansion `t₀ - t = H₀⁻¹ [z - ½(2 + q₀) z² + …]` in powers of the redshift.

Define the luminosity distance `d_L = (1 + z) r(χ)` and the angular-diameter distance `d_A = r(χ) / (1 + z)`.

Prove Etherington's distance-duality relation `d_L = (1 + z)² d_A`.

Prove the low-redshift expansions of `χ`, `d_L` and `d_A` in powers of `z` in terms of the deceleration parameter `q₀`.

Define the energy conditions for the cosmic perfect fluid: the null `ρ + P/c² ≥ 0`, weak `ρ ≥ 0 ∧ ρ + P/c² ≥ 0`, strong `ρ + P/c² ≥ 0 ∧ ρ + 3 P/c² ≥ 0`, and dominant `ρ ≥ 0 ∧ |P| ≤ ρ c²` energy conditions.

Prove that the expansion accelerates iff the cosmic fluid (with the cosmological constant folded in as a `w = −1` component) violates the strong energy condition: `∂ₜ ∂ₜ a > 0 ↔ ρ_tot + 3 P_tot / c² < 0`.

Prove the deceleration parameter in terms of the density parameters and equations of state, for a spatially flat universe: `q = ½ Σ_x Ω_x (1 + 3 w_x)`; in particular `q₀ = ½ Σ_x Ω_{x0} (1 + 3 w_x)`, giving `q₀ = ½ (Ω_{m0} + 2 Ω_{r0} − 2 Ω_Λ)` for ΛCDM.

Prove that a universe with `K ≤ 0`, nonnegative density and `Λ ≥ 0` expands forever: the Friedmann right-hand side stays positive, so `∂ₜ a` never vanishes, and hence `∂ₜ a > 0` at one instant implies `∂ₜ a > 0` at all later times.

Prove the existence of a Big-Bang singularity: a currently expanding, decelerating universe (`ρ > 0`, `P ≥ 0`, `Λ = 0`) reaches `a = 0` at a finite cosmic time in the past, giving a finite age `t₀ < 1 / H₀`; contrast the de Sitter case, which has no such singularity.

Define the perfect-fluid stress-energy tensor `T_{μν} = (ρ + P/c²) u_μ u_ν + P g_{μν}` for the FLRW metric.

Define the continuity equation `∂ₜ ρ + 3 H (ρ + P/c²) = 0` and derive it from the first- and second-order Friedmann equations.

Prove that the Friedmann equation, the acceleration equation and the continuity equation are not independent (a consequence of the Bianchi identity `∇_ν Gᵘᵛ = 0`).

Define the linear (barotropic) equation of state `P = w ρ c²` and prove the density scaling law `ρ = ρ₀ a^(−3(1+w))` for constant `w`.

Specialize the density scaling law to dust (`w = 0`, `ρ ∝ a⁻³`), radiation (`w = 1/3`, `ρ ∝ a⁻⁴`) and vacuum energy (`w = −1`, `ρ` constant).

Prove that the cosmological constant acts as a `w = −1` perfect fluid with `ρ_Λ = Λ c² / (8 π G)` and `P_Λ = −ρ_Λ c²`.

Prove that the de Sitter solution `a(t) = a₀ exp(±√(Λ/3) c t)` (with `ρ = 0`, `K = 0`, `Λ > 0`) solves the Friedmann equations, and that its deceleration parameter is `q = −1`.

Prove that the spatially flat radiation-dominated solution `a = (t/t₀)^(1/2)` solves the Friedmann equations, with `q₀ = 1` and `t₀ = 1 / (2 H₀)`.

Prove that the Einstein-de Sitter (spatially flat, dust) solution `a = (t/t₀)^(2/3)` solves the Friedmann equations, with `q₀ = 1/2` and `t₀ = 2 / (3 H₀)`.

Prove that the Milne solution `a = c t` (empty universe, `K < 0`) has vanishing scalar curvature, i.e. it is Minkowski space in expanding coordinates.

Define the Einstein static universe (`∂ₜ a = ∂ₜ ∂ₜ a = 0`, forcing `K > 0` and `ρ_m = 2 ρ_Λ`) and prove that it is an unstable equilibrium.

Charge density and current density should be generalized to signed measures, in such a way that they are still easy to work with and can be integrated with with tensor notation. See here: https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Maxwell's.20Equations

Prove that the magnetic field around a circular current loop is as given in the reference https://ntrs.nasa.gov/api/citations/20140002333/downloads/20140002333.pdf.

Add a constructor for DistElectromagneticPotential from electric and magnetic fields.

Write lemmas for the various properties (e.g. the electric field) of the electromagnetic potential from the various constructors.

Add results related to the differentiability of the derivative of the Electromagnetic potential.

Currently the API for the field strength tensor has the definition of `fieldStrengthMatrix`. This is now unneeded, and should be replaced with `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and suitble API around that. To undertake this TODO, it is likely easier to start building the API around `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and then remove `fieldStrengthMatrix` once the API is in place.

For the electromagnetic field strength, we have lots of lemmas related to the components of the field strength tensor in terms of the basis. For example, `toTensor_toFieldStrength_basis_repr`, these should be removed. They are used downstream, so there use there should be refactored.

For distributions, prove that the derivative fderivD commutes with integrals and sums. This may require defining the integral of families of distributions although it is expected this will follow from the definition of a distribution.

Replace the definitions of bi-linear maps in `./Mathematics/LinaerMaps` with definitions from Mathlib.

Ensure that all the lines in QuantumInfo are below 100 characters long.

Turn the `sorryful` linter on for the QuantumInfo module.

Remove all instances of `erw` within Physlib. This usually indicates the need for better API.

Refactor: Refactor the code in the QuantumInfo module to mirror the API structure of the rest of Physlib. For example, different key data structures should have their own files or directories. Results should be organized in a general way such that they can be applied more generally.

Find a way to free the environment `env` in `transverseTactics`. This leads to memory problems when using `transverseTactics` directly in loops.

The gauge group of the Georgi-Glashow model, i.e., `SU(5)`.

The homomorphism of the Standard Model gauge group into the Georgi-Glashow gauge group, i.e., the group homomorphism `SU(3) × SU(2) × U(1) → SU(5)` taking `(h, g, α)` to `blockdiag (α ^ 3 g, α ^ (-2) h)`. See page 34 of https://math.ucr.edu/home/baez/guts.pdf

The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₆SubGroup`. See page 34 of https://math.ucr.edu/home/baez/guts.pdf

The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.

The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., `SU(4) × SU(2) × SU(2)`.

The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group, i.e., the group homomorphism `SU(3) × SU(2) × U(1) → SU(4) × SU(2) × SU(2)` taking `(h, g, α)` to `(blockdiag (α h, α ^ (-3)), g, diag (α ^ 3, α ^(-3))`. See page 54 of https://math.ucr.edu/home/baez/guts.pdf

The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₃SubGroup`. See footnote 10 of https://arxiv.org/pdf/2201.07245

The group embedding from `StandardModel.GaugeGroupℤ₃` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.

The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`.

The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` with the non-trivial element `(-1, -1, -1)`. See https://math.ucr.edu/home/baez/guts.pdf

The gauge group of the Pati-Salam model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf

The group `StandardModel.gaugeGroupℤ₆SubGroup` under the homomorphism `embedSM` factors through the subgroup `gaugeGroupℤ₂SubGroup`.

The group homomorphism from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupℤ₂` induced by `embedSM`.

Remove the definitions of elements `(SM 3).Charges` B₀, B₁ etc, here are use only `B : Fin 7 → (SM 3).Charges`.

The gauge group of the Spin(10) model, i.e., the group `Spin(10)`.

The inclusion of the Pati-Salam gauge group into Spin(10), i.e., the lift of the embedding `SO(6) × SO(4) → SO(10)` to universal covers, giving a homomorphism `Spin(6) × Spin(4) → Spin(10)`. Precomposed with the isomorphism, `PatiSalam.gaugeGroupISpinEquiv`, between `SU(4) × SU(2) × SU(2)` and `Spin(6) × Spin(4)`. See page 56 of https://math.ucr.edu/home/baez/guts.pdf

The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of `embedPatiSalam` and `PatiSalam.inclSM`. See page 56 of https://math.ucr.edu/home/baez/guts.pdf

The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism from `SU(n) → Spin(2n)` discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for `n = 5`.

The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of `inclGeorgiGlashow` and `GeorgiGlashow.inclSM`.

The inclusion `inclSM` is equal to the inclusion `inclSMThruGeorgiGlashow`.

Define a general effective potential for the two Higgs doublet model, mirroring `StandardModel.HiggsField.EffectivePotential`

Define the unbroken gauge group using the Higgs field.

The gauge group `GaugeGroupI` is a Lie group.

For every `q` in `GaugeGroupQuot` the group `GaugeGroup q` is a Lie group.

The trivial principal bundle over SpaceTime with structure group `GaugeGroupI`.

A global section of `gaugeBundleI`.

Add other fermions similar to this file with the names: - UpSinglet (3, 1)_{4} (right-handed) - DownSinglet (3, 1)_{-2} (right-handed) - LeptonDoublet (1, 2)_{-3} (left-handed) - LeptonSinglet (1, 1)_{-6} (right-handed)

Improve the efficiency of `mem_repGaugeGroupI_ker_iff_eq` by removing the `grind`s and replacing them with a more direct argument.

Change the action of `GaugeGroupI` on `HiggsVec` to be a representation rather than a `MulAction`.

The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the stability group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the `SU(3) × U(1)` subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` with the embedding given by `(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`.

The subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` which preserves every `HiggsVec` by the action of `StandardModel.HiggsVec.rep` is given by `SU(3) × ℤ₆` where `ℤ₆` is the subgroup of `SU(2) × U(1)` with elements `(α^(-3) * I₂, α)` where `α` is a sixth root of unity.

Make `HiggsBundle` an associated bundle.

Define the global gauge action on HiggsField.

Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)

Prove invariance of potential under global gauge action.

The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`.

There exists a `g` in `gaugeTransformI` such that `gaugeAction g φ = φ'` iff `φ(x)^† φ(x) = φ'(x)^† φ'(x)`.

For every smooth map `f` from `SpaceTime` to `ℝ` such that `f` is positive semidefinite, there exists a Higgs field `φ` such that `f = φ^† φ`.

Define a CoeFun instance for the Higgs Potential (or similar), instead of relying on `P.toFun`.

When there is no quartic coupling, the potential is bounded iff the mass squared is non-positive, i.e., for `P : Potential` then `P.IsBounded` iff `P.μ2 ≤ 0`. That is to say `- P.μ2 * ‖φ‖_H^2 x` is bounded below iff `P.μ2 ≤ 0`.

Define a structure capturing the fermionic content of the Standard Model, with all fermions expressed as left-handed Weyl fermions (`Fermion.LeftHandedWeyl`) and including all three families. The structure should carry a `Module ℂ` instance together with a representation of the Lorentz group and a representation of the global gauge group `GaugeGroupI` (built from `repU1` and `fundamentalSU2`).

Make the result `viableChargesMultiset` a safe definition, that is to say proof that the recursion terminates.

Anomaly cancellation conditions can be derived formally from the gauge group and fermionic representations using e.g. topological invariants. Include such a definition.

Anomaly cancellation conditions can be defined using algebraic varieties. Link such an approach to the approach here.

Split the following two lemmas up into smaller parts.

The lemma `bosonicProjF_mem_ideal` has a proof which is really long. We should either 1) split it up into smaller lemmas or 2) Put more comments into the proof.

The implementation of pure U(1) anomaly cancellation conditions is done currently through the type `ACCSystemCharges`. This whole directory could be simplified by refactoring to remove `ACCSystemCharges` defining `PureU1Charges` as `Fin n → ℚ` directly, or this space quotiented by permutations and overall factors.

Define a smooth structure on `FiniteTarget`.

The Hamiltonian for the free particle is essentially self-adjoint. This follows immediately from the ess. self-adjointness of the momentum-square operator.

The free particle as a quantum system (self-adjoint Hamiltonian acting on a Hilbert space).

Define `HarmonicOscillator` as a structure extending `SpaceDQuantumSystem` (c.f. `Hydrogen.Basic.lean` for an example). In general the potential is determined by a positive-definite, real symmetric matrix `V = ½m(xᵗ·A·x)`. Note that such matrices can always be diagonalized so perhaps it suffices to take `A` diagonal. A special case with enhanced symmetry is the isotropic harmonic oscillator with `A = ω²·𝕀`.

Define the raising/lowering/number operators for the quantum harmonic oscillator.

Prove the commutation relations for the raising/lowering/number/Hamiltonian operators of the quantum harmonic oscillator.

Determine the spectrum of the quantum harmonic oscillator in terms of the eigenvalues of the matrix `A ≻ 0` appearing in the potential.

Determine the energy eigenstates of the quantum harmonic oscillator in the 'Cartesian basis' in terms of Hermite polynomials.

Determine the energy eigenstates of the isotropic quantum harmonic oscillator in the 'spherical basis' in terms of spherical harmonics.

Generalize 1d harmonic oscillator to d dimensions and SpaceDHilbertSpace.

To match this with the results currently in the `QuantumInfo` part of the library, we should: 1. Define `FiniteHilbertSpace` as a structure with a single entry `val`, this should take as an input a finite and decidable type `d`. Below this type is taken as default to be `Fin n`. 2. On this type we should then define the structure of an inner-product space, and a Hilbert space. 3. We could then define the notation `𝓗[d]` to denote the Hilbert space corresponding to the type `d`. 4. The results from `QuantumInfo/Finite/Braket.lean` can then be moved over to Physlib, and related to the definition of the Hilbert space here. Optional. Maybe it is worth moving these files to a directory called `States`, with the idea that it includes this definition of the Hilbert space, the definition of bras and kets, and the definition of mixed states. Maybe also parts of `./ResourceTheory/FreeState`.

Remove 1d Hilbert space once dependencies are moved over to SpaceDHilbertSpace.

Generalize Gaussian states to d dimensions and SpaceDHilbertSpace.

Generalize plane waves to d dimensions and SpaceDHilbertSpace.

Generalize position states to d dimensions and SpaceDHilbertSpace.

Remove 1d Schwartz submodule once dependencies are all generalized to SpaceDHilbertSpace.

Generalize density of PolyBddSchwartzSubmodule to more general measures than just μ ≤ volume.

Prove that the Hydrogen Hamiltonian is _not_ essentially self-adjoint for `d < 3`.

Prove that the Hydrogen Hamiltonian is essentially self-adjoint for `d ≥ 3`.

Prove that (the closure of) the Hydrogen Hamiltonian has eigenvalues (point spectrum) {-½mk²ℏ⁻² / (n + ½(d - 1))² | n ∈ ℕ}. These correspond to the bound states.

Prove that (the closure of) the Hydrogen Hamiltonian has continuous spectrum [0,∞). These correspond to scattering states.

Define the Rydberg formula and Lyman, Balmer, Paschen, etc. series.

Determine the wavelengths / frequencies of the Lyman, Balmer, Paschen, etc. series.

Analyze the Zeeman effect using first-order degenerate perturbation theory.

Analyze the Stark effect using first-order degenerate perturbation theory.

The Hamiltonian for the infinite square well is `(2m)⁻¹momentumSqOperator` with respect to `InfiniteSquareWell.measure`. This requires first generalizing `momentumSqOperator` to `Space d` measures other than `volume`.

The Hamiltonian for the infinite square well is essentially self-adjoint.

The particle in an infinite square well as a quantum system (self-adjoint Hamiltonian acting on a Hilbert space).

Give an example of a closed, symmetric operator with _no_ self-adjoint extension. The canonical example is the derivative operator `T = -i d/dx` on the half-space [0,∞) with domain `D(T) = {ψ ∈ L²([0,∞), ℂ) | ψ(0) = 0}` (or a d-dimensional generalization).

Give an example of a densely defined, closed operator `T` such that each complex number is an eigenvalue of `T†` but `T` has no eigenvalues: c.f. Schmüdgen Ch 2, exercise 9.

Give an example of a symmetric operator `T` on `H` such that `(T + I • 1).range` and `(T - I • 1).range` are dense in `H` but `T` is not essentially self-adjoint. c.f. Schmüdgen Ch 3, exercise 12.

Extend the domain of the momentum operator to the Sobolev space `H¹`.

Prove that the momentum operator is self-adjoint (relies on 15310236534648318597).

Prove that the spectrum of the multiplication operator `𝓜 μ f` is the 'μ-essential range' of `f`.

Prove that the spectrum of the multiplication operator `𝓜 μ f` is the closure of `f.range` for continuous `f`.

Move spectral theory definitions and lemmas over to Mathlib equivalents if/when available.

Prove that `IsStarNormal (T : H →ₗ.[ℂ] H)` is equivalent to `T.domain = T†.domain` and `‖T x‖ = ‖T† x‖` for all `x ∈ T.domain`.

Prove basic properties of `IsStarNormal (T : H →ₗ.[ℂ] H)`, paralleling those for `IsSelfAdjoint (T : H →ₗ.[ℂ] H)`.

Refactor to use `SpaceDHilbertSpace 1`.

Refactor to use `QuantumMechanics.PlanckConstant`.

`{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ`. Proof: expand `contrBispinorDown` and use fact that metrics contract to the identity.

`{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ`. proof: expand `coBispinorDown` and use fact that metrics contract to the identity.

Prove injectivity of ofCliffordAlgebra and construct the full isomorphism.

The linear equivalence between `rightHandedWeyl` and `DualRightHandedWeyl` given by multiplying an element of `rightHandedWeyl` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`.

The linear equivalence `rightHandedWeylDualEquiv` is equivariant with respect to the action of `SL(2,C)` on `rightHandedWeyl` and `DualRightHandedWeyl`.

Define the Lie group structure on the Lorentz group.

Prove topological properties of the Orthochronous Lorentz Group.

The restricted Lorentz group is connected.

Find the conditions for which the age gap for the twin paradox is zero.

In the twin paradox with instantaneous acceleration, Twin A is always older then Twin B.

Do the twin paradox with a non-instantaneous acceleration. This should be done in a different module.

Extend `complexLorentzTensor` to a `ConjTensorSpecies`.

Extend `realLorentzTensor` to a `ConjTensorSpecies`.

Prove lemmas relating to the commutation rules of `dropPair` and `prodP`.

Choose a more descriptive name for `evalT` and `evalP`, taking into consideration the namespaces they live in.

Add lemmas related to the interaction of evalT and permT, prodT and contrT.

Add the lemma corresponding the the commutation of two evaluations of tensor indices.

Add a lemma similar to `contrT_evalT` except with the contraction and evaluation the other way around.

Add a lemmas related to the commutation of evaluation with contraction.

The contractions done here use the relativistic Levi-Civita tensor `ε4` but treat it as a Euclidean tensor. We should define a euclidean form of the Levi-Civita tensor and prove replace the results here with theorems about that tensor.

Replace Lorentz.ContrMod and Lorentz.CoMod in the definition of realLorentzTensor directly with Lorentz.Vector and Lorentz.Covector, and representations defined on them.

In a similar way to `Vector.contract` and `CoVector.contract`, we want to define metrics and units as intertwining maps of representations. This should copy (and eventually replace) the definitions e.g. `./Units/Pre.lean`.

Include in the condition of `TensorSpecies` a relationship between the metrics and the basis vectors.

A simplification of the `entropy` of the two-state canonical ensemble.

A simplification of the `helmholtzFreeEnergy` of the two-state canonical ensemble.

There is a different version of the Stienspring dilation in `QuantumInfo.Channels.CPTP`. We should unify the the version here with that one. Some of the definitions here are more general then the ones in `QuantumInfo` as they do not restrict to `ℂ`. This is something we should modify in `QuantumInfo`.

Make the version of the derivative described through `deriv_eq_mfderiv_manifoldStructure` the definition of `deriv` and prove the equivalence with the current definition, under suitable conditions.

Generalize the statement that a div-free field is a curl to time-dependent fields.

Generalize the statement that a curl-free field is a gradient to time-dependent fields.

SpaceTime should be refactored into a structure, or similar, to prevent casting.

The function `space` is equivariant with respect to rotations.

The results in this file are currently stated, but not proved. They should should be proved following e.g. https://arxiv.org/pdf/1504.05593. This is a large project.

Make SI : UnitChoices computable, probably by replacing the axioms defining the units. See here: https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/physical.20units/near/534914807

Induce further non-additive algebraic, additional order, and topological instances on `WithDim d M` from instances on `M`.

Improve the module doc-string of the `Qubit` file, to explain the current implementation.