DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #45 from pitmonticone/docstrings

Browse source 
docs: clean docstrings
This commit is contained in:
Joseph Tooby-Smith 2024-06-09 11:28:03 -04:00 • committed by GitHub
commit de720c6f69
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 22 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/AnomalyCancellation/Basic.lean
View file

@ -87,7 +87,7 @@ lemma LinSols.ext {χ : ACCSystemLinear} {S T : χ.LinSols} (h : S.val = T.val)
simp_all only
/-- An instance providing the operations and properties for `LinSols` to form an
addative commutative monoid. -/
additive commutative monoid. -/
@[simps!]
instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
AddCommMonoid χ.LinSols where

6
HepLean/AnomalyCancellation/LinearMaps.lean
View file

@ -9,7 +9,7 @@ import Mathlib.Algebra.BigOperators.Fin
/-!
# Linear maps
Some definitions and properites of linear, bilinear, and trilinear maps, along with homogeneous
Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous
quadratic and cubic equations.
## TODO
@ -62,7 +62,7 @@ instance instFun (V : Type) [AddCommMonoid V] [Module ℚ V] :
cases g
simp_all
/-- The construction of a symmetric bilinear map from smul and map_add in the first factor,
/-- The construction of a symmetric bilinear map from `smul` and `map_add` in the first factor,
and swap. -/
@[simps!]
def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S, T))
@ -196,7 +196,7 @@ instance instFun : FunLike (TriLinearSymm V) V (V →ₗ[ℚ] V →ₗ[ℚ] ℚ
cases g
simp_all
/-- The construction of a symmetric trilinear map from smul and map_add in the first factor,
/-- The construction of a symmetric trilinear map from `smul` and `map_add` in the first factor,
and two swap. -/
@[simps!]
def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) = a * f (S, T, L))

6
HepLean/AnomalyCancellation/MSSMNu/B3.lean
View file

@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.MSSMNu.Basic
/-!
# The definition of the solution B₃ and properties thereof
We define $B_3$ and show that it is a double point of the cubic.
We define `B₃` and show that it is a double point of the cubic.
# References
@ -24,7 +24,7 @@ open MSSMCharges
open MSSMACCs
open BigOperators
/-- $B_3$ is the charge which is $B-L$ in all families, but with the third
/-- `B₃` is the charge which is $B-L$ in all families, but with the third
family of the opposite sign. -/
def B₃AsCharge : MSSMACC.charges := toSpecies.symm
⟨fun s => fun i =>
@ -52,7 +52,7 @@ def B₃AsCharge : MSSMACC.charges := toSpecies.symm
| 0 => -3
| 1 => 3⟩
/-- $B_3$ as a solution. -/
/-- `B₃` as a solution. -/
def B₃ : MSSMACC.Sols :=
MSSMACC.AnomalyFreeMk B₃AsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)

10
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
View file

@ -27,8 +27,8 @@ open MSSMCharges
open MSSMACCs
open BigOperators
/-- The plane of linear solutions spanned by $Y_3$, $B_3$ and $R$, a point orthogonal
to $Y_3$ and $B_3$. -/
/-- The plane of linear solutions spanned by `Y₃`, `B₃` and `R`, a point orthogonal
to `Y₃` and `B₃`. -/
def planeY₃B₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) : MSSMACC.LinSols :=
a • Y₃.1.1 + b • B₃.1.1 + c • R.1
@ -127,7 +127,7 @@ lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
rw [show (TriLinearSymm.toCubic cubeTriLin) R.val = cubeTriLin R.val R.val R.val by rfl]
ring
/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic,
/-- The line in the plane spanned by `Y₃`, `B₃` and `R` which is in the quadratic,
as `LinSols`. -/
def lineQuadAFL (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.LinSols :=
planeY₃B₃ R (c2 * quadBiLin R.val R.val - 2 * c3 * quadBiLin B₃.val R.val)
@ -141,7 +141,7 @@ lemma lineQuadAFL_quad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) :
apply Or.inr
ring
/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic. -/
/-- The line in the plane spanned by `Y₃`, `B₃` and `R` which is in the quadratic. -/
def lineQuad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.QuadSols :=
AnomalyFreeQuadMk' (lineQuadAFL R c1 c2 c3) (lineQuadAFL_quad R c1 c2 c3)
@ -184,7 +184,7 @@ def α₁ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
rw [planeY₃B₃_cubic, α₁, α₂, α₃]
ring
/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the cubic. -/
/-- The line in the plane spanned by `Y₃`, `B₃` and `R` which is in the cubic. -/
def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
MSSMACC.LinSols :=
planeY₃B₃ R

