TODO list
This TODO list is automatically created from the Lean files. It contains a number of different types of TODO items:Informal definition
Corresponds to a definition given as an English string which needs formalizing.Informal Lemma
Corresponds to a lemma given as an English string which needs formalizing.Semiformal result
Corresponds to a result which the declaration of the result is formalized, but the proof or definition itself is not.Sorryful result
Corresponds to a result containing `sorry`. These are the easiest place to start.TODO Item
Corresponds to a general TODO item.
Classical Mechanics ⚙️
Hide 15 TODO items:
Sorryful result
(file : ClassicalMechanics.HarmonicOscillator.force)The force of the classical harmonic oscillator defined as - dU(x)/dx where U(x)
is the potential energy.
Sorryful result
(file : ClassicalMechanics.HarmonicOscillator.force_is_linear)The force on the classical harmonic oscillator is - k x.
Sorryful result
(file : ClassicalMechanics.HarmonicOscillator.EquationOfMotion)The definition of the equation of motion for the classical harmonic oscillator defined through the Euler-Lagrange equations.
See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.EquationOfMotionSorryful result
(file : ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_newtons_second_law)The equations of motion are satisfied if and only if Newton’s second law holds.
See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_newtons_second_lawSorryful result
(file : ClassicalMechanics.HarmonicOscillator.ExtremaOfAction)The proposition on a trajectory which is true if that trajectory is an extrema of the action.
semiformal implmentation notes:
- This is not expected to be easy to define.
Sorryful result
(file : ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_extremaOfAction)A trajectory x : ℝ → ℝ satsifies the equation of motion if and only if
it is an extrema of the action.
Implementation note: This result depends on other semi-formal results which will need defining before this.
See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_extremaOfActionTODO Item
(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Basic)Create a new folder for the damped harmonic oscillator, initially as a place-holder.
See on GitHub Tag: 6VZHCTODO Item
(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)Implement other initial condtions. For example:
- initial conditions at a given time.
- Two positions at different times.
- Two velocities at different times.
And convert them into the type
InitialConditionsabove (which may need generalzing a bit to make this possible).
TODO Item
(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)For the classical harmonic oscillator find the time for which it returns to it’s initial position and velocity.
See on GitHub Tag: 6VZI3TODO Item
(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)For the classical harmonic oscillator find the times for which it passes through zero.
See on GitHub Tag: 6VZJBTODO Item
(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)For the classical harmonic oscillator find the velocity when it passes through zero.
See on GitHub Tag: 6VZJHSorryful result
(file : ClassicalMechanics.HarmonicOscillator.sol_equationOfMotion)The solutions for any initial condition solve the equation of motion.
See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.sol_equationOfMotionSorryful result
(file : ClassicalMechanics.HarmonicOscillator.sol_unique)The solutions to the equation of motion for a given set of initial conditions are unique.
Semiformal implmentation:
- One may needed the added condition of smoothness on
xhere. EquationOfMotionneeds defining before this can be proved.
TODO Item
(file : PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave)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 concerened.
TODO Item
(file : PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave)Show that any disturbance (subject to certian conditions) can be expressed as a superposition of harmonic plane waves via Fourier integral.
See on GitHub Tag: EGU3ECondensed Matter 🧊
Hide 3 TODO items:
TODO Item
(file : PhysLean.CondensedMatter.TightBindingChain.Basic)Prove results related to the one-dimensional tight binding chain. This is related to the following issue/feature-request: https://github.com/HEPLean/PhysLean/issues/523
See on GitHub Tag: BBZABSorryful result
(file : CondensedMatter.TightBindingChain.hamiltonian_hermitian)The hamiltonian of the tight binding chain is hermitian.
See on GitHub Tag: CondensedMatter.TightBindingChain.hamiltonian_hermitianSorryful result
(file : CondensedMatter.TightBindingChain.energyEigenstate_orthogonal)The energy eigenstates of the tight binding chain are orthogonal.
See on GitHub Tag: CondensedMatter.TightBindingChain.energyEigenstate_orthogonalCosmology 🌌
Hide 10 TODO items:
Sorryful result
(file : Cosmology.SpatialGeometry)The inductive type with three constructors:
Spherical (k : ℝ)FlatSaddle (k : ℝ)
Sorryful result
(file : Cosmology.SpatialGeometry.S)For s corresponding to
Spherical k,S s r = k * sin (r / k)Flat,S s r = r,Saddle k,S s r = k * sin (r / k).
Semiformal implementation note: There is likely a better name for this function.
See on GitHub Tag: Cosmology.SpatialGeometry.SInformal Lemma
(Cosmology.SpatialGeometry.limit_S_saddle)The limit of S (Saddle k) r as k → ∞ is equal to S (Flat) r.
Informal Lemma
(Cosmology.SpatialGeometry.limit_S_sphere)The limit of S (Sphere k) r as k → ∞ is equal to S (Flat) r.
Sorryful result
(file : Cosmology.FLRW)The structure FLRW is defined to contain the physical parameters of the Friedmann-Lemaître-Robertson-Walker metric. That is, it contains
- The scale factor
a(t) - An element of
SpatialGeometry.
Semiformal implementation note: It is possible that we should restirct
a(t) to be smooth or at least twice differentiable.
Informal definition
(Cosmology.FLRW.hubbleConstant)The hubble constant defined in terms of the scale factor
as (dₜ a) / a.
The notation H is used for the hubbleConstant.
Semiformal implementation note: Implement also scoped notation.
See on GitHub Tag: 6Z2NBInformal definition
(Cosmology.FLRW.decelerationParameter)The deceleration parameter defined in terms of the scale factor
as - (dₜdₜ a) a / (dₜ a)^2.
The notation q is used for the decelerationParameter.
Semiformal implementation note: Implement also scoped notation.
See on GitHub Tag: 6Z2UEInformal Lemma
(Cosmology.FLRW.decelerationParameter_eq_one_plus_hubbleConstant)The deceleration parameter is equal to - (1 + (dₜ H)/H^2).
Informal Lemma
(Cosmology.FLRW.time_evolution_hubbleConstant)The time evolution of the hubble parameter is equal to dₜ H = - H^2 (1 + q).
Informal Lemma
(Cosmology.FLRW.hubbleConstant_decrease_iff)There exists a time at which the hubble constant decreases if and only if
there exists a time where the deceleration parameter is less then -1.
Electromagnetism ⚡
Hide 5 TODO items:
TODO Item
(file : PhysLean.Electromagnetism.Basic)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-PhysLean/topic/Maxwell’s.20Equations
See on GitHub Tag: 6V2UZTODO Item
(file : PhysLean.Electromagnetism.FieldStrength.Basic)Define the dual field strength.
See on GitHub Tag: 6V2OUSorryful result
(file : Electromagnetism.lorentzAction)The Lorentz action on the electric and magnetic fields.
See on GitHub Tag: Electromagnetism.lorentzActionSorryful result
(file : Electromagnetism.toElectricMagneticField_equivariant)The equivalence toElectricMagneticField is equivariant with respect to the
group action.
TODO Item
(file : PhysLean.Electromagnetism.MaxwellEquations)Show that if the charge density is spherically symmetric, then the electric field is also spherically symmetric.
See on GitHub Tag: 6V2VDMathematics ➗
Hide 4 TODO items:
TODO Item
(file : PhysLean.Mathematics.FDerivCurry)Replace following helper lemmas with fun_prop after #24056 in Mathlib has gone through.
See on GitHub Tag: AZ2QNTODO Item
(file : PhysLean.Mathematics.LinearMaps)Replace the definitions in this file with Mathlib definitions.
See on GitHub Tag: 6VZLZSorryful result
(file : fundamental_theorem_of_variational_calculus')The assumption IsTestFunction f in fundamental_theorem_of_variational_calculus can be
weakened to Continuous f.
The proof is by contradiction, assume that there is x₀ such that f x₀ then you can easily
construct g test function with support on the neighborhood of x₀ such that ⟪f x, g x⟫ ≥ 0.
Meta 🏛️
Hide 1 TODO items:
TODO Item
(file : PhysLean.Meta.TransverseTactics)Find a way to free the environment env in transverseTactics.
This leads to memory problems when using transverseTactics directly in loops.
Optics 🔍
Hide 0 TODO items:
Particles 💥
Hide 49 TODO items:
Informal definition
(GeorgiGlashow.GaugeGroupI)The gauge group of the Georgi-Glashow model, i.e., SU(5).
Informal definition
(GeorgiGlashow.inclSM)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
See on GitHub Tag: 6V2WSInformal Lemma
(GeorgiGlashow.inclSM_ker)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
See on GitHub Tag: 6V2W2Informal definition
(GeorgiGlashow.embedSMℤ₆)The group embedding from StandardModel.GaugeGroupℤ₆ to GaugeGroupI induced by inclSM by
quotienting by the kernel inclSM_ker.
Informal definition
(PatiSalam.GaugeGroupI)The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., SU(4) × SU(2) × SU(2).
Informal definition
(PatiSalam.inclSM)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
See on GitHub Tag: 6V2RHInformal Lemma
(PatiSalam.inclSM_ker)The kernel of the map inclSM is equal to the subgroup StandardModel.gaugeGroupℤ₃SubGroup.
See footnote 10 of https://arxiv.org/pdf/2201.07245
See on GitHub Tag: 6V2RQInformal definition
(PatiSalam.embedSMℤ₃)The group embedding from StandardModel.GaugeGroupℤ₃ to GaugeGroupI induced by inclSM by
quotienting by the kernel inclSM_ker.
Informal definition
(PatiSalam.gaugeGroupISpinEquiv)The equivalence between GaugeGroupI and Spin(6) × Spin(4).
Informal definition
(PatiSalam.gaugeGroupℤ₂SubGroup)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
See on GitHub Tag: 6V2SGInformal definition
(PatiSalam.GaugeGroupℤ₂)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
See on GitHub Tag: 6V2SMInformal Lemma
(PatiSalam.sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup)The group StandardModel.gaugeGroupℤ₆SubGroup under the homomorphism embedSM factors through
the subgroup gaugeGroupℤ₂SubGroup.
Informal definition
(PatiSalam.embedSMℤ₆Toℤ₂)The group homomorphism from StandardModel.GaugeGroupℤ₆ to GaugeGroupℤ₂ induced by embedSM.
TODO Item
(file : PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane)Remove the definitions of elements (SM 3).Charges B₀, B₁ etc, here are
use only B : Fin 7 → (SM 3).Charges.
Informal definition
(Spin10Model.GaugeGroupI)The gauge group of the Spin(10) model, i.e., the group Spin(10).
Informal definition
(Spin10Model.inclPatiSalam)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
See on GitHub Tag: 6V2YGInformal definition
(Spin10Model.inclSM)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
See on GitHub Tag: 6V2YOInformal definition
(Spin10Model.inclGeorgiGlashow)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.
Informal definition
(Spin10Model.inclSMThruGeorgiGlashow)The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of
inclGeorgiGlashow and GeorgiGlashow.inclSM.
Informal Lemma
(Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow)The inclusion inclSM is equal to the inclusion inclSMThruGeorgiGlashow.
TODO Item
(file : PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic)Within the definition of the 2HDM potential. The structure Potential should be
renamed to TwoHDM and moved out of the TwoHDM namespace.
Then toFun should be renamed to potential.
TODO Item
(file : PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic)Prove bounded properties of the 2HDM potential. See e.g. https://inspirehep.net/literature/201299 and https://arxiv.org/pdf/hep-ph/0605184.
See on GitHub Tag: 6V2UDInformal Lemma
(TwoHDM.prodMatrix_invariant)The map prodMatrix is invariant under the simultaneous action of gaugeAction on the two
Higgs fields.
Informal Lemma
(TwoHDM.prodMatrix_to_higgsField)Given any smooth map f from spacetime to 2-by-2 complex matrices landing on positive
semi-definite matrices, there exist smooth Higgs fields Φ1 and Φ2 such that f is equal to
prodMatrix Φ1 Φ2.
See https://arxiv.org/pdf/hep-ph/0605184
See on GitHub Tag: 6V2V2TODO Item
(file : PhysLean.Particles.StandardModel.Basic)Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆.
See on GitHub Tag: 6V2FPSorryful result
(file : StandardModel.gaugeGroupℤ₆SubGroup)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 elements (α^2 * I₃, α^(-3) * I₂, α),
where α is a sixth complex root of unity.
See https://math.ucr.edu/home/baez/guts.pdf
See on GitHub Tag: StandardModel.gaugeGroupℤ₆SubGroupSorryful result
(file : StandardModel.GaugeGroupℤ₆)The smallest possible gauge group of the Standard Model, i.e., the quotient of GaugeGroupI by
the ℤ₆-subgroup gaugeGroupℤ₆SubGroup.
See https://math.ucr.edu/home/baez/guts.pdf
See on GitHub Tag: StandardModel.GaugeGroupℤ₆Informal definition
(StandardModel.gaugeGroupℤ₂SubGroup)The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on all particles in the
standard model, i.e., the ℤ₂-subgroup of GaugeGroupI derived from the ℤ₂ subgroup of
gaugeGroupℤ₆SubGroup.
See https://math.ucr.edu/home/baez/guts.pdf
See on GitHub Tag: 6V2GHInformal definition
(StandardModel.GaugeGroupℤ₂)The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of GaugeGroupI by
the ℤ₂-subgroup gaugeGroupℤ₂SubGroup.
See https://math.ucr.edu/home/baez/guts.pdf
See on GitHub Tag: 6V2GOInformal definition
(StandardModel.gaugeGroupℤ₃SubGroup)The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on all particles in the
standard model, i.e., the ℤ₃-subgroup of GaugeGroupI derived from the ℤ₃ subgroup of
gaugeGroupℤ₆SubGroup.
See https://math.ucr.edu/home/baez/guts.pdf
See on GitHub Tag: 6V2GVInformal definition
(StandardModel.GaugeGroupℤ₃)The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of GaugeGroupI by
the ℤ₃-subgroup gaugeGroupℤ₃SubGroup.
See https://math.ucr.edu/home/baez/guts.pdf
See on GitHub Tag: 6V2G3Informal definition
(StandardModel.GaugeGroup)The (global) gauge group of the Standard Model given a choice of quotient, i.e., the map from
GaugeGroupQuot to Type which gives the gauge group of the Standard Model for a given choice of
quotient.
See https://math.ucr.edu/home/baez/guts.pdf
See on GitHub Tag: 6V2HFInformal Lemma
(StandardModel.gaugeGroupI_lie)The gauge group GaugeGroupI is a Lie group.
Informal Lemma
(StandardModel.gaugeGroup_lie)For every q in GaugeGroupQuot the group GaugeGroup q is a Lie group.
Informal definition
(StandardModel.gaugeBundleI)The trivial principal bundle over SpaceTime with structure group GaugeGroupI.
Informal definition
(StandardModel.gaugeTransformI)A global section of gaugeBundleI.
TODO Item
(file : PhysLean.Particles.StandardModel.HiggsBoson.Basic)Make HiggsBundle an associated bundle.
Informal Lemma
(StandardModel.HiggsField.zero_is_zero_section)The zero Higgs field is the zero section of the Higgs bundle, i.e., the HiggsField zero
defined by ofReal 0 is the constant zero-section of the bundle HiggsBundle.
TODO Item
(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)Currently this only contains the action of the global gauge group. Generalize to include the full action of the gauge group.
See on GitHub Tag: 6V2LJInformal Lemma
(StandardModel.HiggsVec.guage_orbit)There exists a g in GaugeGroupI such that rep g φ = φ' iff ‖φ‖ = ‖φ'‖.
Informal Lemma
(StandardModel.HiggsVec.stability_group_single)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 θ}).
Informal Lemma
(StandardModel.HiggsVec.stability_group)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.
TODO Item
(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)Define the global gauge action on HiggsField.
See on GitHub Tag: 6V2MVTODO Item
(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)Prove ⟪φ1, φ2⟫_H invariant under the global gauge action. (norm_map_of_mem_unitary)
TODO Item
(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)Prove invariance of potential under global gauge action.
See on GitHub Tag: 6V2NAInformal definition
(StandardModel.HiggsField.gaugeAction)The action of gaugeTransformI on HiggsField acting pointwise through HiggsVec.rep.
Informal Lemma
(StandardModel.HiggsField.guage_orbit)There exists a g in gaugeTransformI such that gaugeAction g φ = φ' iff
φ(x)^† φ(x) = φ'(x)^† φ'(x).
Informal Lemma
(StandardModel.HiggsField.gauge_orbit_surject)For every smooth map f from SpaceTime to ℝ such that f is positive semidefinite, there
exists a Higgs field φ such that f = φ^† φ.
Informal Lemma
(StandardModel.HiggsField.Potential.isBounded_iff_of_𝓵_zero)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.
QFT 🌊
Hide 10 TODO items:
TODO Item
(file : PhysLean.QFT.AnomalyCancellation.Basic)Anomaly cancellation conditions can be derived formally from the gauge group and fermionic representations using e.g. topological invariants. Include such a definition.
See on GitHub Tag: 6VZMWTODO Item
(file : PhysLean.QFT.AnomalyCancellation.Basic)Anomaly cancellation conditions can be defined using algebraic varieties. Link such an approach to the approach here.
See on GitHub Tag: 6VZM3TODO Item
(file : PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder)Split the following two lemmas up into smaller parts.
See on GitHub Tag: 6V2JJTODO Item
(file : PhysLean.QFT.PerturbationTheory.WickAlgebra.Basic)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.
Sorryful result
(file : WickContraction.Perm.isFull_of_isFull)If Perm φsΛ₁ φsΛ₂ then if φsΛ₁ is a full Wick contraction
then φsΛ₂ is a full Wick contraction..
Implementation note: Please contact JTS before attempting this.
See on GitHub Tag: WickContraction.Perm.isFull_of_isFullSorryful result
(file : WickContraction.Perm.perm_uncontractedList)If Perm φsΛ₁ φsΛ₂ then the uncontracted lists of
φsΛ₁ and φsΛ₂ are permutations of each other.
TODO Item
(file : PhysLean.QFT.QED.AnomalyCancellation.BasisLinear)The definition of coordinateMap here may be improved by replacing
Finsupp.equivFunOnFinite with Finsupp.linearEquivFunOnFinite. Investigate this.
TODO Item
(file : PhysLean.QFT.QED.AnomalyCancellation.Even.BasisLinear)Replace the definition of join with a Mathlib definition, most likely Sum.elim.
TODO Item
(file : PhysLean.QFT.QED.AnomalyCancellation.Odd.BasisLinear)Replace the definition of join with a Mathlib definition, most likely Sum.elim.
TODO Item
(file : PhysLean.QFT.QED.AnomalyCancellation.Permutations)Remove pairSwap, and use the Mathlib defined function Equiv.swap instead.
Quantum Mechanics ⚛️
Hide 4 TODO items:
TODO Item
(file : PhysLean.QuantumMechanics.FiniteTarget.Basic)Make FiniteTarget basis independent, i.e. use a linear map for
the hamiltonian instead of a matrix.
TODO Item
(file : PhysLean.QuantumMechanics.FiniteTarget.Basic)Define a smooth structure on FiniteTarget.
TODO Item
(file : PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic)The momentum operator should be moved to a more general file.
See on GitHub Tag: 6VZH3TODO Item
(file : PhysLean.QuantumMechanics.OneDimension.Operators.Momentum)Make API connecting the momentumOperator to momentumOperatorLinearPMap
for one-dimensional QM.
Relativity ⏳
Hide 30 TODO items:
Informal Lemma
(complexLorentzTensor.contrBispinorUp_eq_metric_contr_contrBispinorDown){contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ.
Proof: expand contrBispinorDown and use fact that metrics contract to the identity.
Informal Lemma
(complexLorentzTensor.coBispinorUp_eq_metric_contr_coBispinorDown){coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ.
proof: expand coBispinorDown and use fact that metrics contract to the identity.
TODO Item
(file : PhysLean.Relativity.CliffordAlgebra)Prove algebra generated by gamma matrices is isomorphic to Clifford algebra.
See on GitHub Tag: 6VZF2TODO Item
(file : PhysLean.Relativity.LorentzAlgebra.Basis)Define the standard basis of the Lorentz algebra.
See on GitHub Tag: 6VZKATODO Item
(file : PhysLean.Relativity.LorentzGroup.Basic)Define the Lie group structure on the Lorentz group.
See on GitHub Tag: 6VZHMSorryful result
(file : LorentzGroup.generalizedBoost_timeComponent_eq)The time component of a generalised boost is equal to
1 +
‖u.1.timeComponent • v.1.spatialPart - v.1.timeComponent • u.1.spatialPart‖ / (1 + ⟪u.1, v.1⟫ₘ)
A proof of this result can be found at the below link: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Lorentz.20group/near/523249684
Note that the decleration of this semiformal result will be similar once
the TODO item FXQ45 is completed.
TODO Item
(file : PhysLean.Relativity.LorentzGroup.Orthochronous.Basic)Prove topological properties of the Orthochronous Lorentz Group.
See on GitHub Tag: 6VZLOTODO Item
(file : PhysLean.Relativity.LorentzGroup.Restricted.Basic)Prove that every member of the restricted Lorentz group is combiniation of a boost and a rotation.
See on GitHub Tag: 6VZNPSemiformal result
(restricted_isConnected)The restricted Lorentz group is connected.
See on GitHub Tag: FXNL5Informal Lemma
(Lorentz.SL2C.toRestrictedLorentzGroup)The homomorphism from SL(2, ℂ) to the restricted Lorentz group.
TODO Item
(file : PhysLean.Relativity.SL2C.Basic)Define homomorphism from SL(2, ℂ) to the restricted Lorentz group.
TODO Item
(file : PhysLean.Relativity.Special.TwinParadox.Basic)Find the conditions for which the age gap for the twin paradox is zero.
See on GitHub Tag: 6V2UQInformal Lemma
(SpecialRelativity.InstantaneousTwinParadox.ageGap_nonneg)In the twin paradox with instantous acceleration, Twin A is always older then Twin B.
See on GitHub Tag: 7ROVETODO Item
(file : PhysLean.Relativity.Special.TwinParadox.Basic)Do the twin paradox with a non-instantaneous acceleration. This should be done in a different module.
See on GitHub Tag: 7ROQ4TODO Item
(file : PhysLean.Relativity.Tensors.Basic)We want to add inv_perserve_color to Simp database, however this fires the linter
simpVarHead. This should be investigated.
TODO Item
(file : PhysLean.Relativity.Tensors.Basic)Prove that if σ satifies PermCond c c1 σ then PermCond.inv σ h
satifies PermCond c1 c (PermCond.inv σ h).
TODO Item
(file : PhysLean.Relativity.Tensors.Color.Basic)In the definition equivToHomEq the tactic try {simp; decide}; try decide
can probably be made more efficent.
Informal definition
(IndexNotation.OverColor.forgetLift)The natural isomorphism between lift (C := C) ⋙ forget and
Functor.id (Discrete C ⥤ Rep k G).
Informal definition
(Fermion.rightHandedWeylAltEquiv)The linear equivalence between rightHandedWeyl and altRightHandedWeyl given by multiplying
an element of rightHandedWeyl by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].
Informal Lemma
(Fermion.rightHandedWeylAltEquiv_equivariant)The linear equivalence rightHandedWeylAltEquiv is equivariant with respect to the action of
SL(2,C) on rightHandedWeyl and altRightHandedWeyl.
TODO Item
(file : PhysLean.Relativity.Tensors.Contraction.Pure)Prove lemmas relating to the commutation rules of dropPair and prodP.
TODO Item
(file : PhysLean.Relativity.Tensors.Evaluation)Add lemmas related to the interaction of evalT and permT, prodT and contrT.
See on GitHub Tag: 6VZ6GTODO Item
(file : PhysLean.Relativity.Tensors.Product)Change products of tensors to use Fin.append rather then
Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm.
TODO Item
(file : PhysLean.Relativity.Tensors.Product)Determine in prodEquiv_symm_pure why in rw (transparency := .instances) [h1]
(transparency := .instances) is needed. As a first step adding this as a comment here.
TODO Item
(file : PhysLean.Relativity.Tensors.RealTensor.Derivative)Prove that the derivative obeys the following equivariant
property with respect to the Lorentz group.
For a function f : ℝT(d, cm) → ℝT(d, cn) then
Λ • (∂ f (x)) = ∂ (fun x => Λ • f (Λ⁻¹ • x)) (Λ • x).
Sorryful result
(file : realLorentzTensor.toComplex_equivariant)The map toComplex is equivariant.
Informal Lemma
(realLorentzTensor.permT_toComplex)The map toComplex commutes with permT.
Informal Lemma
(realLorentzTensor.prodT_toComplex)The map toComplex commutes with prodT.
Informal Lemma
(realLorentzTensor.contrT_toComplex)The map toComplex commutes with contrT.
Informal Lemma
(realLorentzTensor.evalT_toComplex)The map toComplex commutes with evalT.
String Theory 🧵
Hide 0 TODO items:
Statistical Mechanics 🎲
Hide 11 TODO items:
Sorryful result
(file : CanonicalEnsemble.partitionFunction_nsmul)The partition function of n copies of a canonical ensemble.
Sorryful result
(file : CanonicalEnsemble.probability_le_one)Probability of a microstate in a canonical ensemble is less then or equal to 1.
Sorryful result
(file : CanonicalEnsemble.probability_nonneg)Probability of a microstate in a canonical ensemble is non-negative.
See on GitHub Tag: CanonicalEnsemble.probability_nonnegSorryful result
(file : CanonicalEnsemble.probability_nsmul)The probability of a microstate in n copies of a canonical ensemble is
equal to the product of the probability of the corresponding individual microstates.
Sorryful result
(file : CanonicalEnsemble.meanEnergy_nsmul)The mean energy of n copies of a canonical ensemble is equal
to n times the mean energy of the canonical ensemble.
Note, can’t make this SMul since the target type depends on the
value of n.
Sorryful result
(file : CanonicalEnsemble.entropy_nsmul)The entropy of n copies of a canonical ensemble is equal
to n times the entropy of the canonical ensemble.
Sorryful result
(file : CanonicalEnsemble.helmholtzFreeEnergy_nsmul)The free energy of n copies of a canonical ensemble is equal
to n times the entropy of the canonical ensemble.
TODO Item
(file : PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState)Generalize the results for the two-state canonical ensemble so that the two
states have arbitary energies, rather than one state having energy 0.
Informal Lemma
(CanonicalEnsemble.twoState_entropy_eq)A simplification of the entropy of the two-state canonical ensemble.
Informal Lemma
(CanonicalEnsemble.twoState_helmholtzFreeEnergy_eq)A simplification of the helmholtzFreeEnergy of the two-state canonical ensemble.
TODO Item
(file : PhysLean.StatisticalMechanics.Temperature)Define the function from Temperature to ℝ which gives the temperature in
Kelvin, based on axiomized constants.
Thermodynamics 🔥
Hide 0 TODO items:
Other ❓
Hide 3 TODO items:
TODO Item
(file : PhysLean.SpaceAndTime.SpaceTime.Basic)SpaceTime should be refactored into a structure, or similar, to prevent casting.
See on GitHub Tag: 6V2DRInformal Lemma
(SpaceTime.space_equivariant)The function space is equivariant with respect to rotations.
TODO Item
(file : PhysLean.StringTheory.FTheory.SU5U1.Charges.OfRationalSection)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.
See on GitHub Tag: AETF6