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

Merge branch 'master' into Docs

Browse source
This commit is contained in:
jstoobysmith 2025-01-23 14:22:25 +00:00
commit fca75098f1
18 changed files with 163 additions and 314 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/AnomalyCancellation/Basic.lean
View file

@ -14,7 +14,7 @@ This file defines the basic structures for the anomaly cancellation conditions.
It defines a module structure on the charges, and the solutions to the linear ACCs.
-/
TODO "Derive an ACC system from a guage algebra and fermionic representations."
TODO "Derive an ACC system from a gauge algebra and fermionic representations."
TODO "Relate ACC Systems to algebraic varieties."
TODO "Refactor whole file, and dependent files."

36
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
View file

@ -286,11 +286,8 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
/-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
AnomalyFreeMk' (lineCube R.val.val a₁ a₂ a₃)
(by
erw [planeY₃B₃_quad]
rw [R.prop.1, R.prop.2.1, R.prop.2.2]
simp)
(lineCube_cube R.val.val a₁ a₂ a₃)
(by erw [planeY₃B₃_quad, R.prop.1, R.prop.2.1, R.prop.2.2]; simp)
(lineCube_cube R.val.val a₁ a₂ a₃)
lemma inQuadToSol_smul (R : InQuad) (c₁ c₂ c₃ d : ℚ) :
inQuadToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inQuadToSol (R, c₁, c₂, c₃) := by
@ -314,9 +311,7 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
rw [inQuadProj, inQuadToSol_smul]
apply ACCSystem.Sols.ext
change _ • (planeY₃B₃ _ _ _ _).val = _
rw [planeY₃B₃_val]
rw [Y₃_plus_B₃_plus_proj]
rw [cube_proj, cube_proj_proj_B₃, cube_proj_proj_Y₃]
rw [planeY₃B₃_val, Y₃_plus_B₃_plus_proj, cube_proj, cube_proj_proj_B₃, cube_proj_proj_Y₃]
ring_nf
simp only [zero_smul, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add]
have h1 : (cubeTriLin T.val.val T.val.val Y₃.val ^ 2 * dot Y₃.val B₃.val ^ 3 * 3 +
@ -331,14 +326,8 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
/-- Given a element of `inQuadCube × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
def inQuadCubeToSol : InQuadCube × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, b₁, b₂, b₃) =>
AnomalyFreeMk' (planeY₃B₃ R.val.val.val b₁ b₂ b₃)
(by
rw [planeY₃B₃_quad]
rw [R.val.prop.1, R.val.prop.2.1, R.val.prop.2.2]
simp)
(by
rw [planeY₃B₃_cubic]
rw [R.prop.1, R.prop.2.1, R.prop.2.2]
simp)
(by rw [planeY₃B₃_quad, R.val.prop.1, R.val.prop.2.1, R.val.prop.2.2]; simp)
(by rw [planeY₃B₃_cubic, R.prop.1, R.prop.2.1, R.prop.2.2]; simp)
lemma inQuadCubeToSol_smul (R : InQuadCube) (c₁ c₂ c₃ d : ℚ) :
inQuadCubeToSol (R, (d * c₁), (d * c₂), (d * c₃)) = d • inQuadCubeToSol (R, c₁, c₂, c₃) := by
@ -361,8 +350,7 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
rw [inQuadCubeProj, inQuadCubeToSol_smul]
apply ACCSystem.Sols.ext
change _ • (planeY₃B₃ _ _ _ _).val = _
rw [planeY₃B₃_val]
rw [Y₃_plus_B₃_plus_proj]
rw [planeY₃B₃_val, Y₃_plus_B₃_plus_proj]
ring_nf
simp only [Fin.isValue, Fin.reduceFinMk, zero_smul, add_zero, zero_add]
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel₀]
@ -389,8 +377,7 @@ lemma toSol_toSolNSProj (T : NotInLineEqSol) :
use toSolNSProj T.val
have h1 : ¬ LineEqProp (toSolNSProj T.val).1 :=
(linEqPropSol_iff_proj_linEqProp T.val).mpr.mt T.prop
rw [toSol]
simp_all
simp_rw [toSol, h1]
exact toSolNS_proj T
lemma toSol_inLineEq (T : InLineEqSol) : ∃ X, toSol X = T.val := by
@ -398,8 +385,7 @@ lemma toSol_inLineEq (T : InLineEqSol) : ∃ X, toSol X = T.val := by
use ⟨X.1.val, X.2.1, X.2.2⟩
have : ¬ InQuadProp X.1.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mpr.mt T.prop.2
have : LineEqProp X.1.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1
rw [toSol]
simp_all
simp_all only [toSol]
exact inLineEqToSol_proj T
lemma toSol_inQuad (T : InQuadSol) : ∃ X, toSol X = T.val := by
@ -408,8 +394,7 @@ lemma toSol_inQuad (T : InQuadSol) : ∃ X, toSol X = T.val := by
have : ¬ InCubeProp X.1.val.val := (inCubeSolProp_iff_proj_inCubeProp T.val).mpr.mt T.prop.2.2
have : InQuadProp X.1.val.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1
have : LineEqProp X.1.val.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1
rw [toSol]
simp_all
simp_all only [toSol]
exact inQuadToSol_proj T
lemma toSol_inQuadCube (T : InQuadCubeSol) : ∃ X, toSol X = T.val := by
@ -418,8 +403,7 @@ lemma toSol_inQuadCube (T : InQuadCubeSol) : ∃ X, toSol X = T.val := by
have : InCubeProp X.1.val.val.val := (inCubeSolProp_iff_proj_inCubeProp T.val).mp T.prop.2.2
have : InQuadProp X.1.val.val.val := (inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1
have : LineEqProp X.1.val.val.val := (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1
rw [toSol]
simp_all
simp_all only [toSol]
exact inQuadCubeToSol_proj T
theorem toSol_surjective : Function.Surjective toSol := by

2
HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
View file

@ -136,7 +136,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
rw [P_P_P!_accCube' g f hfg] at h1
simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1
cases h1 <;> rename_i h1
· apply Or.inl
· left
linear_combination h1
· cases h1 <;> rename_i h1
· refine Or.inr (Or.inl ?_)

2
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -123,7 +123,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
rw [P_P_P!_accCube' g f hfg] at h1
simp only [Nat.succ_eq_add_one, mul_eq_zero] at h1
cases h1 <;> rename_i h1
· apply Or.inl
· left
linear_combination h1
· cases h1 <;> rename_i h1
· refine Or.inr (Or.inl ?_)

2
HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
View file

@ -75,7 +75,7 @@ lemma swap_fields : P.toFun Φ1 Φ2 =
normSq_apply_im_zero, mul_zero, zero_add, RingHomCompTriple.comp_apply, RingHom.id_apply]
ring_nf
simp only [one_div, add_left_inj, add_right_inj, mul_eq_mul_left_iff]
apply Or.inl
left
rw [HiggsField.innerProd, HiggsField.innerProd, ← InnerProductSpace.conj_symm, Complex.abs_conj]
/-- If `Φ₂` is zero the potential reduces to the Higgs potential on `Φ₁`. -/

8
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
View file

@ -69,8 +69,7 @@ section sines
/-- For a CKM matrix `sin θ₁₂` is non-negative. -/
lemma S₁₂_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₂ V := by
rw [S₁₂, div_nonneg_iff]
apply Or.inl
apply (And.intro (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))
exact .inl (.intro (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))
/-- For a CKM matrix `sin θ₁₃` is non-negative. -/
lemma S₁₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₃ V :=
@ -82,8 +81,7 @@ lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by
· rw [S₂₃, if_pos ha]
exact VAbs_ge_zero 1 0 V
· rw [S₂₃, if_neg ha, @div_nonneg_iff]
apply Or.inl
apply And.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2))
exact .inl (.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))
/-- For a CKM matrix `sin θ₁₂` is less then or equal to 1. -/
lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
@ -95,7 +93,7 @@ lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
cases' h2 with h2 h2
simp_all
exact h2
apply Or.inl
left
simp_all only [VudAbs, VusAbs, or_true, Real.sqrt_pos, true_and]
rw [Real.le_sqrt (VAbs_ge_zero 0 1 V) (le_of_lt h3)]
simp only [Fin.isValue, le_add_iff_nonneg_left]

2
HepLean/Lorentz/Group/Boosts.lean
View file

@ -150,7 +150,7 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
Pi.smul_apply, smul_eq_mul, Pi.sub_apply, Pi.neg_apply]
apply Or.inl
left
ring
open minkowskiMatrix in

2
HepLean/Lorentz/Group/Rotations.lean
View file

@ -11,7 +11,7 @@ import HepLean.Mathematics.SO3.Basic
This file describes the embedding of `SO(3)` into `LorentzGroup 3`.
-/
TODO "Generalize the inclusion of rotations into LorentzGroup to abitary dimension."
TODO "Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension."
noncomputable section
namespace LorentzGroup

65
HepLean/Mathematics/Fin/Involutions.lean
View file

@ -208,8 +208,7 @@ def involutionAddEquiv {n : ℕ} (f : {f : Fin n → Fin n // Function.Involutiv
simp_all only [Subtype.coe_eta] }
let s : Finset (Fin n) := Finset.univ.filter fun i => f.1 i = i
let e2' : { i : Fin n // f.1 i = i} ≃ {i // i ∈ s} := by
refine Equiv.subtypeEquivProp ?h
funext i
apply Equiv.subtypeEquivProp
simp [s]
let e2 : {i // i ∈ s} ≃ Fin (Finset.card s) := by
refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
@ -242,7 +241,7 @@ lemma involutionAddEquiv_cast {n : ℕ} {f1 f2 : {f : Fin n → Fin n // Functio
involutionAddEquiv f1 = (Equiv.subtypeEquivRight (by rw [hf]; simp)).trans
((involutionAddEquiv f2).trans (Equiv.optionCongr (finCongr (by rw [hf])))) := by
subst hf
simp only [finCongr_refl, Equiv.optionCongr_refl, Equiv.trans_refl]
rw [finCongr_refl, Equiv.optionCongr_refl]
rfl
lemma involutionAddEquiv_cast' {m : ℕ} {f1 f2 : {f : Fin m → Fin m // Function.Involutive f}}
@ -259,33 +258,18 @@ lemma involutionAddEquiv_none_succ {n : ℕ}
(h : involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none)
(x : Fin n) : f.1 x.succ = x.succ ↔ (involutionCons n f).1.1 x = x := by
simp only [succ_eq_add_one, involutionCons, Fin.cons_update, Equiv.coe_fn_mk, dite_eq_left_iff]
have hn' := involutionAddEquiv_none_image_zero h
have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ n⟩:= by
rw [← hn']
exact fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn)
apply Iff.intro
· intro h2 h3
rw [Fin.ext_iff]
simp [h2]
· intro h2
have h2' := h2 hx
conv_rhs => rw [← h2']
simp
have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ n⟩:=
involutionAddEquiv_none_image_zero h ▸
fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn)
exact Iff.intro (fun h2 ↦ by simp [h2]) (fun h2 ↦ (Fin.pred_eq_iff_eq_succ hx).mp (h2 hx))
lemma involutionAddEquiv_isSome_image_zero {n : ℕ} :
{f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}}
→ (involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2).isSome
→ ¬ f.1 ⟨0, Nat.zero_lt_succ n⟩ = ⟨0, Nat.zero_lt_succ n⟩ := by
intro f hf
simp only [succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv,
Option.isSome_some, Option.get_some, Option.isSome_none, Equiv.trans_apply,
Equiv.optionCongr_apply, Equiv.coe_trans, RelIso.coe_fn_toEquiv, Option.isSome_map'] at hf
simp_all only [List.length_cons, Fin.zero_eta]
obtain ⟨val, property⟩ := f
simp_all only [List.length_cons]
apply Aesop.BuiltinRules.not_intro
intro a
simp_all only [↓reduceDIte, Option.isSome_none, Bool.false_eq_true]
intro f hf a
simp only [succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv] at hf
simp_all
/-!
@ -303,15 +287,11 @@ def involutionNoFixedEquivSum {n : ℕ} :
∧ (∀ i, f i ≠ i) ∧ f 0 = k.succ} where
toFun f := ⟨(f.1 0).pred (f.2.2 0), ⟨f.1, f.2.1, by simpa using f.2.2⟩⟩
invFun f := ⟨f.2.1, ⟨f.2.2.1, f.2.2.2.1⟩⟩
left_inv f := by
rfl
left_inv f := rfl
right_inv f := by
simp only [succ_eq_add_one, ne_eq, mul_eq]
ext
· simp only [Fin.coe_pred]
rw [f.2.2.2.2]
simp
· simp
· simp [f.2.2.2.2]
· rfl
/-- The condition on fixed point free involutions of `Fin n.succ` for a fixed value of `f 0`,
can be modified by conjugation with an equivalence. -/
@ -329,8 +309,7 @@ def involutionNoFixedZeroSetEquivEquiv {n : ℕ}
intro i
simp only [succ_eq_add_one, Function.comp_apply, ne_eq, Equiv.apply_symm_apply]
have hf2 := f.2.1 i
simpa using hf2, by
simpa using f.2.2.1, by simpa using f.2.2.2⟩
simpa using hf2, by simpa using f.2.2.1, by simpa using f.2.2.2⟩
left_inv f := by
ext i
simp
@ -485,7 +464,7 @@ def involutionNoFixedSetOne {n : ℕ} :
simp [Fin.ext_iff] at h
| ⟨(Nat.succ (Nat.succ m)), h⟩ =>
simp only [succ_eq_add_one, ne_eq, Fin.ext_iff, Fin.val_succ, add_left_inj, f']
have hf:= f.2.2 ⟨m, by exact Nat.add_lt_add_iff_right.mp h⟩
have hf:= f.2.2 ⟨m, Nat.add_lt_add_iff_right.mp h⟩
simp only [ne_eq, Fin.ext_iff] at hf
omega
· simp only [succ_eq_add_one, ne_eq, f']
@ -505,13 +484,9 @@ def involutionNoFixedSetOne {n : ℕ} :
ext i
simp only
split
· simp only [Fin.val_one, succ_eq_add_one, Fin.zero_eta]
rw [f.2.2.2]
simp
· simp only [Fin.val_zero, succ_eq_add_one, Fin.mk_one]
rw [hf1]
simp
· rfl
· simp [Fin.val_one, succ_eq_add_one, Fin.zero_eta, f.2.2.2]
· exact congrArg Fin.val (id (Eq.symm hf1))
· exact rfl
right_inv f := by
simp only [ne_eq, mul_eq, succ_eq_add_one, Function.comp_apply]
ext i
@ -521,8 +496,7 @@ def involutionNoFixedSetOne {n : ℕ} :
simp [Fin.ext_iff] at h
· rename_i h
simp [Fin.ext_iff] at h
· rename_i h
simp only [Fin.val_succ, add_tsub_cancel_right]
· simp only [Fin.val_succ, add_tsub_cancel_right]
congr
apply congrArg
simp_all [Fin.ext_iff]
@ -552,8 +526,7 @@ def involutionNoFixedZeroEquivProd {n : ℕ} :
≃ Fin n.succ ×
{f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
refine Equiv.trans involutionNoFixedEquivSumSame ?_
exact Equiv.sigmaEquivProd (Fin n.succ)
{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i}
exact Equiv.sigmaEquivProd (Fin n.succ) { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
/-!

2
HepLean/Mathematics/List.lean
View file

@ -707,7 +707,7 @@ lemma eraseIdx_get {I : Type} (l : List I) (i : Fin l.length) :
ext x
simp only [Function.comp_apply, List.get_eq_getElem, List.eraseIdx, List.getElem_eraseIdx]
simp only [Fin.succAbove, Fin.coe_cast]
by_cases hi: x.castSucc < Fin.cast (by exact Eq.symm (eraseIdx_length l i)) i
by_cases hi: x.castSucc < Fin.cast (Eq.symm (eraseIdx_length l i)) i
· simp only [hi, ↓reduceIte, Fin.coe_castSucc, dite_eq_left_iff, not_lt]
intro h
rw [Fin.lt_def] at hi

2
HepLean/Mathematics/List/InsertionSort.lean
View file

@ -34,7 +34,7 @@ lemma insertionSortMin_lt_mem_insertionSortDropMinPos {α : Type} (r : α → α
(i : Fin (insertionSortDropMinPos r a l).length) :
r (insertionSortMin r a l) ((insertionSortDropMinPos r a l)[i]) := by
let l1 := List.insertionSort r (a :: l)
have hl1 : l1.Sorted r := by exact List.sorted_insertionSort r (a :: l)
have hl1 : l1.Sorted r := List.sorted_insertionSort r (a :: l)
simp only [l1] at hl1
rw [insertionSort_eq_insertionSortMin_cons r a l] at hl1
simp only [List.sorted_cons, List.mem_insertionSort] at hl1

63
HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean
View file

@ -61,12 +61,10 @@ lemma ofCrAnList_cons (φ : 𝓕.CrAnStates) (φs : List 𝓕.CrAnStates) :
lemma ofCrAnList_append (φs φs' : List 𝓕.CrAnStates) :
ofCrAnList (φs ++ φs') = ofCrAnList φs * ofCrAnList φs' := by
dsimp only [ofCrAnList]
rw [List.map_append, List.prod_append]
simp [ofCrAnList, List.map_append]
lemma ofCrAnList_singleton (φ : 𝓕.CrAnStates) :
ofCrAnList [φ] = ofCrAnState φ := by
simp [ofCrAnList]
ofCrAnList [φ] = ofCrAnState φ := by simp [ofCrAnList]
/-- Maps a state to the sum of creation and annihilation operators in
creation and annihilation free-algebra. -/
@ -94,8 +92,7 @@ lemma ofStateList_cons (φ : 𝓕.States) (φs : List 𝓕.States) :
ofStateList (φ :: φs) = ofState φ * ofStateList φs := rfl
lemma ofStateList_singleton (φ : 𝓕.States) :
ofStateList [φ] = ofState φ := by
simp [ofStateList]
ofStateList [φ] = ofState φ := by simp [ofStateList]
lemma ofStateList_append (φs φs' : List 𝓕.States) :
ofStateList (φs ++ φs') = ofStateList φs * ofStateList φs' := by
@ -104,13 +101,11 @@ lemma ofStateList_append (φs φs' : List 𝓕.States) :
lemma ofStateAlgebra_ofList_eq_ofStateList : (φs : List 𝓕.States) →
ofStateAlgebra (ofList φs) = ofStateList φs
| [] => by
simp [ofStateList]
| [] => by simp [ofStateList]
| φ :: φs => by
rw [ofStateList_cons, StateAlgebra.ofList_cons]
rw [map_mul]
simp only [ofStateAlgebra_ofState, mul_eq_mul_left_iff]
apply Or.inl (ofStateAlgebra_ofList_eq_ofStateList φs)
rw [ofStateList_cons, StateAlgebra.ofList_cons, map_mul, ofStateAlgebra_ofState,
mul_eq_mul_left_iff]
exact .inl (ofStateAlgebra_ofList_eq_ofStateList φs)
lemma ofStateList_sum (φs : List 𝓕.States) :
ofStateList φs = ∑ (s : CrAnSection φs), ofCrAnList s.1 := by
@ -144,21 +139,18 @@ def crPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
@[simp]
lemma crPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
crPart (StateAlgebra.ofState (States.inAsymp φ)) = ofCrAnState ⟨States.inAsymp φ, ()⟩ := by
dsimp only [crPart, StateAlgebra.ofState]
rw [FreeAlgebra.lift_ι_apply]
simp [crPart, StateAlgebra.ofState]
@[simp]
lemma crPart_position (φ : 𝓕.PositionStates) :
crPart (StateAlgebra.ofState (States.position φ)) =
ofCrAnState ⟨States.position φ, CreateAnnihilate.create⟩ := by
dsimp only [crPart, StateAlgebra.ofState]
rw [FreeAlgebra.lift_ι_apply]
simp [crPart, StateAlgebra.ofState]
@[simp]
lemma crPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
crPart (StateAlgebra.ofState (States.outAsymp φ)) = 0 := by
dsimp only [crPart, StateAlgebra.ofState]
rw [FreeAlgebra.lift_ι_apply]
simp [crPart, StateAlgebra.ofState]
/-- The algebra map taking an element of the free-state algbra to
the part of it in the creation and annihilation free algebra
@ -173,36 +165,26 @@ def anPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
@[simp]
lemma anPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
anPart (StateAlgebra.ofState (States.inAsymp φ)) = 0 := by
dsimp only [anPart, StateAlgebra.ofState]
rw [FreeAlgebra.lift_ι_apply]
simp [anPart, StateAlgebra.ofState]
@[simp]
lemma anPart_position (φ : 𝓕.PositionStates) :
anPart (StateAlgebra.ofState (States.position φ)) =
ofCrAnState ⟨States.position φ, CreateAnnihilate.annihilate⟩ := by
dsimp only [anPart, StateAlgebra.ofState]
rw [FreeAlgebra.lift_ι_apply]
simp [anPart, StateAlgebra.ofState]
@[simp]
lemma anPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
anPart (StateAlgebra.ofState (States.outAsymp φ)) = ofCrAnState ⟨States.outAsymp φ, ()⟩ := by
dsimp only [anPart, StateAlgebra.ofState]
rw [FreeAlgebra.lift_ι_apply]
simp [anPart, StateAlgebra.ofState]
lemma ofState_eq_crPart_add_anPart (φ : 𝓕.States) :
ofState φ = crPart (StateAlgebra.ofState φ) + anPart (StateAlgebra.ofState φ) := by
rw [ofState]
cases φ with
| inAsymp φ =>
dsimp only [statesToCrAnType]
simp
| position φ =>
dsimp only [statesToCrAnType]
rw [CreateAnnihilate.sum_eq]
simp
| outAsymp φ =>
dsimp only [statesToCrAnType]
simp
| inAsymp φ => simp [statesToCrAnType]
| position φ => simp [statesToCrAnType, CreateAnnihilate.sum_eq]
| outAsymp φ => simp [statesToCrAnType]
/-!
@ -223,11 +205,9 @@ lemma ofListBasis_eq_ofList (φs : List 𝓕.CrAnStates) :
erw [MonoidAlgebra.lift_apply]
simp only [zero_smul, Finsupp.sum_single_index, one_smul]
rw [@FreeMonoid.lift_apply]
simp only [List.prod]
match φs with
| [] => rfl
| φ :: φs =>
erw [List.map_cons]
| φ :: φs => erw [List.map_cons]
/-!
@ -239,8 +219,7 @@ lemma ofListBasis_eq_ofList (φs : List 𝓕.CrAnStates) :
noncomputable def mulLinearMap : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 where
toFun a := {
toFun := fun b => a * b,
map_add' := fun c d => by
simp [mul_add]
map_add' := fun c d => by simp [mul_add]
map_smul' := by simp}
map_add' := fun a b => by
ext c
@ -251,15 +230,13 @@ noncomputable def mulLinearMap : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕
simp [smul_mul']
lemma mulLinearMap_apply (a b : CrAnAlgebra 𝓕) :
mulLinearMap a b = a * b := by rfl
mulLinearMap a b = a * b := rfl
/-- The linear map associated with scalar-multiplication in `CrAnAlgebra`. -/
noncomputable def smulLinearMap (c : ℂ) : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 where
toFun a := c • a
map_add' := by simp
map_smul' m x := by
simp only [smul_smul, RingHom.id_apply]
rw [NonUnitalNormedCommRing.mul_comm]
map_smul' m x := by simp [smul_smul, RingHom.id_apply, NonUnitalNormedCommRing.mul_comm]
end CrAnAlgebra

237
HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
View file

@ -38,20 +38,16 @@ def normalOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
normalOrder (ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
rw [← ofListBasis_eq_ofList]
simp only [normalOrder, Basis.constr_basis]
rw [← ofListBasis_eq_ofList, normalOrder, Basis.constr_basis]
lemma ofCrAnList_eq_normalOrder (φs : List 𝓕.CrAnStates) :
ofCrAnList (normalOrderList φs) = normalOrderSign φs • normalOrder (ofCrAnList φs) := by
rw [normalOrder_ofCrAnList, normalOrderList]
rw [smul_smul]
simp only [normalOrderSign]
rw [Wick.koszulSign_mul_self]
simp
rw [normalOrder_ofCrAnList, normalOrderList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
one_smul]
lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
rw [← ofCrAnList_nil, normalOrder_ofCrAnList]
simp
rw [← ofCrAnList_nil, normalOrder_ofCrAnList, normalOrderSign_nil, normalOrderList_nil,
ofCrAnList_nil, one_smul]
/-!
@ -63,8 +59,7 @@ lemma normalOrder_ofCrAnList_cons_create (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
normalOrder (ofCrAnList (φ :: φs)) =
ofCrAnState φ * normalOrder (ofCrAnList φs) := by
rw [normalOrder_ofCrAnList]
rw [normalOrderSign_cons_create φ hφ, normalOrderList_cons_create φ hφ φs]
rw [normalOrder_ofCrAnList, normalOrderSign_cons_create φ hφ, normalOrderList_cons_create φ hφ φs]
rw [ofCrAnList_cons, normalOrder_ofCrAnList, mul_smul_comm]
lemma normalOrder_create_mul (φ : 𝓕.CrAnStates)
@ -73,21 +68,18 @@ lemma normalOrder_create_mul (φ : 𝓕.CrAnStates)
normalOrder (ofCrAnState φ * a) = ofCrAnState φ * normalOrder a := by
change (normalOrder ∘ₗ mulLinearMap (ofCrAnState φ)) a =
(mulLinearMap (ofCrAnState φ) ∘ₗ normalOrder) a
refine LinearMap.congr_fun ?h a
apply ofCrAnListBasis.ext
intro l
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
LinearMap.coe_comp, Function.comp_apply]
rw [← ofCrAnList_cons]
rw [normalOrder_ofCrAnList_cons_create φ hφ]
rw [← ofCrAnList_cons, normalOrder_ofCrAnList_cons_create φ hφ]
lemma normalOrder_ofCrAnList_append_annihilate (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnStates) :
normalOrder (ofCrAnList (φs ++ [φ])) =
normalOrder (ofCrAnList φs) * ofCrAnState φ := by
rw [normalOrder_ofCrAnList]
rw [normalOrderSign_append_annihlate φ hφ φs, normalOrderList_append_annihilate φ hφ φs]
rw [ofCrAnList_append, ofCrAnList_singleton, normalOrder_ofCrAnList, smul_mul_assoc]
rw [normalOrder_ofCrAnList, normalOrderSign_append_annihlate φ hφ φs,
normalOrderList_append_annihilate φ hφ φs, ofCrAnList_append, ofCrAnList_singleton,
normalOrder_ofCrAnList, smul_mul_assoc]
lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate)
@ -95,46 +87,35 @@ lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
normalOrder (a * ofCrAnState φ) = normalOrder a * ofCrAnState φ := by
change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φ)) a =
(mulLinearMap.flip (ofCrAnState φ) ∘ₗ normalOrder) a
refine LinearMap.congr_fun ?h a
apply ofCrAnListBasis.ext
intro l
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk]
rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton]
rw [normalOrder_ofCrAnList_append_annihilate φ hφ]
rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton,
normalOrder_ofCrAnList_append_annihilate φ hφ]
lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
normalOrder (crPart (StateAlgebra.ofState φ) * a) =
crPart (StateAlgebra.ofState φ) * normalOrder a := by
match φ with
| .inAsymp φ =>
dsimp only [crPart, StateAlgebra.ofState]
simp only [FreeAlgebra.lift_ι_apply]
rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
exact normalOrder_create_mul ⟨States.inAsymp φ, ()⟩ rfl a
| .position φ =>
dsimp only [crPart, StateAlgebra.ofState]
simp only [FreeAlgebra.lift_ι_apply]
refine normalOrder_create_mul _ ?_ _
simp [crAnStatesToCreateAnnihilate]
| .outAsymp φ =>
simp
rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
exact normalOrder_create_mul _ rfl _
| .outAsymp φ => simp
lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
normalOrder (a * anPart (StateAlgebra.ofState φ)) =
normalOrder a * anPart (StateAlgebra.ofState φ) := by
match φ with
| .inAsymp φ =>
simp
| .inAsymp φ => simp
| .position φ =>
dsimp only [anPart, StateAlgebra.ofState]
simp only [FreeAlgebra.lift_ι_apply]
refine normalOrder_mul_annihilate _ ?_ _
simp [crAnStatesToCreateAnnihilate]
rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
exact normalOrder_mul_annihilate _ rfl _
| .outAsymp φ =>
dsimp only [anPart, StateAlgebra.ofState]
simp only [FreeAlgebra.lift_ι_apply]
refine normalOrder_mul_annihilate _ ?_ _
simp [crAnStatesToCreateAnnihilate]
rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
refine normalOrder_mul_annihilate _ rfl _
/-!
@ -151,9 +132,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.Cr
normalOrder (ofCrAnList φs' * ofCrAnState φa * ofCrAnState φc * ofCrAnList φs) := by
rw [mul_assoc, mul_assoc, ← ofCrAnList_cons, ← ofCrAnList_cons, ← ofCrAnList_append]
rw [normalOrder_ofCrAnList, normalOrderSign_swap_create_annihlate φc φa hφc hφa]
rw [normalOrderList_swap_create_annihlate φc φa hφc hφa]
rw [← smul_smul, ← normalOrder_ofCrAnList]
congr
rw [normalOrderList_swap_create_annihlate φc φa hφc hφa, ← smul_smul, ← normalOrder_ofCrAnList]
rw [ofCrAnList_append, ofCrAnList_cons, ofCrAnList_cons]
noncomm_ring
@ -166,9 +145,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
change (normalOrder ∘ₗ mulLinearMap (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa)) a =
(smulLinearMap _ ∘ₗ normalOrder ∘ₗ
mulLinearMap (ofCrAnList φs * ofCrAnState φa * ofCrAnState φc)) a
refine LinearMap.congr_fun ?h a
apply ofCrAnListBasis.ext
intro l
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
LinearMap.coe_comp, Function.comp_apply, instCommGroup.eq_1]
rw [normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList φc φa hφc hφa]
@ -184,26 +161,20 @@ lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φc * (ofCrAnState φa * b))) a =
(smulLinearMap (𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa)) ∘ₗ
normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φa * (ofCrAnState φc * b))) a
apply LinearMap.congr_fun
apply ofCrAnListBasis.ext
intro l
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) _
simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1]
repeat rw [← mul_assoc]
rw [normalOrder_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1, ← mul_assoc,
normalOrder_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
rfl
lemma normalOrder_superCommute_create_annihilate (φc φa : 𝓕.CrAnStates)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
(a b : 𝓕.CrAnAlgebra) :
normalOrder (a * superCommute (ofCrAnState φc) (ofCrAnState φa) * b) = 0 := by
rw [superCommute_ofCrAnState_ofCrAnState]
simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc]
rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc]
rw [← mul_assoc, ← mul_assoc]
rw [normalOrder_swap_create_annihlate φc φa hφc hφa]
simp only [FieldStatistic.instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
map_smul, sub_self]
simp only [superCommute_ofCrAnState_ofCrAnState, instCommGroup.eq_1, Algebra.smul_mul_assoc]
rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc, ← mul_assoc, ← mul_assoc,
normalOrder_swap_create_annihlate φc φa hφc hφa]
simp
lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
@ -212,8 +183,7 @@ lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
rw [superCommute_ofCrAnState_ofCrAnState_symm]
simp only [instCommGroup.eq_1, neg_smul, mul_neg, Algebra.mul_smul_comm, neg_mul,
Algebra.smul_mul_assoc, map_neg, map_smul, neg_eq_zero, smul_eq_zero]
apply Or.inr
exact normalOrder_superCommute_create_annihilate φc φa hφc hφa a b
exact Or.inr (normalOrder_superCommute_create_annihilate φc φa hφc hφa ..)
lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
normalOrder (a * (crPart (StateAlgebra.ofState φ)) * (anPart (StateAlgebra.ofState φ')) * b) =
@ -221,34 +191,28 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
normalOrder (a * (anPart (StateAlgebra.ofState φ')) *
(crPart (StateAlgebra.ofState φ)) * b) := by
match φ, φ' with
| _, .inAsymp φ' =>
simp
| .outAsymp φ, _ =>
simp
| _, .inAsymp φ' => simp
| .outAsymp φ, _ => simp
| .position φ, .position φ' =>
simp only [crPart_position, anPart_position, instCommGroup.eq_1]
rw [normalOrder_swap_create_annihlate]
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
rfl
rfl
rfl; rfl
| .inAsymp φ, .outAsymp φ' =>
simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1]
rw [normalOrder_swap_create_annihlate]
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
rfl
rfl
rfl; rfl
| .inAsymp φ, .position φ' =>
simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1]
rw [normalOrder_swap_create_annihlate]
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
rfl
rfl
rfl; rfl
| .position φ, .outAsymp φ' =>
simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1]
rw [normalOrder_swap_create_annihlate]
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
rfl
rfl
rfl; rfl
/-!
@ -262,51 +226,45 @@ lemma normalOrder_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
normalOrder (a * (anPart (StateAlgebra.ofState φ)) * (crPart (StateAlgebra.ofState φ')) * b) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • normalOrder (a * (crPart (StateAlgebra.ofState φ')) *
(anPart (StateAlgebra.ofState φ)) * b) := by
rw [normalOrder_swap_crPart_anPart]
rw [smul_smul, FieldStatistic.exchangeSign_symm, FieldStatistic.exchangeSign_mul_self]
simp
simp [normalOrder_swap_crPart_anPart, smul_smul]
lemma normalOrder_superCommute_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
normalOrder (a * superCommute
(crPart (StateAlgebra.ofState φ)) (anPart (StateAlgebra.ofState φ')) * b) = 0 := by
match φ, φ' with
| _, .inAsymp φ' =>
simp
| .outAsymp φ', _ =>
simp
| _, .inAsymp φ' => simp
| .outAsymp φ', _ => simp
| .position φ, .position φ' =>
simp only [crPart_position, anPart_position]
refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
rw [crPart_position, anPart_position]
exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
| .inAsymp φ, .outAsymp φ' =>
simp only [crPart_negAsymp, anPart_posAsymp]
refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
rw [crPart_negAsymp, anPart_posAsymp]
exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
| .inAsymp φ, .position φ' =>
simp only [crPart_negAsymp, anPart_position]
refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
rw [crPart_negAsymp, anPart_position]
exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
| .position φ, .outAsymp φ' =>
simp only [crPart_position, anPart_posAsymp]
refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
rw [crPart_position, anPart_posAsymp]
exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
normalOrder (a * superCommute
(anPart (StateAlgebra.ofState φ)) (crPart (StateAlgebra.ofState φ')) * b) = 0 := by
match φ, φ' with
| .inAsymp φ', _ =>
simp
| _, .outAsymp φ' =>
simp
| .inAsymp φ', _ => simp
| _, .outAsymp φ' => simp
| .position φ, .position φ' =>
simp only [anPart_position, crPart_position]
refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
rw [anPart_position, crPart_position]
exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
| .outAsymp φ', .inAsymp φ =>
simp only [anPart_posAsymp, crPart_negAsymp]
refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
| .position φ', .inAsymp φ =>
simp only [anPart_position, crPart_negAsymp]
refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
| .outAsymp φ, .position φ' =>
simp only [anPart_posAsymp, crPart_position]
refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
/-!
@ -359,8 +317,7 @@ lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
(crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') +
anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
rw [mul_add, add_mul, add_mul]
rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart, mul_add, add_mul, add_mul]
simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart,
instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart]
abel
@ -381,17 +338,14 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
normalOrderSign (φs ++ φc' :: φc :: φs') •
(ofCrAnList (createFilter φs) * superCommute (ofCrAnState φc) (ofCrAnState φc') *
ofCrAnList (createFilter φs') * ofCrAnList (annihilateFilter (φs ++ φs'))) := by
rw [superCommute_ofCrAnState_ofCrAnState]
rw [mul_sub, sub_mul, map_sub]
rw [superCommute_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub]
conv_lhs =>
lhs
rhs
lhs; rhs
rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append,
← ofCrAnList_append]
conv_lhs =>
lhs
rw [normalOrder_ofCrAnList]
rw [normalOrderList_eq_createFilter_append_annihilateFilter]
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
rw [createFilter_append, createFilter_append, createFilter_append,
createFilter_singleton_create _ hφc, createFilter_singleton_create _ hφc']
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -401,10 +355,8 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
instCommGroup.eq_1, Algebra.smul_mul_assoc, Algebra.mul_smul_comm, map_smul]
rw [← annihilateFilter_append]
conv_lhs =>
rhs
rhs
rw [smul_mul_assoc]
rw [Algebra.mul_smul_comm, smul_mul_assoc]
rhs; rhs
rw [smul_mul_assoc, Algebra.mul_smul_comm, smul_mul_assoc]
rhs
rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append,
← ofCrAnList_append]
@ -412,8 +364,7 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
rhs
rw [map_smul]
rhs
rw [normalOrder_ofCrAnList]
rw [normalOrderList_eq_createFilter_append_annihilateFilter]
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
rw [createFilter_append, createFilter_append, createFilter_append,
createFilter_singleton_create _ hφc, createFilter_singleton_create _ hφc']
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -423,25 +374,20 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
List.append_nil, Algebra.smul_mul_assoc]
rw [← annihilateFilter_append]
conv_lhs =>
lhs
lhs
lhs; lhs
simp
conv_lhs =>
rhs
rhs
lhs
rhs; rhs; lhs
simp
rw [normalOrderSign_swap_create_create φc φc' hφc hφc']
rw [smul_smul, mul_comm, ← smul_smul]
rw [← smul_sub, ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
conv_lhs =>
rhs
rhs
rhs; rhs
rw [ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
rw [← smul_mul_assoc, ← smul_mul_assoc, ← Algebra.mul_smul_comm]
rw [← sub_mul, ← sub_mul, ← mul_sub]
congr
rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton]
rw [← sub_mul, ← sub_mul, ← mul_sub, ofCrAnList_append, ofCrAnList_singleton,
ofCrAnList_singleton]
rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc]
lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
@ -455,17 +401,14 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
(ofCrAnList (createFilter (φs ++ φs'))
* ofCrAnList (annihilateFilter φs) * superCommute (ofCrAnState φa) (ofCrAnState φa')
* ofCrAnList (annihilateFilter φs')) := by
rw [superCommute_ofCrAnState_ofCrAnState]
rw [mul_sub, sub_mul, map_sub]
rw [superCommute_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub]
conv_lhs =>
lhs
rhs
lhs; rhs
rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_append, ← ofCrAnList_append,
← ofCrAnList_append]
conv_lhs =>
lhs
rw [normalOrder_ofCrAnList]
rw [normalOrderList_eq_createFilter_append_annihilateFilter]
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
rw [createFilter_append, createFilter_append, createFilter_append,
createFilter_singleton_annihilate _ hφa, createFilter_singleton_annihilate _ hφa']
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -475,8 +418,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
instCommGroup.eq_1, Algebra.smul_mul_assoc, Algebra.mul_smul_comm, map_smul]
rw [← createFilter_append]
conv_lhs =>
rhs
rhs
rhs; rhs
rw [smul_mul_assoc]
rw [Algebra.mul_smul_comm, smul_mul_assoc]
rhs
@ -486,8 +428,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
rhs
rw [map_smul]
rhs
rw [normalOrder_ofCrAnList]
rw [normalOrderList_eq_createFilter_append_annihilateFilter]
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
rw [createFilter_append, createFilter_append, createFilter_append,
createFilter_singleton_annihilate _ hφa, createFilter_singleton_annihilate _ hφa']
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
@ -497,20 +438,16 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
List.append_nil, Algebra.smul_mul_assoc]
rw [← createFilter_append]
conv_lhs =>
lhs
lhs
lhs; lhs
simp
conv_lhs =>
rhs
rhs
lhs
rhs; rhs; lhs
simp
rw [normalOrderSign_swap_annihilate_annihilate φa φa' hφa hφa']
rw [smul_smul, mul_comm, ← smul_smul]
rw [← smul_sub, ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
conv_lhs =>
rhs
rhs
rhs; rhs
rw [ofCrAnList_append, ofCrAnList_append, ofCrAnList_append]
rw [← Algebra.mul_smul_comm, ← smul_mul_assoc, ← Algebra.mul_smul_comm]
rw [← mul_sub, ← sub_mul, ← mul_sub]
@ -519,7 +456,6 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
apply congrArg
rw [mul_assoc]
apply congrArg
congr
rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton]
rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc]
@ -558,16 +494,14 @@ lemma ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute (φs : List 𝓕.Cr
ofCrAnList φs * normalOrder (ofStateList φs') =
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs') * ofCrAnList φs
+ ⟨ofCrAnList φs, normalOrder (ofStateList φs')⟩ₛca := by
rw [ofCrAnList_superCommute_normalOrder_ofStateList]
simp
simp [ofCrAnList_superCommute_normalOrder_ofStateList]
lemma ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.CrAnStates)
(φs' : List 𝓕.States) :
ofCrAnState φ * normalOrder (ofStateList φs') =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs') * ofCrAnState φ
+ ⟨ofCrAnState φ, normalOrder (ofStateList φs')⟩ₛca := by
rw [← ofCrAnList_singleton, ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute]
simp [ofCrAnList_singleton]
simp [← ofCrAnList_singleton, ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute]
lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
(φs' : List 𝓕.States) :
@ -576,16 +510,9 @@ lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
+ ⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φs')⟩ₛca := by
rw [normalOrder_mul_anPart]
match φ with
| .inAsymp φ =>
simp
| .position φ =>
simp only [anPart_position, instCommGroup.eq_1]
rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute]
simp [crAnStatistics]
| .outAsymp φ =>
simp only [anPart_posAsymp, instCommGroup.eq_1]
rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute]
simp [crAnStatistics]
| .inAsymp φ => simp
| .position φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute, crAnStatistics]
| .outAsymp φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute, crAnStatistics]
end

24
HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
View file

@ -69,19 +69,14 @@ lemma koszulSignInsert_create (φ : 𝓕.CrAnStates)
lemma normalOrderSign_cons_create (φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
normalOrderSign (φ :: φs) = normalOrderSign φs := by
dsimp only [normalOrderSign, Wick.koszulSign]
rw [koszulSignInsert_create φ hφ φs]
simp
simp [normalOrderSign, Wick.koszulSign, koszulSignInsert_create φ hφ φs]
@[simp]
lemma normalOrderSign_singleton (φ : 𝓕.CrAnStates) :
normalOrderSign [φ] = 1 := by
lemma normalOrderSign_singleton (φ : 𝓕.CrAnStates) : normalOrderSign [φ] = 1 := by
simp [normalOrderSign]
@[simp]
lemma normalOrderSign_nil :
normalOrderSign (𝓕 := 𝓕) [] = 1 := by
simp [normalOrderSign, Wick.koszulSign]
lemma normalOrderSign_nil : normalOrderSign (𝓕 := 𝓕) [] = 1 := rfl
lemma koszulSignInsert_append_annihilate (φ' φ : 𝓕.CrAnStates)
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) :
@ -139,10 +134,8 @@ lemma normalOrderSign_swap_create_annihlate_fst (φc φa : 𝓕.CrAnStates)
lemma koszulSignInsert_swap (φ φc φa : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa :: φc :: φs')
= Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φa :: φs') := by
apply Wick.koszulSignInsert_eq_perm
refine List.Perm.append_left φs ?h.a
exact List.Perm.swap φc φa φs'
= Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φa :: φs') :=
Wick.koszulSignInsert_eq_perm _ _ _ _ _ (List.Perm.append_left φs (List.Perm.swap φc φa φs'))
lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate) :
@ -157,12 +150,9 @@ lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
rw [← mul_assoc, mul_comm _ (FieldStatistic.exchangeSign _ _), mul_assoc]
simp only [FieldStatistic.instCommGroup.eq_1, mul_eq_mul_left_iff]
apply Or.inl
conv_rhs =>
rw [normalOrderSign]
dsimp [Wick.koszulSign]
rw [← normalOrderSign]
conv_rhs => rw [normalOrderSign, Wick.koszulSign, ← normalOrderSign]
simp only [mul_eq_mul_right_iff]
apply Or.inl
left
rw [koszulSignInsert_swap]
lemma normalOrderSign_swap_create_create_fst (φc φc' : 𝓕.CrAnStates)

2
HepLean/PerturbationTheory/WickContraction/Insert.lean
View file

@ -200,7 +200,7 @@ lemma mem_uncontracted_insert_none_iff (c : WickContraction n) (i : Fin n.succ)
· simp only [Nat.succ_eq_add_one, ← Fin.exists_succAbove_eq_iff] at hi
obtain ⟨z, hk⟩ := hi
subst hk
have hn : ¬ i.succAbove z = i := by exact Fin.succAbove_ne i z
have hn : ¬ i.succAbove z = i := Fin.succAbove_ne i z
simp only [Nat.succ_eq_add_one, insert_succAbove_mem_uncontracted_iff, hn, false_or]
apply Iff.intro
· intro h

4
HepLean/PerturbationTheory/WickContraction/InsertList.lean
View file

@ -77,7 +77,7 @@ lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
· simp [congrLift]
· rw [Fin.lt_def] at h ⊢
simp_all only [Nat.succ_eq_add_one, Fin.val_fin_lt, not_lt, finCongr_apply, Fin.coe_cast]
have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j
omega
/-!
@ -188,7 +188,7 @@ lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
· simp [congrLift]
· rw [Fin.lt_def] at h ⊢
simp_all only [Nat.succ_eq_add_one, Fin.val_fin_lt, not_lt, finCongr_apply, Fin.coe_cast]
have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j
omega
lemma insertList_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)

20
HepLean/PerturbationTheory/WickContraction/Sign.lean
View file

@ -240,7 +240,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States)
simp_all only [and_true, Finset.mem_insert]
rw [succAbove_mem_insertListLiftFinset]
simp only [Fin.ext_iff, Fin.coe_cast]
have h1 : ¬ (i.succAbove ↑j) = i := by exact Fin.succAbove_ne i ↑j
have h1 : ¬ (i.succAbove ↑j) = i := Fin.succAbove_ne i ↑j
simp only [Fin.val_eq_val, h1, signFinset, Finset.mem_filter, Finset.mem_univ, true_and,
false_or]
rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff]
@ -284,7 +284,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States)
intro h
simp only [Fin.ext_iff, Fin.coe_cast] at h
simp only [Fin.val_eq_val] at h
have hn : ¬ i.succAbove k = i := by exact Fin.succAbove_ne i k
have hn : ¬ i.succAbove k = i := Fin.succAbove_ne i k
exact False.elim (hn h)
· split
simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_erase, ne_eq,
@ -807,7 +807,7 @@ lemma stat_signFinset_insert_some_self_fst
obtain ⟨y, hy1, hy2⟩ := h
simp only [Fin.ext_iff, Fin.coe_cast] at hy2
simp only [Fin.val_eq_val] at hy2
rw [Function.Injective.eq_iff (by exact Fin.succAbove_right_injective)] at hy2
rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hy2
subst hy2
simp only [hy1, true_and]
apply And.intro
@ -885,7 +885,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S
obtain ⟨y, hy1, hy2⟩ := h
simp only [Fin.ext_iff, Fin.coe_cast] at hy2
simp only [Fin.val_eq_val] at hy2
rw [Function.Injective.eq_iff (by exact Fin.succAbove_right_injective)] at hy2
rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hy2
subst hy2
simp only [hy1, true_and]
apply And.intro
@ -965,13 +965,13 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List
· exact h1'
· /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
intro j hj
have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
have hn : ¬ c.getDual? j = none := Option.isSome_iff_ne_none.mp hj
simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
hn, hj, forall_true_left, false_or, true_and, and_false, false_and, Finset.mem_inter,
not_false_eq_true, and_true, not_and, not_lt, getDual?_getDual?_get_get, reduceCtorEq,
Option.isSome_some, Option.get_some, forall_const, and_imp]
intro h1 h2
have hijsucc' : i.succAbove ((c.getDual? j).get hj) ≠ i := by exact Fin.succAbove_ne i _
have hijsucc' : i.succAbove ((c.getDual? j).get hj) ≠ i := Fin.succAbove_ne i _
have hkneqj : ↑k ≠ j := by
by_contra hkj
have hk := k.prop
@ -1025,7 +1025,7 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
signInsertSome φ φs c i k *
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, c.uncontracted.filter (fun x => x < ↑k)⟩)
= 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by
have hik : i.succAbove ↑k ≠ i := by exact Fin.succAbove_ne i ↑k
have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),
signInsertSomeCoef_eq_finset (hφj := hg.2), if_pos (by omega), ← map_mul, ← map_mul]
congr 1
@ -1036,7 +1036,7 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1
· /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
intro j hj
have hijsucc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
have hijsucc : i.succAbove j ≠ i := Fin.succAbove_ne i j
simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and,
and_false, or_false, Finset.mem_inter, not_false_eq_true, and_self, not_and, not_lt,
@ -1055,8 +1055,8 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
omega
· /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
intro j hj
have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
have hijSuc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
have hn : ¬ c.getDual? j = none := Option.isSome_iff_ne_none.mp hj
have hijSuc : i.succAbove j ≠ i := Fin.succAbove_ne i j
have hkneqj : ↑k ≠ j := by
by_contra hkj
have hk := k.prop

2
HepLean/PerturbationTheory/WicksTheorem.lean
View file

@ -198,7 +198,7 @@ lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : Li
congr 1
exact signInsertSome_mul_filter_contracted_of_lt φ φs c i k hk hg
· omega
· have hik : i.succAbove ↑k ≠ i := by exact Fin.succAbove_ne i ↑k
· have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_lt]
swap
· exact hlt _