Research proof index

In the state algebra time, ordering obeys T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ) where φᵢ is the state which has maximum time and s is the exchange sign of φᵢ and φ₀φ₁…φᵢ₋₁. Here s is written using finite sets.

The commutator of the annihilation part of a field operator with a normal ordered list of field operators can be decomposed into the sum of the commutators of the annihilation part with each element of the list of field operators, i.e. [anPart φ, 𝓝(φ₀…φₙ)]ₛ= ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [anPart φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ).

The projection of 𝓕.WickAlgebra to statSubmodule (𝓕 := 𝓕) fermionic. -/ def fermionicProj : 𝓕.WickAlgebra →ₗ[ℂ] statSubmodule (𝓕 := 𝓕) fermionic where toFun := Quotient.lift fermionicProjFree fermionicProjFree_eq_of_equiv map_add' x y := by obtain ⟨x, hx⟩ := ι_surjective x obtain ⟨y, hy⟩ := ι_surjective y subst hx hy rw [← map_add, ι_apply, ι_ap...

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a i ≤ φs.length, then the following relation holds: 𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ) where s is the exchange sign for φ and the uncontracted fields in φ₀…φᵢ₋₁. The proof of this result ultimately is a consequence of `norma...

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted, then 𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ) is equal to the normal ordering of [φsΛ]ᵘᶜ with the 𝓕.FieldOp corresponding to k removed. The proof of this result ultimately is a consequence of definitions.

For a field specification 𝓕, an element φ of 𝓕.CrAnFieldOp, a list φs of 𝓕.CrAnFieldOp, the following relation holds [φ, 𝓝(φ₀…φₙ)]ₛ = ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ). The proof of this result ultimately goes as follows - The definition of normalOrder is used to rewrite 𝓝(φ₀…φₙ) as a scalar multiple of a `ofCrAnList...