4
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
View file

@ -233,7 +233,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
ring_nf
simp
/-- Given a `R ` perpendicular to $Y_3$, and $B_3$, a element of `Sols`. This map is
/-- Given a `R ` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
not surjective. -/
def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) =>
a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)
@ -332,7 +332,6 @@ def inQuadProj (T : inQuadSol) : inQuad × ℚ × ℚ × ℚ :=
- cubeTriLin T.val.val T.val.val Y₃.val
* (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val)))
lemma inQuadToSol_proj (T : inQuadSol) : inQuadToSol (inQuadProj T) = T.val := by
rw [inQuadProj, inQuadToSol_smul]
apply ACCSystem.Sols.ext
@ -371,7 +370,6 @@ lemma inQuadCubeToSol_smul (R : inQuadCube) (c₁ c₂ c₃ d : ℚ) :
rw [planeY₃B₃_smul]
rfl
/-- On elements of `inQuadCubeSol` a right-inverse to `inQuadCubeToSol`. -/
def inQuadCubeProj (T : inQuadCubeSol) : inQuadCube × ℚ × ℚ × ℚ :=
(⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩,

2
HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
View file

@ -10,7 +10,7 @@ import HepLean.StandardModel.HiggsBoson.Basic
The two Higgs doublet model is the standard model plus an additional Higgs doublet.
Currently this file contains the definition of the 2HDM optential.
Currently this file contains the definition of the 2HDM potential.
-/

2
HepLean/SpaceTime/FourVelocity.lean
View file

@ -70,7 +70,7 @@ lemma zero_nonneg_iff (v : PreFourVelocity) : 0 ≤ v.1 0 ↔ 1 ≤ v.1 0 := by
· intro h
linarith
/-- A `PreFourVelocity` is a `FourVelocity` if its time componenet is non-negative. -/
/-- A `PreFourVelocity` is a `FourVelocity` if its time component is non-negative. -/
def IsFourVelocity (v : PreFourVelocity) : Prop := 0 ≤ v.1 0

12
HepLean/SpaceTime/LorentzGroup/Boosts.lean
View file

@ -12,14 +12,14 @@ import Mathlib.Topology.Constructions
This file defines those Lorentz which are boosts.
We first define generalised boosts, which are restricted lorentz transforamations taking
a four velocity `u` to a four velcoity `v`.
We first define generalised boosts, which are restricted lorentz transformations taking
a four velocity `u` to a four velocity `v`.
A boost is the speical case of a generalised boost when `u = stdBasis 0`.
A boost is the special case of a generalised boost when `u = stdBasis 0`.
## TODO
- Show that generalised boosts are in the restircted Lorentz group.
- Show that generalised boosts are in the restricted Lorentz group.
- Define boosts.
## References
@ -35,7 +35,7 @@ namespace lorentzGroup
open FourVelocity
/-- An auxillary linear map used in the definition of a genearlised boost. -/
/-- An auxillary linear map used in the definition of a generalised boost. -/
def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
toFun x := (2 * ηLin x u) • v.1.1
map_add' x y := by
@ -61,7 +61,7 @@ def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
rfl
/-- An genearlised boost. This is a Lorentz transformation which takes the four velocity `u`
/-- An generalised boost. This is a Lorentz transformation which takes the four velocity `u`
to `v`. -/
def genBoost (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime :=
LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v

2
HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
View file

@ -171,7 +171,7 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬
rw [zero_zero_mul]
exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
def orthchroRep : lorentzGroup →* ℤ₂ where
toFun := orthchroMap
map_one' := by