From 2fb2c6db81f26ee3b0a4969cec54f1648fd537ad Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 19 Jun 2024 13:17:23 -0400 Subject: [PATCH] docs: Add docs for sections to be done. --- HepLean/FeynmanDiagrams/Momentum.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean index 2152a68..bf68321 100644 --- a/HepLean/FeynmanDiagrams/Momentum.lean +++ b/HepLean/FeynmanDiagrams/Momentum.lean @@ -191,5 +191,29 @@ allowed space of half-edge momenta. of the space of allowed Half-loop momenta. -/ noncomputable def numberOfLoops : ℕ := FiniteDimensional.finrank ℝ F.allowedHalfEdgeMomenta +/-! + +## Lemmas regarding `numberOfLoops` + +We now give a series of lemmas which be used to help calculate the number of loops +for specific Feynman diagrams. + +### TODO + +- Complete this section. + + +-/ + +/-! + +## Category theory + +### TODO + +- Complete this section. + + +-/ end FeynmanDiagram