DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Add mathjax

Browse source
This commit is contained in:
jstoobysmith 2024-12-06 06:52:44 +00:00
parent 00d1076356
commit 91ac919067
3 changed files with 25 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

20
HepLean/Meta/Notes/ToHTML.lean
View file

@ -125,6 +125,20 @@ def codeButton : String := "
}
</style>
"
def mathJaxScript : String := "
<!-- MathJax code -->
<script type=\"text/javascript\">
window.MathJax = {
tex: {
inlineMath: [['$', '$']], // Use $...$ for inline math
displayMath: [['$$', '$$']] // Use $$...$$ for block math
}
};
</script>
<script type=\"text/javascript\" id=\"MathJax-script\" async
src=\"https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js\">
</script>
"
/-- The header to the html code. -/
def headerHTML : String :=
@ -133,7 +147,7 @@ layout: default
---
<!DOCTYPE html>
<html>
<head>" ++ codeBlockHTML ++ informalDefStyle ++ codeButton ++ "</head>
<head>" ++ codeBlockHTML ++ mathJaxScript ++ informalDefStyle ++ codeButton ++ "</head>
</head>
<body>"
@ -147,11 +161,11 @@ def titleHTML : String :=
def leanNote : String := "
<br>
<div style=\"border: 1px solid black; padding: 10px;\">
<p>Note: These are are not ordinary notes. They are created using an interactive theorem
<p>Note: These are not ordinary notes. They are created using an interactive theorem
prover called <a href=\"https://lean-lang.org\">Lean</a>.
Lean formally checks definitions, theorems and proofs for correctness.
These notes are part of a much larger project called
<a href=\"https://github.com/HEPLean/HepLean\">HepLean</a>., which aims to digitalize
<a href=\"https://github.com/HEPLean/HepLean\">HepLean</a>, which aims to digitalize
high energy physics into Lean. Please consider contributing to this project.
<br><br>
Please provide feedback or suggestions for improvements by creating a GitHub issue

8
HepLean/PerturbationTheory/Wick/Algebra.lean
View file

@ -25,8 +25,12 @@ We will formally define the operator ring, in terms of the fields present in the
-/
note "
<h1>Operator algebra</h1>
This is a test note."
<h2>Operator algebra</h2>
The operator algebra is a super-algebra over the complex numbers, which acts on
the Hilbert space of the theory. A super-algebra is an algebra with a Z/2 grading.
To do pertubation theory in a QFT we need a need some basic properties of the operator algebra,
$A$.
"
namespace Wick

3
HepLean/PerturbationTheory/Wick/Species.lean
View file

@ -29,7 +29,8 @@ The first bit of data we need is a type of fields `𝓯`. We also need to know w
are dual to what other fields, for example in a complex scalar theory `φ` is dual to `φ†`.
We can encode this information in an involution `ξ : 𝓯 → 𝓯`.
<br><br>
...
The second bit of data we need is how the fields interact with each other. In other words,
a list of interaction vertices `𝓘`, and the type of fields associated to each vertex.
<br><br>
This necessary information to do perturbation theory is encoded in a `Wick Species`, which
we define as: