Merge pull request #89 from HEPLean/Update-versions
feat: Add AI doc-string check & stats
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
d3ccf80805
22 changed files with 265 additions and 47 deletions
|
|
@ -119,7 +119,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
|
|||
apply LinSols.ext
|
||||
exact χ.chargesAddCommMonoid.nsmul_succ _ _
|
||||
|
||||
/-- An instance providing the operations and properties for `LinSols` to form an
|
||||
/-- An instance providing the operations and properties for `LinSols` to form a
|
||||
module over `ℚ`. -/
|
||||
@[simps!]
|
||||
instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
|
||||
|
|
@ -147,7 +147,7 @@ instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
|
|||
exact χ.chargesModule.add_smul _ _ _
|
||||
|
||||
/-- An instance providing the operations and properties for `LinSols` to form an
|
||||
an additive community. -/
|
||||
additive commutative group. -/
|
||||
instance linSolsAddCommGroup (χ : ACCSystemLinear) : AddCommGroup χ.LinSols :=
|
||||
Module.addCommMonoidToAddCommGroup ℚ
|
||||
|
||||
|
|
@ -201,8 +201,8 @@ def quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.LinSols w
|
|||
toFun := QuadSols.toLinSols
|
||||
map_smul' _ _ := rfl
|
||||
|
||||
/-- If there are no quadratic equations (i.e. no U(1)'s in the underlying gauge group. The inclusion
|
||||
of linear solutions into quadratic solutions. -/
|
||||
/-- The inclusion of the linear solutions into the quadratic solutions, where there is
|
||||
no quadratic equations (i.e. no U(1)'s in the underlying gauge group). -/
|
||||
def linSolsInclQuadSolsZero (χ : ACCSystemQuad) (h : χ.numberQuadratic = 0) :
|
||||
χ.LinSols →[ℚ] χ.QuadSols where
|
||||
toFun S := ⟨S, by intro i; rw [h] at i; exact Fin.elim0 i⟩
|
||||
|
|
@ -233,7 +233,7 @@ lemma Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) :
|
|||
cases' S
|
||||
simp_all only
|
||||
|
||||
/-- We say a charge S is a solution if it extends to a solution. -/
|
||||
/-- A charge `S` is a solution if it extends to a solution. -/
|
||||
def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop :=
|
||||
∃ (sol : χ.Sols), sol.val = S
|
||||
|
||||
|
|
|
|||
|
|
@ -18,13 +18,13 @@ From this we define
|
|||
|
||||
-/
|
||||
|
||||
/-- The type of of a group action on a system of charges is defined as a representation on
|
||||
/-- The type of a group action on a system of charges is defined as a representation on
|
||||
the vector spaces of charges under which the anomaly equations are invariant.
|
||||
-/
|
||||
structure ACCSystemGroupAction (χ : ACCSystem) where
|
||||
/-- The underlying type of the group. -/
|
||||
group : Type
|
||||
/-- An instance given group the structure of a group. -/
|
||||
/-- An instance given the `group` component the structure of a `Group`. -/
|
||||
groupInst : Group group
|
||||
/-- The representation of group acting on the vector space of charges. -/
|
||||
rep : Representation ℚ group χ.Charges
|
||||
|
|
@ -79,8 +79,7 @@ lemma rep_linSolRep_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g :
|
|||
(S : χ.LinSols) : χ.linSolsIncl (G.linSolRep g S) =
|
||||
G.rep g (χ.linSolsIncl S) := rfl
|
||||
|
||||
/-- An instance given the structure to define a multiplicative action of `G.group` on `quadSols`.
|
||||
-/
|
||||
/-- A multiplicative action of `G.group` on `quadSols`. -/
|
||||
instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
|
||||
MulAction G.group χ.QuadSols where
|
||||
smul f S := ⟨G.linSolRep f S.1, by
|
||||
|
|
@ -112,8 +111,7 @@ instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.
|
|||
smul g S := ⟨G.quadSolAction.toFun S.1 g, by
|
||||
simp only [MulAction.toFun_apply]
|
||||
change χ.cubicACC (G.rep g S.val) = 0
|
||||
rw [G.cubicInvariant, S.cubicSol]
|
||||
⟩
|
||||
rw [G.cubicInvariant, S.cubicSol]⟩
|
||||
mul_smul f1 f2 S := by
|
||||
apply ACCSystem.Sols.ext
|
||||
change (G.rep.toFun (f1 * f2)) S.val = _
|
||||
|
|
|
|||
|
|
@ -60,7 +60,7 @@ def toSpeciesMaps' : (Fin 18 → ℚ) ≃ (Fin 6 → Fin 3 → ℚ) :=
|
|||
((@finProdFinEquiv 6 3).arrowCongr (Equiv.refl ℚ))).symm
|
||||
|
||||
/-- An equivalence between `MSSMCharges.charges` and `(Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ))`.
|
||||
This split charges up into the SM and additional fermions, and further splits the SM into
|
||||
This splits charges up into the SM and additional fermions, and further splits the SM into
|
||||
species. -/
|
||||
@[simps!]
|
||||
def toSpecies : MSSMCharges.Charges ≃ (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ) :=
|
||||
|
|
@ -233,7 +233,7 @@ lemma accSU3_ext {S T : MSSMCharges.Charges}
|
|||
repeat erw [hj]
|
||||
rfl
|
||||
|
||||
/-- The acc for `Y²`. -/
|
||||
/-- The ACC for `Y²`. -/
|
||||
@[simp]
|
||||
def accYY : MSSMCharges.Charges →ₗ[ℚ] ℚ where
|
||||
toFun S := ∑ i, ((Q S) i + 8 * (U S) i + 2 * (D S) i + 3 * (L S) i
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ def LineEqPropSol (R : MSSMACC.Sols) : Prop :=
|
|||
cubeTriLin R.val R.val Y₃.val * quadBiLin B₃.val R.val -
|
||||
cubeTriLin R.val R.val B₃.val * quadBiLin Y₃.val R.val = 0
|
||||
|
||||
/-- A rational which appears in `toSolNS` acting on sols, and which been zero is
|
||||
/-- A rational which appears in `toSolNS` acting on sols, and which being zero is
|
||||
equivalent to satisfying `lineEqPropSol`. -/
|
||||
def lineEqCoeff (T : MSSMACC.Sols) : ℚ := dot Y₃.val B₃.val * α₃ (proj T.1.1)
|
||||
|
||||
|
|
@ -185,30 +185,30 @@ lemma inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) :
|
|||
`lineEqProp`. -/
|
||||
def InLineEq : Type := {R : MSSMACC.AnomalyFreePerp // LineEqProp R}
|
||||
|
||||
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
|
||||
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the conditions
|
||||
`lineEqProp` and `inQuadProp`. -/
|
||||
def InQuad : Type := {R : InLineEq // InQuadProp R.val}
|
||||
|
||||
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
|
||||
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the conditions
|
||||
`lineEqProp`, `inQuadProp` and `inCubeProp`. -/
|
||||
def InQuadCube : Type := {R : InQuad // InCubeProp R.val.val}
|
||||
|
||||
/-- Those solutions which do not satisfy the condition `lineEqPropSol`. -/
|
||||
def NotInLineEqSol : Type := {R : MSSMACC.Sols // ¬ LineEqPropSol R}
|
||||
|
||||
/-- Those solutions which satisfy the condition `lineEqPropSol` by not `inQuadSolProp`. -/
|
||||
/-- Those solutions which satisfy the condition `lineEqPropSol` but not `inQuadSolProp`. -/
|
||||
def InLineEqSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ ¬ InQuadSolProp R}
|
||||
|
||||
/-- Those solutions which satisfy the condition `lineEqPropSol` and `inQuadSolProp` but
|
||||
not `inCubeSolProp`. -/
|
||||
def InQuadSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ ¬ InCubeSolProp R}
|
||||
|
||||
/-- Those solutions which satisfy the condition all the conditions `lineEqPropSol`, `inQuadSolProp`
|
||||
/-- Those solutions which satisfy the conditions `lineEqPropSol`, `inQuadSolProp`
|
||||
and `inCubeSolProp`. -/
|
||||
def InQuadCubeSol : Type :=
|
||||
{R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ InCubeSolProp R}
|
||||
|
||||
/-- Given a `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/
|
||||
/-- Given an `R` perpendicular to `Y₃` and `B₃` a quadratic solution. -/
|
||||
def toSolNSQuad (R : MSSMACC.AnomalyFreePerp) : MSSMACC.QuadSols :=
|
||||
lineQuad R
|
||||
(3 * cubeTriLin R.val R.val Y₃.val)
|
||||
|
|
@ -230,7 +230,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
|
|||
ring_nf
|
||||
simp
|
||||
|
||||
/-- Given a `R ` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
|
||||
/-- Given an `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)
|
||||
|
|
@ -258,7 +258,7 @@ lemma toSolNS_proj (T : NotInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val :=
|
|||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h1]
|
||||
simp
|
||||
|
||||
/-- Given a element of `inLineEq × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
|
||||
/-- A solution to the ACCs, given an element of `inLineEq × ℚ × ℚ × ℚ`. -/
|
||||
def inLineEqToSol : InLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c₁, c₂, c₃) =>
|
||||
AnomalyFreeMk'' (lineQuad R.val c₁ c₂ c₃)
|
||||
(by
|
||||
|
|
@ -301,7 +301,7 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
|
|||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
|
||||
simp
|
||||
|
||||
/-- Given a element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
|
||||
/-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
|
||||
def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
|
||||
AnomalyFreeMk' (lineCube R.val.val a₁ a₂ a₃)
|
||||
(by
|
||||
|
|
@ -389,7 +389,7 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
|
|||
rw [show dot Y₃.val B₃.val = 108 by rfl]
|
||||
simp
|
||||
|
||||
/-- Given an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` a solution. We will
|
||||
/-- A solution from an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ`. We will
|
||||
show that this map is a surjection. -/
|
||||
def toSol : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, b, c) =>
|
||||
if h₃ : LineEqProp R ∧ InQuadProp R ∧ InCubeProp R then
|
||||
|
|
|
|||
|
|
@ -136,7 +136,7 @@ lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
|
|||
rw [boundary_castSucc hS hk, boundary_succ hS hk]
|
||||
ring
|
||||
|
||||
/-- We say a `S ∈ charges` has a boundary if there exists a `k ∈ Fin n` which is a boundary. -/
|
||||
/-- A `S ∈ charges` has a boundary if there exists a `k ∈ Fin n` which is a boundary. -/
|
||||
@[simp]
|
||||
def HasBoundary (S : (PureU1 n.succ).Charges) : Prop :=
|
||||
∃ (k : Fin n), Boundary S k
|
||||
|
|
|
|||
|
|
@ -616,7 +616,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : Pa' f = Pa' f' ↔ f =
|
|||
rw [← Finset.sum_add_distrib]
|
||||
simp
|
||||
have h2 : ∀ i, (f i + (- f' i)) = 0 := by
|
||||
exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent (n))
|
||||
exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n)
|
||||
(fun i => f i + -f' i) h1
|
||||
have h2i := h2 i
|
||||
linarith
|
||||
|
|
@ -667,7 +667,7 @@ lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
|
|||
simp only [Fintype.card_sum, Fintype.card_fin, mul_eq]
|
||||
omega
|
||||
|
||||
/-- The basis formed out of our basisa vectors. -/
|
||||
/-- The basis formed out of our `basisa` vectors. -/
|
||||
noncomputable def basisaAsBasis :
|
||||
Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols :=
|
||||
basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic
|
|||
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
|
||||
(lineInCubic_expand h g f hS 1 2) / 6
|
||||
|
||||
/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
|
||||
/-- A `LinSol` satisfies `LineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
|
||||
def LineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
|
||||
∀ (M : (FamilyPermutations (2 * n.succ)).group),
|
||||
LineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)
|
||||
|
|
|
|||
|
|
@ -37,11 +37,11 @@ def LineInPlaneProp : ℚ × ℚ × ℚ → Prop := fun s =>
|
|||
s.1 = s.2.1 ∨ s.1 = - s.2.1 ∨ 2 * s.2.2 + s.1 + s.2.1 = 0
|
||||
|
||||
/-- The proposition on a `LinSol` to satisfy the `linInPlane` condition. -/
|
||||
def LineInPlaneCond (S : (PureU1 (n)).LinSols) : Prop :=
|
||||
∀ (i1 i2 i3 : Fin (n)) (_ : i1 ≠ i2) (_ : i2 ≠ i3) (_ : i1 ≠ i3),
|
||||
def LineInPlaneCond (S : (PureU1 n).LinSols) : Prop :=
|
||||
∀ (i1 i2 i3 : Fin n) (_ : i1 ≠ i2) (_ : i2 ≠ i3) (_ : i1 ≠ i3),
|
||||
LineInPlaneProp (S.val i1, (S.val i2, S.val i3))
|
||||
|
||||
lemma lineInPlaneCond_perm {S : (PureU1 (n)).LinSols} (hS : LineInPlaneCond S)
|
||||
lemma lineInPlaneCond_perm {S : (PureU1 n).LinSols} (hS : LineInPlaneCond S)
|
||||
(M : (FamilyPermutations n).group) :
|
||||
LineInPlaneCond ((FamilyPermutations n).linSolRep M S) := by
|
||||
intro i1 i2 i3 h1 h2 h3
|
||||
|
|
|
|||
|
|
@ -601,7 +601,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔
|
|||
rw [← Finset.sum_add_distrib]
|
||||
simp
|
||||
have h2 : ∀ i, (f i + (- f' i)) = 0 := by
|
||||
exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent (n))
|
||||
exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n)
|
||||
(fun i => f i + -f' i) h1
|
||||
have h2i := h2 i
|
||||
linarith
|
||||
|
|
|
|||
|
|
@ -61,16 +61,16 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S
|
|||
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
|
||||
(lineInCubic_expand h g f hS 1 2) / 6
|
||||
|
||||
/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
|
||||
/-- A `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
|
||||
def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
|
||||
∀ (M : (FamilyPermutations (2 * n + 1)).group),
|
||||
LineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)
|
||||
|
||||
/-- If `lineInCubicPerm S` then `lineInCubic S`. -/
|
||||
/-- If `lineInCubicPerm S`, then `lineInCubic S`. -/
|
||||
lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : LineInCubicPerm S) :
|
||||
LineInCubic S := hS 1
|
||||
|
||||
/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/
|
||||
/-- If `lineInCubicPerm S`, then `lineInCubicPerm (M S)` for all permutations `M`. -/
|
||||
lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
|
||||
(hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) :
|
||||
LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) := by
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ namespace PureU1
|
|||
|
||||
variable {n : ℕ}
|
||||
|
||||
/-- We say a charge is shorted if for all `i ≤ j`, then `S i ≤ S j`. -/
|
||||
/-- A charge is sorted if for all `i ≤ j`, then `S i ≤ S j`. -/
|
||||
@[simp]
|
||||
def Sorted {n : ℕ} (S : (PureU1 n).Charges) : Prop :=
|
||||
∀ i j (_ : i ≤ j), S i ≤ S j
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
|
|||
|
||||
instance : Module ℝ F.HalfEdgeMomenta := Pi.module _ _ _
|
||||
|
||||
/-- An auxillary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
|
||||
/-- An auxiliary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
|
||||
def euclidInnerAux (x : F.HalfEdgeMomenta) : F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
|
||||
toFun y := ∑ i, (x i) * (y i)
|
||||
map_add' z y :=
|
||||
|
|
@ -77,7 +77,7 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ]
|
|||
simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply,
|
||||
LinearMap.smul_apply]
|
||||
|
||||
/-- The type which assocaites to each ege a `1`-dimensional vector space.
|
||||
/-- The type which associates to each edge a `1`-dimensional vector space.
|
||||
Corresponding to that spanned by its total outflowing momentum. -/
|
||||
def EdgeMomenta : Type := F.𝓔 → ℝ
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ open CKMMatrix
|
|||
|
||||
noncomputable section
|
||||
|
||||
/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
|
||||
/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard parameterization of the CKM matrix
|
||||
as a `3×3` complex matrix. -/
|
||||
def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
|
||||
![![Real.cos θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₃ * exp (-I * δ₁₃)],
|
||||
|
|
@ -96,8 +96,8 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
|
|||
rw [sin_sq, sin_sq]
|
||||
ring
|
||||
|
||||
/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
|
||||
as a CKM matrix. -/
|
||||
/-- A CKM Matrix from four reals `θ₁₂`, `θ₁₃`, `θ₂₃`, and `δ₁₃`. This is the standard
|
||||
parameterization of CKM matrices. -/
|
||||
def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
|
||||
⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
|
||||
rw [mem_unitaryGroup_iff']
|
||||
|
|
|
|||
|
|
@ -151,7 +151,7 @@ lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= by
|
|||
refine (inv_eq_left_inv ?h).symm
|
||||
exact mem_iff_dual_mul_self.mp Λ.2
|
||||
|
||||
/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
|
||||
/-- The transpose of a matrix in the Lorentz group is an element of the Lorentz group. -/
|
||||
def transpose (Λ : LorentzGroup d) : LorentzGroup d :=
|
||||
⟨Λ.1ᵀ, mem_iff_transpose.mp Λ.2⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ variable (d : ℕ)
|
|||
/-- The type of Lorentz Vectors in `d`-space dimensions. -/
|
||||
def LorentzVector : Type := (Fin 1 ⊕ Fin d) → ℝ
|
||||
|
||||
/-- An instance of a additive commutative monoid on `LorentzVector`. -/
|
||||
/-- An instance of an additive commutative monoid on `LorentzVector`. -/
|
||||
instance : AddCommMonoid (LorentzVector d) := Pi.addCommMonoid
|
||||
|
||||
/-- An instance of a module on `LorentzVector`. -/
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ open Matrix
|
|||
# The definition of the Minkowski Matrix
|
||||
|
||||
-/
|
||||
/-- The `d.succ`-dimensional real of the form `diag(1, -1, -1, -1, ...)`. -/
|
||||
/-- The `d.succ`-dimensional real matrix of the form `diag(1, -1, -1, -1, ...)`. -/
|
||||
def minkowskiMatrix {d : ℕ} : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
|
||||
LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin d) ℝ
|
||||
|
||||
|
|
@ -146,7 +146,7 @@ lemma self_eq_time_minus_norm : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 :
|
|||
rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
|
||||
noncomm_ring
|
||||
|
||||
/-- The Minkowski metric is symmetric. -/
|
||||
/-- The Minkowski metric is symmetric in its arguments.. -/
|
||||
lemma symm : ⟪v, w⟫ₘ = ⟪w, v⟫ₘ := by
|
||||
simp only [as_sum]
|
||||
ac_rfl
|
||||
|
|
|
|||
|
|
@ -50,6 +50,7 @@ noncomputable def matrixToLin : Matrix (Fin 2) (Fin 2) ℂ →* (HiggsVec →L[
|
|||
Matrix.toLin_mul orthonormBasis.toBasis orthonormBasis.toBasis orthonormBasis.toBasis g h
|
||||
map_one' := ContinuousLinearMap.coe_inj.mp $ Matrix.toLin_one orthonormBasis.toBasis
|
||||
|
||||
/-- `matrixToLin` commutes with the `star` operation. -/
|
||||
lemma matrixToLin_star (g : Matrix (Fin 2) (Fin 2) ℂ) :
|
||||
matrixToLin (star g) = star (matrixToLin g) :=
|
||||
ContinuousLinearMap.coe_inj.mp $ Matrix.toLin_conjTranspose orthonormBasis orthonormBasis g
|
||||
|
|
@ -129,7 +130,7 @@ lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) :
|
|||
mem_specialUnitaryGroup_iff.mpr ⟨rotateMatrix_unitary hφ, rotateMatrix_det hφ⟩
|
||||
|
||||
/-- Given a Higgs vector, an element of the gauge group which puts the first component of the
|
||||
vector to zero, and the second component to a real -/
|
||||
vector to zero, and the second component to a real number. -/
|
||||
def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroup :=
|
||||
⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -16,6 +16,12 @@ rev = "v4.10.0-rc1"
|
|||
[[lean_lib]]
|
||||
name = "HepLean"
|
||||
|
||||
# -- Optional inclusion of llm. Needed for `openAI_doc_check`
|
||||
#[[require]]
|
||||
#name = "llm"
|
||||
#git = "https://github.com/leanprover-community/llm"
|
||||
#rev = "main"
|
||||
|
||||
# -- Optional inclusion of tryAtEachStep
|
||||
#[[require]]
|
||||
#name = "tryAtEachStep"
|
||||
|
|
@ -48,4 +54,13 @@ srcDir = "scripts"
|
|||
|
||||
[[lean_exe]]
|
||||
name = "mathlib_textLint_on_hepLean"
|
||||
srcDir = "scripts"
|
||||
srcDir = "scripts"
|
||||
|
||||
[[lean_exe]]
|
||||
name = "stats"
|
||||
srcDir = "scripts"
|
||||
|
||||
# -- Optional inclusion of openAI_doc_check. Needs `llm` above.
|
||||
#[[lean_exe]]
|
||||
#name = "openAI_doc_check"
|
||||
#srcDir = "scripts"
|
||||
|
|
@ -37,6 +37,37 @@ Run using
|
|||
lake exe type_former_lint
|
||||
```
|
||||
|
||||
## stats.sh
|
||||
|
||||
Outputs statistics for HepLean.
|
||||
|
||||
Run using
|
||||
```
|
||||
lake exe stats
|
||||
```
|
||||
|
||||
## openAI_doc_check.lean
|
||||
|
||||
Uses openAI's API to check for spelling mistakes etc. in doc strings.
|
||||
|
||||
This code needs `https://github.com/jstoobysmith/Lean_llm_fork` to be installed.
|
||||
|
||||
It also needs the enviroment variable `OPENAI_API_KEY` defined using e.g.
|
||||
```
|
||||
export OPENAI_API_KEY=<Your-openAI-key>
|
||||
```
|
||||
|
||||
Run on a specific file using
|
||||
```
|
||||
lake exe openAI_doc_check <module_name>
|
||||
```
|
||||
where `<module_name>` is e.g. `HepLean.SpaceTime.Basic`.
|
||||
|
||||
Run on a random file using
|
||||
```
|
||||
lake exe openAI_doc_check random
|
||||
```
|
||||
|
||||
## lint-all.sh
|
||||
|
||||
Performs all linting checks on HepLean.
|
||||
|
|
|
|||
|
|
@ -17,6 +17,11 @@ There are currently not enforced at the GitHub action level.
|
|||
|
||||
Parts of this file are adapted from `Mathlib.Tactic.Linter.TextBased`,
|
||||
authored by Michael Rothgang.
|
||||
|
||||
## TODO
|
||||
|
||||
Some of the linters here can be replaced by regex.
|
||||
|
||||
-/
|
||||
open Lean System Meta
|
||||
|
||||
|
|
@ -78,7 +83,8 @@ def hepLeanLintFile (path : FilePath) : IO Bool := do
|
|||
let allOutput := (Array.map (fun lint ↦
|
||||
(Array.map (fun (e, n, c) ↦ HepLeanErrorContext.mk e n c path)) (lint lines)))
|
||||
#[doubleEmptyLineLinter, doubleSpaceLinter, substringLinter ".-/", substringLinter " )",
|
||||
substringLinter "( ", substringLinter "=by", substringLinter " def "]
|
||||
substringLinter "( ", substringLinter "=by", substringLinter " def ",
|
||||
substringLinter "/-- We "]
|
||||
let errors := allOutput.flatten
|
||||
printErrors errors
|
||||
return errors.size > 0
|
||||
|
|
|
|||
79
scripts/openAI_doc_check.lean
Normal file
79
scripts/openAI_doc_check.lean
Normal file
|
|
@ -0,0 +1,79 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import Batteries.Lean.IO.Process
|
||||
import Lean
|
||||
import Lean.Parser
|
||||
import Lean.Data.Json
|
||||
import Mathlib.Lean.CoreM
|
||||
import LLM.GPT.Json
|
||||
import LLM.GPT.API
|
||||
/-!
|
||||
|
||||
# HepLean OpenAI doc check
|
||||
|
||||
This file uses the openAI API to check the doc strings of definitions and theorems in a
|
||||
Lean 4 file.
|
||||
|
||||
This file depends on `https://github.com/leanprover-community/llm` being imported.
|
||||
This is not currently done by default.
|
||||
|
||||
-/
|
||||
open Lean
|
||||
open LLM
|
||||
open System Meta
|
||||
|
||||
def getDocString (constName : Array ConstantInfo) : MetaM String := do
|
||||
let env ← getEnv
|
||||
let mut docString := ""
|
||||
for c in constName do
|
||||
if ¬ Lean.Name.isInternalDetail c.name then
|
||||
let doc ← Lean.findDocString? env c.name
|
||||
match doc with
|
||||
| some x => docString := docString ++ "- " ++ x ++ "\n"
|
||||
| none => docString := docString
|
||||
return docString
|
||||
|
||||
def header : String := "
|
||||
Answer as if you an expert mathematician, physicist and software engineer.
|
||||
Below I have listed the doc strings of definitions and theorems in a Lean 4 file.
|
||||
Output a list of 1) spelling mistakes. 2) grammatical errors. 3) suggestions for improvement.
|
||||
Note that text within `...` should be treated as code and not spellchecked. Doc strings
|
||||
should be a complete sentence, or a noun phrase.
|
||||
|
||||
|
||||
"
|
||||
|
||||
def main (args : List String) : IO UInt32 := do
|
||||
initSearchPath (← findSysroot)
|
||||
let firstArg := args.head?
|
||||
match firstArg with
|
||||
| some x => do
|
||||
let mut imp : Import := Import.mk x.toName false
|
||||
if x == "random" then
|
||||
let mods : Name := `HepLean
|
||||
let imps : Import := {module := mods}
|
||||
let mFile ← findOLean imps.module
|
||||
unless (← mFile.pathExists) do
|
||||
throw <| IO.userError s!"object file '{mFile}' of module {imps.module} does not exist"
|
||||
let (hepLeanMod, _) ← readModuleData mFile
|
||||
let imports := hepLeanMod.imports
|
||||
let y ← IO.rand 0 (imports.size -1)
|
||||
imp := imports.get! y
|
||||
let mFile ← findOLean imp.module
|
||||
let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean"
|
||||
IO.println s!"Checking: {filePath}"
|
||||
let (modData, _) ← readModuleData mFile
|
||||
let cons := modData.constants
|
||||
let docString ← CoreM.withImportModules #[imp.module] (getDocString cons).run'
|
||||
let message : LLM.Message := {role := Role.user, content := header ++ docString}
|
||||
let request : GPT.Request := {messages := [message]}
|
||||
let response ← LLM.GPT.chat (toString <| ToJson.toJson request)
|
||||
let parsedRespone := GPT.parse response
|
||||
match parsedRespone with
|
||||
| .ok x => IO.println x
|
||||
| .error e => IO.println e
|
||||
| none => IO.println "No module provided."
|
||||
return 0
|
||||
88
scripts/stats.lean
Normal file
88
scripts/stats.lean
Normal file
|
|
@ -0,0 +1,88 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import Batteries.Lean.HashSet
|
||||
import Lean
|
||||
import Mathlib.Lean.Expr.Basic
|
||||
import Mathlib.Lean.CoreM
|
||||
import HepLean
|
||||
/-!
|
||||
|
||||
# HepLean Stats
|
||||
|
||||
This file concerns with statistics of HepLean.
|
||||
|
||||
-/
|
||||
|
||||
|
||||
open Lean System Meta
|
||||
|
||||
structure FileStats where
|
||||
numDefs : Nat
|
||||
numLemsWithoutDocString : Nat
|
||||
numLemsWithDocString : Nat
|
||||
|
||||
def FileStats.add (a b : FileStats) : FileStats where
|
||||
numDefs := a.numDefs + b.numDefs
|
||||
numLemsWithoutDocString := a.numLemsWithoutDocString + b.numLemsWithoutDocString
|
||||
numLemsWithDocString := a.numLemsWithDocString + b.numLemsWithDocString
|
||||
|
||||
def FileStats.zero : FileStats where
|
||||
numDefs := 0
|
||||
numLemsWithoutDocString := 0
|
||||
numLemsWithDocString := 0
|
||||
|
||||
instance : ToString FileStats where
|
||||
toString fs := s!"Number of definitions: {fs.numDefs}\n" ++
|
||||
s!"Number of lemmas without doc string: {fs.numLemsWithoutDocString}\n" ++
|
||||
s!"Number of lemmas with doc string: {fs.numLemsWithDocString}"
|
||||
|
||||
def getConstantDoc (constName : Array ConstantInfo) : MetaM (FileStats) := do
|
||||
let env ← getEnv
|
||||
let mut numDefs := 0
|
||||
let mut numLemsWithoutDocString := 0
|
||||
let mut numLemsWithDocString := 0
|
||||
for c in constName do
|
||||
if ¬ Lean.Name.isInternalDetail c.name then
|
||||
if c.isDef then
|
||||
numDefs := numDefs + 1
|
||||
if c.isThm then
|
||||
let doc ← Lean.findDocString? env c.name
|
||||
if doc == none then
|
||||
numLemsWithoutDocString := numLemsWithoutDocString + 1
|
||||
else
|
||||
numLemsWithDocString := numLemsWithDocString + 1
|
||||
return {numDefs := numDefs,
|
||||
numLemsWithoutDocString := numLemsWithoutDocString,
|
||||
numLemsWithDocString := numLemsWithDocString}
|
||||
|
||||
def getStats (imp : Import) : MetaM FileStats := do
|
||||
if imp.module == `Init then
|
||||
return {numDefs := 0,
|
||||
numLemsWithoutDocString := 0,
|
||||
numLemsWithDocString := 0}
|
||||
let mFile ← findOLean imp.module
|
||||
let (modData, _) ← readModuleData mFile
|
||||
let cons := modData.constants
|
||||
let out ← (getConstantDoc cons)
|
||||
return out
|
||||
|
||||
def getStatsArray (a : Array Import) : MetaM (Array FileStats) := do
|
||||
return ← a.mapM getStats
|
||||
|
||||
def main (_ : List String) : IO UInt32 := do
|
||||
initSearchPath (← findSysroot)
|
||||
let mods : Name := `HepLean
|
||||
let imp : Import := {module := mods}
|
||||
let mFile ← findOLean imp.module
|
||||
unless (← mFile.pathExists) do
|
||||
throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist"
|
||||
let (hepLeanMod, _) ← readModuleData mFile
|
||||
let noFiles := hepLeanMod.imports.size - 1
|
||||
let fileStats ← CoreM.withImportModules #[`HepLean] (getStatsArray hepLeanMod.imports).run'
|
||||
let totalStats := Array.foldl FileStats.add FileStats.zero fileStats
|
||||
IO.println s!"Total number of files: {noFiles}"
|
||||
IO.println totalStats
|
||||
pure 0
|
||||
Loading…
Add table
Add a link
Reference in a new issue