diff --git a/home_page/_layouts/default.html b/home_page/_layouts/default.html index 4e9e01f..ca29568 100644 --- a/home_page/_layouts/default.html +++ b/home_page/_layouts/default.html @@ -17,6 +17,7 @@ {% else %} {% endif %} + {% include mathjax.html %} {% include head-custom.html %} @@ -47,4 +48,4 @@

{{ page.description | default: site.description | de - \ No newline at end of file + diff --git a/home_page/index.md b/home_page/index.md index dfeed32..36e2b24 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -12,6 +12,7 @@ meta-twitter:card: summary meta-twitter:title: AQFT in Lean meta-viewport: width=device-width, initial-scale=1 title: Formalising AQFT in Lean +usemathjax: true --- # AQFT in Lean @@ -95,7 +96,7 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: **GNS Construction** - Cauchy–Schwarz inequality for states -- Equivalence of the two descriptions of the left-ideal \$\$\mathcal{N}\$\$; \$\$\mathcal{N}\$\$ is a closed linear subspace +- Equivalence of the two descriptions of the left-ideal $$\mathcal{N}$$; $$\mathcal{N}$$ is a closed linear subspace - Full GNS Construction Theorem (Hilbert space, \*-representation, cyclic vector, faithfulness, uniqueness up to unitary equivalence) - Separating vector of a faithful state @@ -127,9 +128,9 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: - Einstein Causality in a representation, curved spacetime (Theorem 93) **KMS condition** -- Boundary coincidence for \$\$a = 1\$\$ -- \$\$i\beta\$\$-periodic entire extension (strip Schwarz reflection) -- Strip-Liouville holds for \$\$\beta > 0\$\$ +- Boundary coincidence for $$a = 1$$ +- $$i\beta$$-periodic entire extension (strip Schwarz reflection) +- Strip-Liouville holds for $$\beta > 0$$ - KMS states are invariant (Theorem 83) - Uniqueness on the strip from boundary values; uniqueness of the KMS correlation function - A Killing flow induces a one-parameter automorphism group