PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar

Feynman diagrams in a complex scalar field theory #

source
def PhiFour.complexScalarFeynmanRules :
PreFeynmanRule

The pre-Feynman rules for a complex scalar theory.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem PhiFour.complexScalarFeynmanRules_edgeLabelMap (x : Fin 1) :
    complexScalarFeynmanRules.edgeLabelMap x = match x with | 0 => CategoryTheory.Over.mk ![0, 1]
    source
    @[simp]
    theorem PhiFour.complexScalarFeynmanRules_vertexLabelMap (x : Fin 3) :
    complexScalarFeynmanRules.vertexLabelMap x = match x with | 0 => CategoryTheory.Over.mk ![0] | 1 => CategoryTheory.Over.mk ![1] | 2 => CategoryTheory.Over.mk ![0, 0, 1, 1]
    source
    @[simp]
    theorem PhiFour.complexScalarFeynmanRules_EdgeLabel :
    complexScalarFeynmanRules.EdgeLabel = Fin 1
    source
    @[simp]
    theorem PhiFour.complexScalarFeynmanRules_HalfEdgeLabel :
    complexScalarFeynmanRules.HalfEdgeLabel = Fin 2
    source
    @[simp]
    theorem PhiFour.complexScalarFeynmanRules_VertexLabel :
    complexScalarFeynmanRules.VertexLabel = Fin 3
    source
    instance PhiFour.instOfNatEdgeLabelComplexScalarFeynmanRules (a : ℕ) :
    OfNat complexScalarFeynmanRules.EdgeLabel a

    An instance allowing us to use integers for edge labels for complex scalar theory.

    Equations
    source
    instance PhiFour.instOfNatHalfEdgeLabelComplexScalarFeynmanRules (a : ℕ) :
    OfNat complexScalarFeynmanRules.HalfEdgeLabel a

    An instance allowing us to use integers for half-edge labels for complex scalar theory.

    Equations
    source
    instance PhiFour.instOfNatVertexLabelComplexScalarFeynmanRules (a : ℕ) :
    OfNat complexScalarFeynmanRules.VertexLabel a

    An instance allowing us to use integers for vertex labels for complex scalar theory.

    Equations
    source
    instance PhiFour.instIsFinitePreFeynmanRuleComplexScalarFeynmanRules :
    complexScalarFeynmanRules.IsFinitePreFeynmanRule

    The pre feynman rules for complex scalars are finite.

    Equations
    • One or more equations did not get rendered due to their size.