From 9f27a3a9fd9523faaba9d75f5419e1d18ec07439 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 19 Jul 2024 17:00:32 -0400 Subject: [PATCH] refactor: Lint --- HepLean/AnomalyCancellation/Basic.lean | 2 +- HepLean/AnomalyCancellation/GroupActions.lean | 16 +++---- HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 4 +- .../MSSMNu/OrthogY3B3/Basic.lean | 6 +-- .../MSSMNu/OrthogY3B3/PlaneWithY3B3.lean | 2 +- .../MSSMNu/OrthogY3B3/ToSols.lean | 7 ++- HepLean/AnomalyCancellation/PureU1/Basic.lean | 6 +-- .../PureU1/BasisLinear.lean | 15 +++---- .../AnomalyCancellation/PureU1/ConstAbs.lean | 2 +- .../PureU1/Even/BasisLinear.lean | 24 +++++------ .../PureU1/Even/LineInCubic.lean | 12 +++--- .../PureU1/Even/Parameterization.lean | 12 +++--- .../PureU1/LineInPlaneCond.lean | 2 +- .../PureU1/Odd/BasisLinear.lean | 14 +++--- .../PureU1/Odd/LineInCubic.lean | 8 ++-- .../PureU1/Odd/Parameterization.lean | 12 +++--- .../PureU1/Permutations.lean | 10 ++--- HepLean/AnomalyCancellation/PureU1/Sort.lean | 2 +- .../SM/NoGrav/One/Lemmas.lean | 2 +- .../SM/NoGrav/One/LinearParameterization.lean | 8 ++-- .../AnomalyCancellation/SM/Permutations.lean | 2 +- HepLean/AnomalyCancellation/SMNu/Basic.lean | 2 +- .../AnomalyCancellation/SMNu/FamilyMaps.lean | 2 +- .../SMNu/PlusU1/BMinusL.lean | 2 +- .../SMNu/PlusU1/BoundPlaneDim.lean | 4 +- .../SMNu/PlusU1/HyperCharge.lean | 2 +- HepLean/FeynmanDiagrams/Basic.lean | 14 +++--- HepLean/FeynmanDiagrams/Momentum.lean | 12 +++--- HepLean/FlavorPhysics/CKMMatrix/Basic.lean | 22 +++++----- .../FlavorPhysics/CKMMatrix/Invariants.lean | 4 +- .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean | 2 +- .../StandardParameterization/Basic.lean | 6 +-- .../StandardParameters.lean | 18 ++++---- HepLean/Mathematics/SO3/Basic.lean | 2 +- HepLean/SpaceTime/LorentzGroup/Basic.lean | 2 +- HepLean/SpaceTime/LorentzGroup/Boosts.lean | 2 +- .../SpaceTime/LorentzGroup/Orthochronous.lean | 6 +-- .../SpaceTime/LorentzTensor/Real/Basic.lean | 4 +- .../LorentzTensor/Real/Multiplication.lean | 4 +- HepLean/SpaceTime/LorentzVector/NormOne.lean | 6 +-- HepLean/SpaceTime/MinkowskiMetric.lean | 2 +- HepLean/SpaceTime/SL2C/Basic.lean | 6 +-- .../StandardModel/HiggsBoson/GaugeAction.lean | 4 +- .../HiggsBoson/PointwiseInnerProd.lean | 3 +- HepLean/StandardModel/Representations.lean | 2 +- scripts/hepLean_style_lint.lean | 43 +++++++++++++------ 46 files changed, 176 insertions(+), 168 deletions(-) diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index a3b6f4a..83d38d8 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -234,7 +234,7 @@ lemma Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) : /-- A charge `S` is a solution if it extends to a solution. -/ def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop := - ∃ (sol : χ.Sols), sol.val = S + ∃ (sol : χ.Sols), sol.val = S /-- An instance giving the properties and structures to define an action of `ℚ` on `Sols`. -/ instance solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols where diff --git a/HepLean/AnomalyCancellation/GroupActions.lean b/HepLean/AnomalyCancellation/GroupActions.lean index f275eeb..356cf47 100644 --- a/HepLean/AnomalyCancellation/GroupActions.lean +++ b/HepLean/AnomalyCancellation/GroupActions.lean @@ -43,8 +43,8 @@ instance {χ : ACCSystem} (G : ACCSystemGroupAction χ) : Group G.group := G.gro def linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) : χ.LinSols →ₗ[ℚ] χ.LinSols where toFun S := ⟨G.rep g S.val, by - intro i - rw [G.linearInvariant, S.linearSol]⟩ + intro i + rw [G.linearInvariant, S.linearSol]⟩ map_add' S T := by apply ACCSystemLinear.LinSols.ext exact (G.rep g).map_add' _ _ @@ -82,9 +82,9 @@ lemma rep_linSolRep_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.group χ.QuadSols where smul f S := ⟨G.linSolRep f S.1, by - intro i - simp only [linSolRep_apply_apply_val] - rw [G.quadInvariant, S.quadSol]⟩ + intro i + simp only [linSolRep_apply_apply_val] + rw [G.quadInvariant, S.quadSol]⟩ mul_smul f1 f2 S := by apply ACCSystemQuad.QuadSols.ext change (G.rep.toFun (f1 * f2)) S.val = _ @@ -107,9 +107,9 @@ lemma rep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) ( /-- The group action acting on solutions to the anomaly cancellation conditions. -/ instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.group χ.Sols where 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]⟩ + simp only [MulAction.toFun_apply] + change χ.cubicACC (G.rep g S.val) = 0 + 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 c908ec5..5dcea41 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean @@ -56,7 +56,7 @@ def toSplitSMPlusH : MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) /-- An equivalence between `(Fin 18 → ℚ)` and `(Fin 6 → Fin 3 → ℚ)`. -/ @[simps!] def toSpeciesMaps' : (Fin 18 → ℚ) ≃ (Fin 6 → Fin 3 → ℚ) := - ((Equiv.curry _ _ _).symm.trans + ((Equiv.curry _ _ _).symm.trans ((@finProdFinEquiv 6 3).arrowCongr (Equiv.refl ℚ))).symm /-- An equivalence between `MSSMCharges.charges` and `(Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ))`. @@ -367,7 +367,7 @@ lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) : rw [add_comm (2 * Hd S * Hd R * Hd L + 2 * Hu S * Hu R * Hu L) _] rw [add_assoc] rw [← add_assoc _ _ (2 * Hd S * Hd R * Hd L + 2 * Hu S * Hu R * Hu L + - (2 * Hd T * Hd R * Hd L + 2 * Hu T * Hu R * Hu L))] + (2 * Hd T * Hd R * Hd L + 2 * Hu T * Hu R * Hu L))] congr 1 rw [← Finset.sum_add_distrib] apply Fintype.sum_congr diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean index 41200ab..d52c855 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean @@ -109,8 +109,8 @@ lemma quad_self_proj (T : MSSMACC.Sols) : lemma quad_proj (T : MSSMACC.Sols) : quadBiLin (proj T.1.1).val (proj T.1.1).val = 2 * dot Y₃.val B₃.val * - ((dot B₃.val T.val - dot Y₃.val T.val) * quadBiLin Y₃.val T.val + - (dot Y₃.val T.val - 2 * dot B₃.val T.val) * quadBiLin B₃.val T.val) := by + ((dot B₃.val T.val - dot Y₃.val T.val) * quadBiLin Y₃.val T.val + + (dot Y₃.val T.val - 2 * dot B₃.val T.val) * quadBiLin B₃.val T.val) := by nth_rewrite 1 [proj_val] repeat rw [quadBiLin.map_add₁] repeat rw [quadBiLin.map_smul₁] @@ -151,7 +151,7 @@ lemma cube_proj_proj_B₃ (T : MSSMACC.LinSols) : rw [cubeTriLin.map_add₂, cubeTriLin.map_smul₁, cubeTriLin.map_smul₂] rw [cubeTriLin.swap₁, cubeTriLin.swap₂, doublePoint_Y₃_B₃] rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.swap₁, cubeTriLin.swap₂, - cubeTriLin.swap₁, doublePoint_B₃_B₃] + cubeTriLin.swap₁, doublePoint_B₃_B₃] rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂] ring diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean index a6da91d..50177fb 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean @@ -48,7 +48,7 @@ lemma planeY₃B₃_eq (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h : a = a' lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R.val ≠ 0) (h : (planeY₃B₃ R a b c).val = (planeY₃B₃ R a' b' c').val) : - a = a' ∧ b = b' ∧ c = c' := by + a = a' ∧ b = b' ∧ c = c' := by rw [planeY₃B₃_val, planeY₃B₃_val] at h have h1 := congrArg (fun S => dot Y₃.val S) h have h2 := congrArg (fun S => dot B₃.val S) h diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean index 3f11e3b..d3a5c3d 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean @@ -43,7 +43,7 @@ instance (R : MSSMACC.AnomalyFreePerp) : Decidable (LineEqProp R) := by apply And.decidable /-- A condition on `Sols` which we will show in `linEqPropSol_iff_proj_linEqProp` that is equivalent - to the condition that the `proj` of the solution satisfies `lineEqProp`. -/ + to the condition that the `proj` of the solution satisfies `lineEqProp`. -/ 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 @@ -338,8 +338,7 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b ring_nf simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add] have h1 : (cubeTriLin T.val.val T.val.val Y₃.val ^ 2 * dot Y₃.val B₃.val ^ 3 * 3 + - dot Y₃.val B₃.val ^ 3 * cubeTriLin T.val.val T.val.val B₃.val ^ 2 - * 3) = cubicCoeff T.val := by + dot Y₃.val B₃.val ^ 3 * cubeTriLin T.val.val T.val.val B₃.val ^ 2* 3) = cubicCoeff T.val := by rw [cubicCoeff] ring rw [h1] @@ -360,7 +359,7 @@ def inQuadCubeToSol : InQuadCube × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R simp) lemma inQuadCubeToSol_smul (R : InQuadCube) (c₁ c₂ c₃ d : ℚ) : - inQuadCubeToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inQuadCubeToSol (R, c₁, c₂, c₃):= by + inQuadCubeToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inQuadCubeToSol (R, c₁, c₂, c₃) := by apply ACCSystem.Sols.ext change (planeY₃B₃ _ _ _ _).val = _ rw [planeY₃B₃_smul] diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean index 3d62794..e5a459b 100644 --- a/HepLean/AnomalyCancellation/PureU1/Basic.lean +++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean @@ -31,8 +31,8 @@ def accGrav (n : ℕ) : ((PureU1Charges n).Charges →ₗ[ℚ] ℚ) where toFun S := ∑ i : Fin n, S i map_add' S T := Finset.sum_add_distrib map_smul' a S := by - simp [HSMul.hSMul, SMul.smul] - rw [← Finset.mul_sum] + simp [HSMul.hSMul, SMul.smul] + rw [← Finset.mul_sum] /-- The symmetric trilinear form used to define the cubic anomaly. -/ @[simps!] @@ -95,7 +95,7 @@ def PureU1 (n : ℕ) : ACCSystem where cubicACC := PureU1.accCube n /-- An equivalence of vector spaces of charges when the number of fermions is equal. -/ -def pureU1EqCharges {n m : ℕ} (h : n = m): +def pureU1EqCharges {n m : ℕ} (h : n = m) : (PureU1 n).Charges ≃ₗ[ℚ] (PureU1 m).Charges where toFun f := f ∘ Fin.cast h.symm invFun f := f ∘ Fin.cast h diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean index a3290f5..eb11981 100644 --- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean @@ -24,14 +24,11 @@ namespace BasisLinear last position. -/ @[simp] def asCharges (j : Fin n) : (PureU1 n.succ).Charges := - (fun i => - if i = j.castSucc then - 1 - else - if i = Fin.last n then - - 1 - else - 0) + (fun i => + if i = j.castSucc then 1 + else if i = Fin.last n then + - 1 + else 0) lemma asCharges_eq_castSucc (j : Fin n) : asCharges j (Fin.castSucc j) = 1 := by @@ -123,7 +120,7 @@ def asBasis : Basis (Fin n) ℚ ((PureU1 n.succ).LinSols) where repr := coordinateMap instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) := - Module.Finite.of_basis asBasis + Module.Finite.of_basis asBasis lemma finrank_AnomalyFreeLinear : FiniteDimensional.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean index 2087c4d..795653a 100644 --- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean +++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean @@ -96,7 +96,7 @@ lemma is_zero (h0 : S (0 : Fin n.succ) = 0) : S = 0 := by /-- A boundary of `S : (PureU1 n.succ).charges` (assumed sorted, constAbs and non-zero) is defined as a element of `k ∈ Fin n` such that `S k.castSucc` and `S k.succ` are different signs. - -/ +-/ @[simp] def Boundary (S : (PureU1 n.succ).Charges) (k : Fin n) : Prop := S k.castSucc < 0 ∧ 0 < S k.succ diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean index 575717d..06f2707 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean @@ -550,7 +550,7 @@ def Pa' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n.succ)).LinSols : ∑ i, f i • basisa i lemma Pa'_P'_P!' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : - Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr):= by + Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr) := by exact Fintype.sum_sum_type _ lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by @@ -617,7 +617,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : Pa' f = Pa' f' ↔ f = simp have h2 : ∀ i, (f i + (- f' i)) = 0 := by exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n) - (fun i => f i + -f' i) h1 + (fun i => f i + -f' i) h1 have h2i := h2 i linarith intro h @@ -685,9 +685,9 @@ lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) : rfl lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by - rw [(mem_span_range_iff_exists_fun ℚ)] - use f - rfl + rw [(mem_span_range_iff_exists_fun ℚ)] + use f + rfl lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin n) : (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈ @@ -700,11 +700,9 @@ lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) (hS : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ) - (h : S.val = P g + P! f): - ∃ - (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ), - S'.val = P g' + P! f' ∧ P! f' = P! f + - (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by + (h : S.val = P g + P! f) : ∃ (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ), + S'.val = P g' + P! f' ∧ P! f' = P! f + + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j have hX : X ∈ Submodule.span ℚ (Set.range (basis!AsCharges)) := by apply Submodule.add_mem @@ -723,10 +721,8 @@ lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) exact hS lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols) - (hS : VectorLikeEven S.val) : - ∃ (M : (FamilyPermutations (2 * n.succ)).group), - (FamilyPermutations (2 * n.succ)).linSolRep M S - ∈ Submodule.span ℚ (Set.range basis) := by + (hS : VectorLikeEven S.val) : ∃ (M : (FamilyPermutations (2 * n.succ)).group), + (FamilyPermutations (2 * n.succ)).linSolRep M S ∈ Submodule.span ℚ (Set.range basis) := by use (Tuple.sort S.val).symm change sortAFL S ∈ Submodule.span ℚ (Set.range basis) rw [mem_span_range_iff_exists_fun ℚ] diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean index 7a5db47..afeb271 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean @@ -49,23 +49,23 @@ lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1 simp only [TriLinearSymm.toCubic_add] at h1 simp only [HomogeneousCubic.map_smul, - accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 + accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 erw [P_accCube, P!_accCube] at h1 rw [← h1] ring /-- - This lemma states that for a given `S` of type `(PureU1 (2 * n.succ)).AnomalyFreeLinear` and - a proof `h` that the line through `S` lies on a cubic curve, - for any functions `g : Fin n.succ → ℚ` and `f : Fin n → ℚ`, if `S.val = P g + P! f`, - then `accCubeTriLinSymm.toFun (P g, P g, P! f) = 0`. +This lemma states that for a given `S` of type `(PureU1 (2 * n.succ)).AnomalyFreeLinear` and +a proof `h` that the line through `S` lies on a cubic curve, +for any functions `g : Fin n.succ → ℚ` and `f : Fin n → ℚ`, if `S.val = P g + P! f`, +then `accCubeTriLinSymm.toFun (P g, P g, P! f) = 0`. -/ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by intro g f hS linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) - - (lineInCubic_expand h g f hS 1 2) / 6 + (lineInCubic_expand h g f hS 1 2) / 6 /-- A `LinSol` satisfies `LineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/ def LineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop := diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean index b24b6c6..836d868 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean @@ -49,15 +49,15 @@ lemma parameterizationAsLinear_val (g : Fin n.succ → ℚ) (f : Fin n → ℚ) change a • (_ • (P' g).val + _ • (P!' f).val) = _ rw [P'_val, P!'_val] -lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ): +lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) : accCube (2* n.succ) (parameterizationAsLinear g f a).val = 0 := by change accCubeTriLinSymm.toCubic _ = 0 rw [parameterizationAsLinear_val, HomogeneousCubic.map_smul, TriLinearSymm.toCubic_add, HomogeneousCubic.map_smul, HomogeneousCubic.map_smul] erw [P_accCube, P!_accCube] rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃] + accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, + accCubeTriLinSymm.map_smul₃] ring /-- The construction of a `Sol` from a `Fin n.succ → ℚ`, a `Fin n → ℚ` and a `ℚ`. -/ @@ -112,7 +112,7 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) : GenericCase S ∨ SpecialCase S := by obtain ⟨g, f, h⟩ := span_basis S.1.1 have h1 : accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0 ∨ - accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by + accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by exact ne_or_eq _ _ cases h1 <;> rename_i h1 exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩) @@ -142,8 +142,8 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols} erw [P_accCube, P!_accCube] have h := h g f hS rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃] + accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, + accCubeTriLinSymm.map_smul₃] rw [h] rw [anomalyFree_param _ _ hS] at h simp at h diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean index a4e8557..fe7c187 100644 --- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean +++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean @@ -89,7 +89,7 @@ lemma lineInPlaneCond_eq_last {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols intro a linarith have ht : S.val ((Fin.last n.succ.succ.succ).succ) = - - S.val ((Fin.last n.succ.succ.succ).castSucc) := by + - S.val ((Fin.last n.succ.succ.succ).castSucc) := by rw [← mul_right_inj' hx] simp [Nat.succ_eq_add_one] simp at h diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean index dd877c7..d8ef7b7 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean @@ -535,7 +535,7 @@ def Pa' (f : (Fin n) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basisa i lemma Pa'_P'_P!' (f : (Fin n) ⊕ (Fin n) → ℚ) : - Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr):= by + Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr) := by exact Fintype.sum_sum_type _ lemma P'_val (f : Fin n → ℚ) : (P' f).val = P f := by @@ -602,7 +602,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔ simp have h2 : ∀ i, (f i + (- f' i)) = 0 := by exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n) - (fun i => f i + -f' i) h1 + (fun i => f i + -f' i) h1 have h2i := h2 i linarith intro h @@ -671,15 +671,15 @@ lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) : lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ) (hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep - (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g f : Fin n.succ → ℚ) (hS1 : S.val = P g + P! f): + (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g f : Fin n.succ → ℚ) (hS1 : S.val = P g + P! f) : ∃ (g' f' : Fin n.succ → ℚ), - S'.val = P g' + P! f' ∧ P! f' = P! f + + S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j have hf : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by - rw [(mem_span_range_iff_exists_fun ℚ)] - use f - rfl + rw [(mem_span_range_iff_exists_fun ℚ)] + use f + rfl have hP : (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by apply Submodule.smul_mem diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean index fc447c5..bc3bb0e 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean @@ -49,7 +49,7 @@ lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1 simp only [TriLinearSymm.toCubic_add] at h1 simp only [HomogeneousCubic.map_smul, - accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 + accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 erw [P_accCube, P!_accCube] at h1 rw [← h1] ring @@ -59,7 +59,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by intro g f hS linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) - - (lineInCubic_expand h g f hS 1 2) / 6 + (lineInCubic_expand h g f hS 1 2) / 6 /-- A `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/ def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop := @@ -119,8 +119,8 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} have h2 := Pa_δa₂ f g 0 rw [← hS] at h1 h2 h4 simp at h2 - have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0):= by - linear_combination -(1 * h1) - 1 * h4 - 1 * h2 + have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0) := by + linear_combination -(1 * h1) - 1 * h4 - 1 * h2 rw [h5] rw [δa₄_δ!₂] have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean index 36fbdfe..38b78a5 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean @@ -44,7 +44,7 @@ lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) : change a • (_ • (P' g).val + _ • (P!' f).val) = _ rw [P'_val, P!'_val] -lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ): +lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ) : (accCube (2 * n + 1)) (parameterizationAsLinear g f a).val = 0 := by change accCubeTriLinSymm.toCubic _ = 0 rw [parameterizationAsLinear_val] @@ -53,8 +53,8 @@ lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ): rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul] erw [P_accCube g, P!_accCube f] rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃] + accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, + accCubeTriLinSymm.map_smul₃] ring /-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a solution. -/ @@ -111,7 +111,7 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) : GenericCase S ∨ SpecialCase S := by obtain ⟨g, f, h⟩ := span_basis S.1.1 have h1 : accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0 ∨ - accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by + accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by exact ne_or_eq _ _ cases h1 <;> rename_i h1 exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩) @@ -143,8 +143,8 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols} erw [P!_accCube] have h := h g f hS rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, - accCubeTriLinSymm.map_smul₃] + accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, + accCubeTriLinSymm.map_smul₃] rw [h] rw [anomalyFree_param _ _ hS] at h simp at h diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean index 73865f2..997b96c 100644 --- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean +++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean @@ -310,8 +310,8 @@ lemma Prop_two (P : ℚ × ℚ → Prop) {S : (PureU1 n).LinSols} rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply] at h1 simp at h1 change P - (S.val ((permTwo hij hab).toFun a), - S.val ((permTwo hij hab).toFun b)) at h1 + (S.val ((permTwo hij hab).toFun a), + S.val ((permTwo hij hab).toFun b)) at h1 erw [permTwo_fst,permTwo_snd] at h1 exact h1 @@ -325,11 +325,11 @@ lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols} intro i j k hij hjk hik have h1 := h (permThree hij hjk hik hab hbc hac).symm rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply, - FamilyPermutations_anomalyFreeLinear_apply] at h1 + FamilyPermutations_anomalyFreeLinear_apply] at h1 simp at h1 change P - (S.val ((permThree hij hjk hik hab hbc hac).toFun a), - S.val ((permThree hij hjk hik hab hbc hac).toFun b), + (S.val ((permThree hij hjk hik hab hbc hac).toFun a), + S.val ((permThree hij hjk hik hab hbc hac).toFun b), S.val ((permThree hij hjk hik hab hbc hac).toFun c)) at h1 erw [permThree_fst,permThree_snd, permThree_thd] at h1 exact h1 diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sort.lean index e986648..fa3c36a 100644 --- a/HepLean/AnomalyCancellation/PureU1/Sort.lean +++ b/HepLean/AnomalyCancellation/PureU1/Sort.lean @@ -24,7 +24,7 @@ variable {n : ℕ} /-- 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 + ∀ i j (_ : i ≤ j), S i ≤ S j /-- Given a charge assignment `S`, the corresponding sorted charge assignment. -/ @[simp] diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean index 3b50b95..3abcb12 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean @@ -46,7 +46,7 @@ lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) : have h1 := SU2Sol S.1.1 have h2 := SU3Sol S.1.1 simp only [accSU2, SMSpecies_numberCharges, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, - Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk, accSU3] at h1 h2 + Finset.sum_singleton, LinearMap.coe_mk, AddHom.coe_mk, accSU3] at h1 h2 erw [hQ] at h1 h2 simp_all linear_combination 3 * h2 diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean index 5319158..617ea11 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean @@ -116,8 +116,8 @@ lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0) def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where toFun S := S.asLinear invFun S := ⟨SMCharges.Q S.val (0 : Fin 1), (SMCharges.U S.val (0 : Fin 1) - - SMCharges.D S.val (0 : Fin 1))/2, - SMCharges.E S.val (0 : Fin 1)⟩ + SMCharges.D S.val (0 : Fin 1))/2, + SMCharges.E S.val (0 : Fin 1)⟩ left_inv S := by apply linearParameters.ext rfl @@ -134,7 +134,7 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where intro i rw [asLinear_val] funext j - have hj : j = (0 : Fin 1):= by + have hj : j = (0 : Fin 1) := by simp only [Fin.isValue] ext simp @@ -284,7 +284,7 @@ lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection (FLTThree : FermatLastTheoremWith ℚ 3) : S.v = 0 ∨ S.w = 0 := by rw [S.cubic] at h - have h1 : (-1)^3 = (-1 : ℚ):= by rfl + have h1 : (-1)^3 = (-1 : ℚ) := by rfl rw [← h1] at h by_contra hn simp [not_or] at hn diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean index b77269d..2619530 100644 --- a/HepLean/AnomalyCancellation/SM/Permutations.lean +++ b/HepLean/AnomalyCancellation/SM/Permutations.lean @@ -70,7 +70,7 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Cha ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by rw [repCharges_toSpecies] exact Fintype.sum_equiv (f⁻¹ j) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) x) - (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl) + (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl) lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges) : accGrav (repCharges f S) = accGrav S := diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean index b2c6d6f..7455ada 100644 --- a/HepLean/AnomalyCancellation/SMNu/Basic.lean +++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean @@ -260,7 +260,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂ lemma quadBiLin_decomp (S T : (SMνCharges n).Charges) : quadBiLin S T = ∑ i, Q S i * Q T i - 2 * ∑ i, U S i * U T i + - ∑ i, D S i * D T i - ∑ i, L S i * L T i + ∑ i, E S i * E T i := by + ∑ i, D S i * D T i - ∑ i, L S i * L T i + ∑ i, E S i * E T i := by erw [← quadBiLin.toFun_eq_coe] rw [quadBiLin] simp only [quadBiLin, BiLinearSymm.mk₂, AddHom.toFun_eq_coe, AddHom.coe_mk, LinearMap.coe_mk] diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean index f060ca6..323c06b 100644 --- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean +++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean @@ -213,7 +213,7 @@ lemma familyUniversal_cubeTriLin (S : (SMνCharges 1).Charges) (T R : (SMνCharg lemma familyUniversal_cubeTriLin' (S T : (SMνCharges 1).Charges) (R : (SMνCharges n).Charges) : cubeTriLin (familyUniversal n S) (familyUniversal n T) R = 6 * S (0 : Fin 6) * T (0 : Fin 6) * ∑ i, Q R i + - 3 * S (1 : Fin 6) * T (1 : Fin 6) * ∑ i, U R i + 3 * S (1 : Fin 6) * T (1 : Fin 6) * ∑ i, U R i + 3 * S (2 : Fin 6) * T (2 : Fin 6) * ∑ i, D R i + 2 * S (3 : Fin 6) * T (3 : Fin 6) * ∑ i, L R i + S (4 : Fin 6) * T (4 : Fin 6) * ∑ i, E R i + S (5 : Fin 6) * T (5 : Fin 6) * ∑ i, N R i := by diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean index 31849b5..2891537 100644 --- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean +++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean @@ -86,7 +86,7 @@ lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) : def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols := linearToQuad (a • S.1 + b • (BL n).1.1) (add_quad S a b) -lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S := by +lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := by simp [addQuad, linearToQuad] rfl diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean index 8bb3b3d..e0f92b1 100644 --- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean +++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean @@ -24,7 +24,7 @@ open BigOperators /-- A proposition which is true if for a given `n`, a plane of charges of dimension `n` exists in which each point is a solution. -/ def ExistsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).Charges), - LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) + LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) : ∃ (B : Fin 11 ⊕ Fin n → (PlusU1 3).Charges), LinearIndependent ℚ B := by @@ -38,7 +38,7 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) : rw [@add_eq_zero_iff_eq_neg] at hg rw [← @Finset.sum_neg_distrib] at hg have h1 : ∑ x : Fin n, -(g (Sum.inr x) • Y (Sum.inr x)) = - ∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x):= by + ∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x) := by apply Finset.sum_congr simp only intro i _ diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean index 765e79d..d2fce6f 100644 --- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean +++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean @@ -84,7 +84,7 @@ lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) : def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols := linearToQuad (a • S.1 + b • (Y n).1.1) (add_quad S a b) -lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S := by +lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := by simp [addQuad, linearToQuad] rfl diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean index 29ceb4a..6695f91 100644 --- a/HepLean/FeynmanDiagrams/Basic.lean +++ b/HepLean/FeynmanDiagrams/Basic.lean @@ -92,7 +92,7 @@ def preimageType' {𝓥 : Type} (v : 𝓥) : Over 𝓥 ⥤ Type where def preimageVertex {𝓔 𝓥 : Type} (v : 𝓥) : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where obj f := Over.mk (fun x => Prod.fst (f.hom x.1) : - (P.toVertex ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel) + (P.toVertex ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel) map {f g} F := Over.homMk ((P.toVertex ⋙ preimageType' v).map F) (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1) @@ -101,7 +101,7 @@ def preimageVertex {𝓔 𝓥 : Type} (v : 𝓥) : def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where obj f := Over.mk (fun x => Prod.fst (f.hom x.1) : - (P.toEdge ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel) + (P.toEdge ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel) map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F) (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1) @@ -173,11 +173,11 @@ instance preimageEdgeDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : | isFalse h => isFalse h instance preimageVertexDecidable {𝓔 𝓥 : Type} (v : 𝓥) - (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] : + (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] : DecidableEq ((P.preimageVertex v).obj F).left := Subtype.instDecidableEq instance preimageEdgeDecidable {𝓔 𝓥 : Type} (v : 𝓔) - (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] : + (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] : DecidableEq ((P.preimageEdge v).obj F).left := Subtype.instDecidableEq instance preimageVertexFintype {𝓔 𝓥 : Type} [DecidableEq 𝓥] @@ -378,7 +378,7 @@ instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} ( /-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/ def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel) (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) - (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥): FeynmanDiagram P where + (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) : FeynmanDiagram P where 𝓔𝓞 := Over.mk 𝓔𝓞 𝓥𝓞 := Over.mk 𝓥𝓞 𝓱𝓔To𝓔𝓥 := Over.mk 𝓱𝓔To𝓔𝓥 @@ -674,7 +674,7 @@ instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Fintype F.SymmetryType Fintype.ofEquiv _ F.symmetryTypeEquiv.symm /-- The symmetry factor can be defined as the cardinal of the symmetry type. - In general this is not a finite number. -/ + In general this is not a finite number. -/ @[simp] def cardSymmetryFactor : Cardinal := Cardinal.mk (F.SymmetryType) @@ -705,7 +705,7 @@ A feynman diagram is connected if its simple graph is connected. -/ /-- A relation on the vertices of Feynman diagrams. The proposition is true if the two - vertices are not equal and are connected by a single edge. -/ + vertices are not equal and are connected by a single edge. -/ @[simp] def AdjRelation : F.𝓥 → F.𝓥 → Prop := fun x y => x ≠ y ∧ diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean index b23fcdb..ddeefde 100644 --- a/HepLean/FeynmanDiagrams/Momentum.lean +++ b/HepLean/FeynmanDiagrams/Momentum.lean @@ -45,7 +45,7 @@ We define the direct sum of the edge and vertex momentum spaces. -/ /-- The type which assocaites to each half-edge a `1`-dimensional vector space. - Corresponding to that spanned by its momentum. -/ + Corresponding to that spanned by its momentum. -/ def HalfEdgeMomenta : Type := F.𝓱𝓔 → ℝ instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup @@ -78,7 +78,7 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] LinearMap.smul_apply] /-- The type which associates to each edge a `1`-dimensional vector space. - Corresponding to that spanned by its total outflowing momentum. -/ + Corresponding to that spanned by its total outflowing momentum. -/ def EdgeMomenta : Type := F.𝓔 → ℝ instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup @@ -86,7 +86,7 @@ instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _ /-- The type which assocaites to each ege a `1`-dimensional vector space. - Corresponding to that spanned by its total inflowing momentum. -/ + Corresponding to that spanned by its total inflowing momentum. -/ def VertexMomenta : Type := F.𝓥 → ℝ instance : AddCommGroup F.VertexMomenta := Pi.addCommGroup @@ -125,7 +125,7 @@ We define various maps into `F.HalfEdgeMomenta`. In particular, we define a map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta`. This map represents the space orthogonal (with respect to the standard Euclidean inner product) to the allowed momenta of half-edges (up-to an offset determined by the - external momenta). +external momenta). The number of loops of a diagram is defined as the number of half-edges minus the rank of this matrix. @@ -147,7 +147,7 @@ def vertexToHalfEdgeMomenta : F.VertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta wher map_smul' _ _ := rfl /-- The linear map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta` induced by - `F.edgeToHalfEdgeMomenta` and `F.vertexToHalfEdgeMomenta`. -/ + `F.edgeToHalfEdgeMomenta` and `F.vertexToHalfEdgeMomenta`. -/ def edgeVertexToHalfEdgeMomenta : F.EdgeVertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta := DirectSum.toModule ℝ (Fin 2) F.HalfEdgeMomenta (fun i => match i with | 0 => F.edgeToHalfEdgeMomenta | 1 => F.vertexToHalfEdgeMomenta) @@ -163,7 +163,7 @@ allowed momenta. -/ /-- The submodule of `F.HalfEdgeMomenta` corresponding to the range of - `F.edgeVertexToHalfEdgeMomenta`. -/ + `F.edgeVertexToHalfEdgeMomenta`. -/ def orthogHalfEdgeMomenta : Submodule ℝ F.HalfEdgeMomenta := LinearMap.range F.edgeVertexToHalfEdgeMomenta diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean index fced370..39132dd 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean @@ -293,47 +293,47 @@ def VAbs (i j : Fin 3) : Quotient CKMMatrixSetoid → ℝ := Quotient.lift (fun V => VAbs' V i j) (VAbs'_equiv i j) /-- The absolute value of the `ud`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VudAbs := VAbs 0 0 /-- The absolute value of the `us`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VusAbs := VAbs 0 1 /-- The absolute value of the `ub`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VubAbs := VAbs 0 2 /-- The absolute value of the `cd`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VcdAbs := VAbs 1 0 /-- The absolute value of the `cs`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VcsAbs := VAbs 1 1 /-- The absolute value of the `cb`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VcbAbs := VAbs 1 2 /-- The absolute value of the `td`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VtdAbs := VAbs 2 0 /-- The absolute value of the `ts`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VtsAbs := VAbs 2 1 /-- The absolute value of the `tb`th element of a representative of an equivalence class of - CKM matrices. -/ + CKM matrices. -/ @[simp] abbrev VtbAbs := VAbs 2 2 @@ -372,7 +372,7 @@ def Rcdcb (V : CKMMatrix) : ℂ := [V]cd / [V]cb /-- The ratio of the `cd` and `cb` elements of a CKM matrix. -/ scoped[CKMMatrix] notation (name := cd_cb_ratio) "[" V "]cd|cb" => Rcdcb V -lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cd = Rcdcb V * [V]cb := by +lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0) : [V]cd = Rcdcb V * [V]cb := by rw [Rcdcb] exact (div_mul_cancel₀ (V.1 1 0) h).symm @@ -382,7 +382,7 @@ def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb /-- The ratio of the `cs` and `cb` elements of a CKM matrix. -/ scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V -lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cs = Rcscb V * [V]cb := by +lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0) : [V]cs = Rcscb V * [V]cb := by rw [Rcscb] exact (div_mul_cancel₀ [V]cs h).symm diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean index 386fe0c..9aaa3b3 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean @@ -49,8 +49,8 @@ def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ := Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv /-- An invariant for CKM mtrices corresponding to the square of the absolute values - of the `us`, `ub` and `cb` elements multipled together divied by `(VudAbs V ^ 2 + VusAbs V ^2)` . - -/ + of the `us`, `ub` and `cb` elements multipled together divied by `(VudAbs V ^ 2 + VusAbs V ^2)` . +-/ def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ := VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2) diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean index 98abb1a..32a8bed 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean @@ -165,7 +165,7 @@ def FstRowThdColRealCond (U : CKMMatrix) : Prop := [U]ud = VudAbs ⟦U⟧ ∧ [U there is no phase difference between the `t`th-row and the cross product of the conjugates of the `u`th and `c`th rows, and the `cd`th and `cs`th elements are real and related in a set way. - -/ +-/ def ubOnePhaseCond (U : CKMMatrix) : Prop := [U]ud = 0 ∧ [U]us = 0 ∧ [U]cb = 0 ∧ [U]ub = 1 ∧ [U]t = conj [U]u ×₃ conj [U]c ∧ [U]cd = - VcdAbs ⟦U⟧ ∧ [U]cs = √(1 - VcdAbs ⟦U⟧ ^ 2) diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean index ffb291b..8fbca35 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean @@ -100,8 +100,8 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : parameterization of CKM matrices. -/ def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix := ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by - rw [mem_unitaryGroup_iff'] - exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩ + rw [mem_unitaryGroup_iff'] + exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩ namespace standParam lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : @@ -158,7 +158,7 @@ lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Rea VusVubVcdSq ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ = Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2 := by simp only [VusVubVcdSq, VusAbs, VAbs, VAbs', Fin.isValue, standParam, standParamAsMatrix, - neg_mul, Quotient.lift_mk, cons_val', cons_val_one, head_cons, + neg_mul, Quotient.lift_mk, cons_val', cons_val_one, head_cons, empty_val', cons_val_fin_one, cons_val_zero, _root_.map_mul, VubAbs, cons_val_two, tail_cons, VcbAbs, VudAbs, Complex.abs_ofReal] by_cases hx : Real.cos θ₁₃ ≠ 0 diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean index 64716b7..77f1d0d 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean @@ -142,17 +142,17 @@ lemma S₂₃_eq_ℂsin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.sin ( (ofReal_sin _).symm.trans (congrArg ofReal (S₂₃_eq_sin_θ₂₃ V)) lemma complexAbs_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : - Complex.abs (Complex.sin (θ₁₂ V)) = sin (θ₁₂ V):= by + Complex.abs (Complex.sin (θ₁₂ V)) = sin (θ₁₂ V) := by rw [S₁₂_eq_ℂsin_θ₁₂, Complex.abs_ofReal, ofReal_inj, abs_eq_self] exact S₁₂_nonneg _ lemma complexAbs_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : - Complex.abs (Complex.sin (θ₁₃ V)) = sin (θ₁₃ V):= by + Complex.abs (Complex.sin (θ₁₃ V)) = sin (θ₁₃ V) := by rw [S₁₃_eq_ℂsin_θ₁₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self] exact S₁₃_nonneg _ lemma complexAbs_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : - Complex.abs (Complex.sin (θ₂₃ V)) = sin (θ₂₃ V):= by + Complex.abs (Complex.sin (θ₂₃ V)) = sin (θ₂₃ V) := by rw [S₂₃_eq_ℂsin_θ₂₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self] exact S₂₃_nonneg _ @@ -185,19 +185,19 @@ lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos ( simp [C₂₃] lemma complexAbs_cos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₂ V)) = - cos (θ₁₂ V):= by + cos (θ₁₂ V) := by rw [C₁₂_eq_ℂcos_θ₁₂, Complex.abs_ofReal] simp only [ofReal_inj, abs_eq_self] exact Real.cos_arcsin_nonneg _ lemma complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₃ V)) = - cos (θ₁₃ V):= by + cos (θ₁₃ V) := by rw [C₁₃_eq_ℂcos_θ₁₃, Complex.abs_ofReal] simp only [ofReal_inj, abs_eq_self] exact Real.cos_arcsin_nonneg _ lemma complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₂₃ V)) = - cos (θ₂₃ V):= by + cos (θ₂₃ V) := by rw [C₂₃_eq_ℂcos_θ₂₃, Complex.abs_ofReal] simp only [ofReal_inj, abs_eq_self] exact Real.cos_arcsin_nonneg _ @@ -349,10 +349,10 @@ lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) : lemma mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = 0 ↔ - VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0 := by + VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0 := by rw [VudAbs_eq_C₁₂_mul_C₁₃, VubAbs_eq_S₁₃, VusAbs_eq_S₁₂_mul_C₁₃, VcbAbs_eq_S₂₃_mul_C₁₃, - VtbAbs_eq_C₂₃_mul_C₁₃, ← ofReal_inj, - ← ofReal_inj, ← ofReal_inj, ← ofReal_inj, ← ofReal_inj] + VtbAbs_eq_C₂₃_mul_C₁₃, ← ofReal_inj, + ← ofReal_inj, ← ofReal_inj, ← ofReal_inj, ← ofReal_inj] simp only [ofReal_mul] rw [← S₁₃_eq_ℂsin_θ₁₃, ← S₁₂_eq_ℂsin_θ₁₂, ← S₂₃_eq_ℂsin_θ₂₃, ← C₁₃_eq_ℂcos_θ₁₃, ← C₂₃_eq_ℂcos_θ₂₃,← C₁₂_eq_ℂcos_θ₁₂] diff --git a/HepLean/Mathematics/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean index af0badd..1d78a7c 100644 --- a/HepLean/Mathematics/SO3/Basic.lean +++ b/HepLean/Mathematics/SO3/Basic.lean @@ -147,7 +147,7 @@ lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by calc det (A.1 - 1) = det (A.1 - A.1 * A.1ᵀ) := by simp [A.2.2] _ = det A.1 * det (1 - A.1ᵀ) := by rw [← det_mul, mul_sub, mul_one] - _ = det (1 - A.1ᵀ):= by simp [A.2.1] + _ = det (1 - A.1ᵀ) := by simp [A.2.1] _ = det (1 - A.1ᵀ)ᵀ := by rw [det_transpose] _ = det (1 - A.1) := by simp _ = det (- (A.1 - 1)) := by simp diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index f9bda99..acfeea5 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -36,7 +36,7 @@ open minkowskiMetric in /-- The Lorentz group is the subset of matrices which preserve the minkowski metric. -/ def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) := {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ | - ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ} + ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ} namespace LorentzGroup /-- Notation for the Lorentz group. -/ diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean index c95ce62..ea2f466 100644 --- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean +++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean @@ -145,7 +145,7 @@ lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ Lor smul_eq_mul, LinearMap.neg_apply] field_simp rw [u.1.2, v.1.2, minkowskiMetric.symm v.1.1 u, minkowskiMetric.symm u y, - minkowskiMetric.symm v y] + minkowskiMetric.symm v y] ring /-- A generalised boost as an element of the Lorentz Group. -/ diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean index 57f479e..a6a8e71 100644 --- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean +++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean @@ -63,7 +63,7 @@ lemma not_orthochronous_iff_le_zero : /-- The continuous map taking a Lorentz transformation to its `0 0` element. -/ def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ, - Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩ + Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩ /-- An auxillary function used in the definition of `orthchroMapReal`. -/ def stepFunction : ℝ → ℝ := fun t => @@ -72,7 +72,7 @@ def stepFunction : ℝ → ℝ := fun t => lemma stepFunction_continuous : Continuous stepFunction := by apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_const continuous_id) - <;> intro a ha + <;> intro a ha rw [@Set.Iic_def, @frontier_Iic, @Set.mem_singleton_iff] at ha rw [ha] simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte] @@ -157,7 +157,7 @@ def orthchroRep : LorentzGroup d →* ℤ₂ where map_mul' Λ Λ' := by simp only by_cases h : IsOrthochronous Λ - <;> by_cases h' : IsOrthochronous Λ' + <;> by_cases h' : IsOrthochronous Λ' rw [orthchroMap_IsOrthochronous h, orthchroMap_IsOrthochronous h', orthchroMap_IsOrthochronous (mul_othchron_of_othchron_othchron h h')] rfl diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean index 15c753f..e35d763 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean @@ -26,7 +26,7 @@ This will relation should be made explicit in the future. /-! TODO: Generalize to maps into Lorentz tensors. -/ /-- The possible `colors` of an index for a RealLorentzTensor. - There are two possiblities, `up` and `down`. -/ + There are two possiblities, `up` and `down`. -/ inductive RealLorentzTensor.Colors where | up : RealLorentzTensor.Colors | down : RealLorentzTensor.Colors @@ -359,7 +359,7 @@ def splitIndexValue {T : Marked d X n} : (indexValueIso d (Equiv.refl _) T.color_eq_elim).trans indexValueSumEquiv - @[simp] +@[simp] lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X] (P : T.UnmarkedIndexValue × T.MarkedIndexValue → ℝ) : ∑ i, P (splitIndexValue i) = ∑ j, ∑ k, P (j, k) := by diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean index 19e5aa5..5928a52 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean @@ -186,7 +186,7 @@ lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1) S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) = _ trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueSumEquiv i).1 j * T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))* - toTensorRepMat Λ (indexValueSumEquiv i).2 k * + toTensorRepMat Λ (indexValueSumEquiv i).2 k * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) apply Finset.sum_congr rfl (fun x _ => ?_) rw [Finset.sum_mul_sum] @@ -196,7 +196,7 @@ lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1) rw [Finset.sum_comm] trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (indexValueSumEquiv i).1 j * T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))* - toTensorRepMat Λ (indexValueSumEquiv i).2 k * + toTensorRepMat Λ (indexValueSumEquiv i).2 k * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) apply Finset.sum_congr rfl (fun j _ => ?_) rw [Finset.sum_comm] diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean index 072f096..c78afb0 100644 --- a/HepLean/SpaceTime/LorentzVector/NormOne.lean +++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean @@ -277,9 +277,9 @@ lemma metric_continuous (u : LorentzVector d) : (continuous_apply (Sum.inl 0)) (Continuous.comp' continuous_subtype_val continuous_subtype_val) · refine Continuous.comp' continuous_neg $ Continuous.inner - (Continuous.comp' (Pi.continuous_precomp Sum.inr) continuous_const) - (Continuous.comp' (Pi.continuous_precomp Sum.inr) (Continuous.comp' - continuous_subtype_val continuous_subtype_val)) + (Continuous.comp' (Pi.continuous_precomp Sum.inr) continuous_const) + (Continuous.comp' (Pi.continuous_precomp Sum.inr) (Continuous.comp' + continuous_subtype_val continuous_subtype_val)) end FuturePointing diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean index fa10338..9a0cf3e 100644 --- a/HepLean/SpaceTime/MinkowskiMetric.lean +++ b/HepLean/SpaceTime/MinkowskiMetric.lean @@ -328,7 +328,7 @@ lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by · simp [h, LieAlgebra.Orthogonal.indefiniteDiagonal, minkowskiMatrix] exact fun a => False.elim (h (id (Eq.symm a))) -lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d): +lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d) : Λ ν μ = η ν ν * ⟪e ν, Λ *ᵥ e μ⟫ₘ := by rw [on_basis_mulVec, ← mul_assoc] have h1 : η ν ν * η ν ν = 1 := by diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean index f189574..cc5f4df 100644 --- a/HepLean/SpaceTime/SL2C/Basic.lean +++ b/HepLean/SpaceTime/SL2C/Basic.lean @@ -34,7 +34,7 @@ we can define a representation a representation of `SL(2, ℂ)` on spacetime. -/ /-- Given an element `M ∈ SL(2, ℂ)` the linear map from `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` to - itself defined by `A ↦ M * A * Mᴴ`. -/ + itself defined by `A ↦ M * A * Mᴴ`. -/ @[simps!] def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) →ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where @@ -51,7 +51,7 @@ def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) : RingHom.id_apply] /-- The representation of `SL(2, ℂ)` on `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` given by - `M A ↦ M * A * Mᴴ`. -/ + `M A ↦ M * A * Mᴴ`. -/ @[simps!] def repSelfAdjointMatrix : Representation ℝ SL(2, ℂ) $ selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where toFun := toLinearMapSelfAdjointMatrix @@ -103,7 +103,7 @@ lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) @[simps!] def toLorentzGroupElem (M : SL(2, ℂ)) : LorentzGroup 3 := ⟨LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (repLorentzVector M), - by simp [repLorentzVector, iff_det_selfAdjoint]⟩ + by simp [repLorentzVector, iff_det_selfAdjoint]⟩ /-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/ @[simps!] diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean index 25945a4..c081ff0 100644 --- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean +++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean @@ -76,7 +76,7 @@ def unitToLinear : unitary (HiggsVec →L[ℂ] HiggsVec) →* HiggsVec →ₗ[ /-- The representation of the gauge group acting on `higgsVec`. -/ @[simps!] def rep : Representation ℂ GaugeGroup HiggsVec := - unitToLinear.comp (unitaryToLin.comp higgsRepUnitary) + unitToLinear.comp (unitaryToLin.comp higgsRepUnitary) lemma higgsRepUnitary_mul (g : GaugeGroup) (φ : HiggsVec) : (higgsRepUnitary g).1 *ᵥ φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) := by @@ -138,7 +138,7 @@ lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) : rep (rotateGuageGroup hφ) φ = ![0, ofReal ‖φ‖] := by rw [rep_apply] simp only [rotateGuageGroup, rotateMatrix, one_pow, one_smul, - Nat.succ_eq_add_one, Nat.reduceAdd, ofReal_eq_coe] + Nat.succ_eq_add_one, Nat.reduceAdd, ofReal_eq_coe] ext i fin_cases i · simp only [mulVec, Fin.zero_eta, Fin.isValue, cons_val', empty_val', cons_val_fin_one, diff --git a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean index 7f43491..e1b7fc6 100644 --- a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean +++ b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean @@ -55,8 +55,7 @@ lemma innerProd_left_zero (φ : HiggsField) : ⟪0, φ⟫_H = 0 := by lemma innerProd_right_zero (φ : HiggsField) : ⟪φ, 0⟫_H = 0 := by funext x simp [innerProd] -example (x : ℝ): RCLike.ofReal x = ofReal' x := by - rfl + lemma innerProd_expand (φ1 φ2 : HiggsField) : ⟪φ1, φ2⟫_H = fun x => equivRealProdCLM.symm (((φ1 x 0).re * (φ2 x 0).re + (φ1 x 1).re * (φ2 x 1).re+ (φ1 x 0).im * (φ2 x 0).im + (φ1 x 1).im * (φ2 x 1).im), diff --git a/HepLean/StandardModel/Representations.lean b/HepLean/StandardModel/Representations.lean index 8990980..be53819 100644 --- a/HepLean/StandardModel/Representations.lean +++ b/HepLean/StandardModel/Representations.lean @@ -32,7 +32,7 @@ noncomputable def repU1Map (g : unitary ℂ) : unitaryGroup (Fin 2) ℂ := simp only [one_pow, one_smul]⟩ /-- The 2d representation of U(1) with charge 3 as a homomorphism - from U(1) to `unitaryGroup (Fin 2) ℂ`. -/ + from U(1) to `unitaryGroup (Fin 2) ℂ`. -/ @[simps!] noncomputable def repU1 : unitary ℂ →* unitaryGroup (Fin 2) ℂ where toFun g := repU1Map g diff --git a/scripts/hepLean_style_lint.lean b/scripts/hepLean_style_lint.lean index 405c457..7d0b2fd 100644 --- a/scripts/hepLean_style_lint.lean +++ b/scripts/hepLean_style_lint.lean @@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith -/ import Lean import Mathlib.Tactic.Linter.TextBased +import Batteries.Data.Array.Merge /-! # HepLean style linter @@ -60,7 +61,17 @@ def substringLinter (s : String) : HepLeanTextLinter := fun lines ↦ Id.run do let col := match k with | none => 1 | some k => String.offsetOfPos l k.stopPos - some (s!" Found instance of substring {s}.", lno, col) + some (s!" Found instance of substring `{s}`.", lno, col) + else none) + errors.toArray + +/-- Number of space at new line must be even. -/ +def numInitialSpacesEven : HepLeanTextLinter := fun lines ↦ Id.run do + let enumLines := (lines.toList.enumFrom 1) + let errors := enumLines.filterMap (fun (lno, l) ↦ + let numSpaces := (l.takeWhile (· == ' ')).length + if numSpaces % 2 != 0 then + some (s!"Number of initial spaces is not even.", lno, 1) else none) errors.toArray @@ -78,18 +89,18 @@ def printErrors (errors : Array HepLeanErrorContext) : IO Unit := do for e in errors do IO.println (s!"error: {e.path}:{e.lineNumber}:{e.columnNumber}: {e.error}") -def hepLeanLintFile (path : FilePath) : IO Bool := do +def hepLeanLintFile (path : FilePath) : IO (Array HepLeanErrorContext) := do let lines ← IO.FS.lines path let allOutput := (Array.map (fun lint ↦ (Array.map (fun (e, n, c) ↦ HepLeanErrorContext.mk e n c path)) (lint lines))) - #[doubleEmptyLineLinter, doubleSpaceLinter, substringLinter ".-/", substringLinter " )", + #[doubleEmptyLineLinter, doubleSpaceLinter, numInitialSpacesEven, + substringLinter ".-/", substringLinter " )", substringLinter "( ", substringLinter "=by", substringLinter " def ", substringLinter "/-- We ", substringLinter "[ ", substringLinter " ]", substringLinter " ," , substringLinter "by exact ", - substringLinter "⟨ ", substringLinter " ⟩"] + substringLinter "⟨ ", substringLinter " ⟩", substringLinter "):"] let errors := allOutput.flatten - printErrors errors - return errors.size > 0 + return errors def main (_ : List String) : IO UInt32 := do initSearchPath (← findSysroot) @@ -99,13 +110,19 @@ def main (_ : List String) : IO UInt32 := do unless (← mFile.pathExists) do throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist" let (hepLeanMod, _) ← readModuleData mFile - let mut warned := false - for imp in hepLeanMod.imports do - if imp.module == `Init then continue - let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean" - if ← hepLeanLintFile filePath then - warned := true - if warned then + let filePaths := hepLeanMod.imports.filterMap (fun imp ↦ + if imp.module == `Init then + none + else + some ((mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean")) + let errors := (← filePaths.mapM hepLeanLintFile).flatten + let errorMessagesPresent := (errors.map (fun e => e.error)).sortDedup + for eM in errorMessagesPresent do + IO.println s!"\n\nError: {eM}" + for e in errors do + if e.error == eM then + IO.println s!"{e.path}:{e.lineNumber}:{e.columnNumber}: {e.error}" + if errors.size > 0 then throw <| IO.userError s!"Errors found." else IO.println "No linting issues found."