From 8300033b9f1fb288101c8ce88666b19342609084 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 7 Jun 2024 14:37:09 -0400
Subject: [PATCH] feat: Add 2HDM potential

---
 HepLean.lean                                  |  1 +
 .../BeyondTheStandardModel/TwoHDM/Basic.lean  | 29 +++++++++++++++++++
 HepLean/StandardModel/HiggsBoson/Basic.lean   |  4 +++
 3 files changed, 34 insertions(+)
 create mode 100644 HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean

diff --git a/HepLean.lean b/HepLean.lean
index 474955b..8972e40 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -47,6 +47,7 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
 import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
+import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
new file mode 100644
index 0000000..731a40c
--- /dev/null
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.StandardModel.HiggsBoson.Basic
+
+namespace TwoHDM
+
+open StandardModel
+open ComplexConjugate
+
+noncomputable section
+
+/-- The potential of the two Higgs doublet model.  -/
+def potential (Φ1 Φ2 : higgsField)
+    (m11Sq m22Sq lam₁ lam₂ lam₃ lam₄ : ℝ) (m12Sq lam₅ lam₆ lam₇ : ℂ) (x : spaceTime) : ℝ :=
+  m11Sq * Φ1.normSq x  + m22Sq * Φ2.normSq x
+  - (m12Sq * (Φ1.innerProd Φ2) x + conj m12Sq * (Φ2.innerProd Φ1) x).re
+  + 1/2 * lam₁ * Φ1.normSq x ^ 2 + 1/2 * lam₂ * Φ2.normSq x ^ 2
+  + lam₃ * Φ1.normSq x * Φ2.normSq x
+  + lam₄ * ‖Φ1.innerProd Φ2 x‖
+  + (1/2 * lam₅ * (Φ1.innerProd Φ2) x ^ 2 + 1/2 * conj lam₅ * (Φ2.innerProd Φ1) x ^ 2).re
+  + (lam₆ * Φ1.normSq x * (Φ1.innerProd Φ2) x + conj lam₆ * Φ1.normSq x * (Φ2.innerProd Φ1) x).re
+  + (lam₇ * Φ2.normSq x * (Φ1.innerProd Φ2) x + conj lam₇ * Φ2.normSq x * (Φ2.innerProd Φ1) x).re
+
+
+end
+end TwoHDM
diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean
index da76073..7805c98 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -100,6 +100,10 @@ lemma apply_im_smooth (φ : higgsField) (i : Fin 2):
     Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : spaceTime) =>  (φ x i))) :=
   Smooth.comp (ContinuousLinearMap.smooth imCLM) (φ.apply_smooth i)
 
+/-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
+def innerProd (φ1 φ2 : higgsField) : spaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
+
+
 /-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the
  higgs vector.  -/
 @[simp]