diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index 68a7426..451f47d 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/GroupActions.lean b/HepLean/AnomalyCancellation/GroupActions.lean index d9b21fc..05edfa9 100644 --- a/HepLean/AnomalyCancellation/GroupActions.lean +++ b/HepLean/AnomalyCancellation/GroupActions.lean @@ -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 = _ diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean index 3b69995..49883d7 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean index 3623350..6774b88 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean index 4a2ed22..1371ee9 100644 --- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean +++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean index 086ba59..24686eb 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean index 9b9f6b3..064c3d3 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean @@ -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) diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean index 7d1f83f..a4e8557 100644 --- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean +++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean index 9e19db1..61dcf38 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean index c01a557..edd2003 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean @@ -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 diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sort.lean index 92a9a70..e986648 100644 --- a/HepLean/AnomalyCancellation/PureU1/Sort.lean +++ b/HepLean/AnomalyCancellation/PureU1/Sort.lean @@ -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 diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean index 97dd77a..b23fcdb 100644 --- a/HepLean/FeynmanDiagrams/Momentum.lean +++ b/HepLean/FeynmanDiagrams/Momentum.lean @@ -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.𝓔 → ℝ diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean index de163c7..417371e 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean @@ -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'] diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 3112055..ab50ccc 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -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⟩ diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean index ff85c66..ce829c0 100644 --- a/HepLean/SpaceTime/LorentzVector/Basic.lean +++ b/HepLean/SpaceTime/LorentzVector/Basic.lean @@ -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`. -/ diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean index dbea26e..fa10338 100644 --- a/HepLean/SpaceTime/MinkowskiMetric.lean +++ b/HepLean/SpaceTime/MinkowskiMetric.lean @@ -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 diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean index a2597e1..9eadda7 100644 --- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean +++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean @@ -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⟩ diff --git a/lakefile.toml b/lakefile.toml index 49e2387..0326152 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -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" \ No newline at end of file +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" \ No newline at end of file diff --git a/scripts/README.md b/scripts/README.md index bb0b952..6a49ffb 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -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= +``` + +Run on a specific file using +``` +lake exe openAI_doc_check +``` +where `` 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. diff --git a/scripts/hepLean_style_lint.lean b/scripts/hepLean_style_lint.lean index 254ddd0..c1c709f 100644 --- a/scripts/hepLean_style_lint.lean +++ b/scripts/hepLean_style_lint.lean @@ -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 diff --git a/scripts/openAI_doc_check.lean b/scripts/openAI_doc_check.lean new file mode 100644 index 0000000..b8a07df --- /dev/null +++ b/scripts/openAI_doc_check.lean @@ -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 diff --git a/scripts/stats.lean b/scripts/stats.lean new file mode 100644 index 0000000..3a14bca --- /dev/null +++ b/scripts/stats.lean @@ -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