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

Sign Insert Some mul filter contracted of not lt

WickContraction.signInsertSome_mul_filter_contracted_of_not_lt

Plain-language statement

The following two signs are equal for i < i.succAbove k. The sign signInsertSome φ φs φsΛ i k which is constructed as follows: 1a. For each contracted pair {a1, a2} in φsΛ with a1 < a2 the sign 𝓢(φ, φₐ₂) if a₁ < i ≤ a₂ and a₁ < k. 1b. For each contracted pair {a1, a2} in φsΛ with a1 < a2 the sign 𝓢(φⱼ, φₐ₂) if a₁ < k < a₂ and `...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Static Contract insert some

WickContraction.staticContract_insert_some

Plain-language statement

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)).staticContract is equal to the product of - [anPart φ, φs[k]]ₛ if i ≤ k or [anPart φs[k], φ]ₛ if k < i - φsΛ.staticContract. The proof of this result ultimately...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Static Wick Term insert zero some

WickContraction.staticWickTerm_insert_zero_some

Plain-language statement

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a k in φsΛ.uncontracted, (φsΛ ↩Λ φ 0 (some k)).wickTerm is equal to the product of - the sign 𝓢(φ, φ₀…φᵢ₋₁) - the sign φsΛ.sign - φsΛ.staticContract - s • [anPart φ, ofFieldOp φs[k]]ₛ where s is the sign associated with moving `...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Contract insert some of lt

WickContraction.timeContract_insert_some_of_lt

Plain-language statement

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 such that i ≤ k, with the condition that φ has greater or equal time to φs[k], then (φsΛ ↩Λ φ i (some k)).timeContract is equal to the product of - [anPart φ, φs[k]]ₛ - φsΛ.timeContract -...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Contract insert some of not lt

WickContraction.timeContract_insert_some_of_not_lt

Plain-language statement

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 such that k < i, with the condition that φs[k] does not have time greater or equal to φ, then (φsΛ ↩Λ φ i (some k)).timeContract is equal to the product of - [anPart φ, φs[k]]ₛ - `φsΛ.timeCo...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Contract insert And Contract some

WickContraction.timeContract_insertAndContract_some

Plain-language statement

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)).timeContract is equal to the product of - timeContract φ φs[k] if i ≤ k or timeContract φs[k] φ if k < i - φsΛ.timeContract. The proof of this result ultimately...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record