Charges associated with a potential term #
Given a potential term T
, and a charge x : Charges
,
we can extract the set of charges associated with instances of that potential term.
def
SuperSymmetry.SU5.Charges.ofPotentialTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
(x : Charges 𝓩)
(T : PotentialTerm)
:
Multiset 𝓩
Given a charges x : Charges
associated to the representations, and a potential
term T
, the charges associated with instances of that potential term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm_mono
{𝓩 : Type}
[AddCommGroup 𝓩]
{x y : Charges 𝓩}
(h : x ⊆ y)
(T : PotentialTerm)
:
@[simp]
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm_empty
{𝓩 : Type}
[AddCommGroup 𝓩]
(T : PotentialTerm)
:
def
SuperSymmetry.SU5.Charges.ofPotentialTerm'
{𝓩 : Type}
[AddCommGroup 𝓩]
(y : Charges 𝓩)
(T : PotentialTerm)
:
Multiset 𝓩
Given a charges x : Charges
associated to the representations, and a potential
term T
, the charges associated with instances of that potential term.
This is a more explicit form of PotentialTerm
, which has the benifit that
it is quick with decide
, but it is not defined based on more fundamental
concepts, like ofPotentialTerm
is.
Equations
- One or more equations did not get rendered due to their size.
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.μ = match y.1, y.2.1 with | none, x => ∅ | x, none => ∅ | some qHd, some qHu => {qHd - qHu}
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.β = match y.2.1 with | none => ∅ | some qHu => Multiset.map (fun (x : 𝓩) => -qHu + x) y.2.2.1.val
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.Λ = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2) (y.2.2.1.product (y.2.2.1.product y.2.2.2)).val
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.W3 = match y.2.1 with | none => ∅ | some qHu => Multiset.map (fun (x : 𝓩 × 𝓩) => -qHu - qHu + x.1 + x.2) (y.2.2.1.product y.2.2.1).val
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.K1 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => -x.1 + x.2.1 + x.2.2) (y.2.2.1.product (y.2.2.2.product y.2.2.2)).val
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.K2 = match y.1, y.2.1 with | none, x => ∅ | x, none => ∅ | some qHd, some qHu => Multiset.map (fun (x : 𝓩) => qHd + qHu + x) y.2.2.2.val
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.topYukawa = match y.2.1 with | none => ∅ | some qHu => Multiset.map (fun (x : 𝓩 × 𝓩) => -qHu + x.1 + x.2) (y.2.2.2.product y.2.2.2).val
- y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.bottomYukawa = match y.1 with | none => ∅ | some qHd => Multiset.map (fun (x : 𝓩 × 𝓩) => qHd + x.1 + x.2) (y.2.2.1.product y.2.2.2).val
Instances For
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_μ_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.μ = Multiset.map (fun (x : 𝓩 × 𝓩) => x.1 - x.2) (x.1.toFinset.product x.2.1.toFinset).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_β_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.β = Multiset.map (fun (x : 𝓩 × 𝓩) => -x.1 + x.2) (x.2.1.toFinset.product x.2.2.1).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_W2_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.W2 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2.1 + x.2.2.2)
(x.1.toFinset.product (x.2.2.2.product (x.2.2.2.product x.2.2.2))).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_W3_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.W3 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => -x.1 - x.1 + x.2.1 + x.2.2)
(x.2.1.toFinset.product (x.2.2.1.product x.2.2.1)).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_W4_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.W4 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 - x.2.1 - x.2.1 + x.2.2)
(x.1.toFinset.product (x.2.1.toFinset.product x.2.2.1)).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_K2_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.K2 = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2) (x.1.toFinset.product (x.2.1.toFinset.product x.2.2.2)).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_topYukawa_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.topYukawa = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => -x.1 + x.2.1 + x.2.2) (x.2.1.toFinset.product (x.2.2.2.product x.2.2.2)).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_bottomYukawa_finset
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
:
x.ofPotentialTerm' PotentialTerm.bottomYukawa = Multiset.map (fun (x : 𝓩 × 𝓩 × 𝓩) => x.1 + x.2.1 + x.2.2) (x.1.toFinset.product (x.2.2.1.product x.2.2.2)).val
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm_subset_ofPotentialTerm'
{𝓩 : Type}
[AddCommGroup 𝓩]
{x : Charges 𝓩}
(T : PotentialTerm)
:
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_subset_ofPotentialTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{x : Charges 𝓩}
(T : PotentialTerm)
:
theorem
SuperSymmetry.SU5.Charges.mem_ofPotentialTerm_iff_mem_ofPotentialTerm
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{T : PotentialTerm}
{n : 𝓩}
{y : Charges 𝓩}
:
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_mono
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{x y : Charges 𝓩}
(h : x ⊆ y)
(T : PotentialTerm)
:
@[simp]
theorem
SuperSymmetry.SU5.Charges.ofPotentialTerm'_empty
{𝓩 : Type}
[AddCommGroup 𝓩]
(T : PotentialTerm)
: