`BookProof.SmHiggsVacuum.higgs_goldstone` {lam mu2 : ℝ} {u w : E} (hu : lam * ‖u‖ ^ 2 = mu2) (hperp : (inner ℝ u w : ℝ) = 0) (t : ℝ) : higgsV lam mu2 (u + t • w) = higgsV lam mu2 u
ProvedBookProof.SmHiggsVacuum.higgs_goldstonetheoremstimepiece
Prove the following Lean 4 theorem from ChapterSmHiggsVacuum.
BookProof.SmHiggsVacuum.higgs_goldstone {lam mu2 : ℝ} {u w : E} (hu : lam * ‖u‖ ^ 2 = mu2) (hperp : (inner ℝ u w : ℝ) = 0) (t : ℝ) : higgsV lam mu2 (u + t • w) = higgsV lam mu2 u + (lam / 4) * t ^ 4 * ‖w‖ ^ 4
Formalization note: Lean 4 identifier BookProof.SmHiggsVacuum.higgs_goldstone.
Preamble
-- Generated from ChapterSmHiggsVacuum.lean — theorem BookProof.SmHiggsVacuum.higgs_goldstone
import Mathlib
import Definitions.Def_ChapterSmHiggsVacuum
open BookProof.SmHiggsVacuum
open Finset
noncomputable section
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]Formal statement
theorem BookProof.SmHiggsVacuum.higgs_goldstone {lam mu2 : ℝ} {u w : E} (hu : lam * ‖u‖ ^ 2 = mu2)
(hperp : (inner ℝ u w : ℝ) = 0) (t : ℝ) :
higgsV lam mu2 (u + t • w) = higgsV lam mu2 u + (lam / 4) * t ^ 4 * ‖w‖ ^ 4 := by sorry