Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 591 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

591 results

Clear filters
Project-declaredLean 4.32.0

Of Field Op mul normal Order of Field Op List eq super Commute

FieldSpecification.WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute

Plain-language statement

Within a proto-operator algebra we have that φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ(φφ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛF.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Of Field Op List normal Order insert

FieldSpecification.WickAlgebra.ofFieldOpList_normalOrder_insert

Plain-language statement

Within a proto-operator algebra, N(φφ₀φ₁…φₙ) = s • N(φ₀…φₖ₋₁φφₖ…φₙ), where s is the exchange sign for φ and φ₀…φₖ₋₁.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Contract mem center

FieldSpecification.WickAlgebra.timeContract_mem_center

Plain-language statement

For a field specification 𝓕, and φ and ψ elements of 𝓕.FieldOp, then timeContract φ ψ is in the center of 𝓕.WickAlgebra.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Contract of time Order Rel

FieldSpecification.WickAlgebra.timeContract_of_timeOrderRel

Plain-language statement

For a field specification 𝓕, and φ and ψ elements of 𝓕.FieldOp, if φ and ψ are time-ordered then timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Order have Eq Time split

FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split

Plain-language statement

For a list φs of 𝓕.FieldOp, then 𝓣(φs) is equal to the sum of - ∑ φsΛ, φsΛ.wickTerm where the sum is over all Wick contraction φsΛ which have no contractions of equal time. - ∑ φsΛ, φsΛ.sign • φsΛ.timeContract * (∑ φssucΛ, φssucΛ.wickTerm), where the first sum is over all Wick contraction φsΛ which only have equal time contractions and the...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Order of Field Op List eq Time Only

FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly

Plain-language statement

For a list φs of 𝓕.FieldOp, then 𝓣(φs) = ∑ φsΛ, φsΛ.sign • φsΛ.timeContract * 𝓣(𝓝([φsΛ]ᵘᶜ)) where the sum is over all Wick contraction φsΛ which only have equal time contractions. This result follows from - static_wick_theorem to rewrite 𝓣(φs) on the left hand side as a sum of 𝓣(φsΛ.staticWickTerm). - `EqTimeOnly.timeOrder_staticContra...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record