TraceExpansion.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix expansions for the two trace moments in the IMM argument. These identities contain no analytic or asymptotic assumptions.

def OAI.Problem335.pathShiftMatrix line 17

Source documentation

A matrix whose column is a weighted sum of path shifts.

def pathShiftMatrix [AddCommMonoid R] (shift : I → P → J) (weight : I → P → R) :
    Matrix J I R := by
…

theorem OAI.Problem335.trace_transpose_mul_self line 23

Source documentation

Expanding a real Gram matrix gives the sum of squared entries.

theorem trace_transpose_mul_self {I : Type u_1} {J : Type u_2}
    [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : Matrix J I ℝ) :
    Matrix.trace (A.transpose * A) = ∑ i, ∑ j, (A j i) ^ 2 := by
…

theorem OAI.Problem335.trace_gram_sq line 29

Source documentation

The second moment is the sum of squares of all Gram entries.

theorem trace_gram_sq {I : Type u_1} {J : Type u_2}
    [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : Matrix J I ℝ) :
    Matrix.trace ((A.transpose * A) ^ 2) =
      ∑ i, ∑ k, (∑ j, A j i * A j k) ^ 2 := by
…

theorem OAI.Problem335.pathShiftMatrix_gram_apply line 45

Source documentation

The Gram entry is a weighted count of pairs of paths with equal shifts.

theorem pathShiftMatrix_gram_apply
    {I : Type u_1} {J : Type u_2} {P : Type u_3} {R : Type u_4}
    [Fintype I] [Fintype J] [Fintype P] [DecidableEq I] [DecidableEq J] [CommSemiring R]
    (shift : I → P → J) (weight : I → P → R) (i k : I) :
    ((pathShiftMatrix shift weight).transpose * pathShiftMatrix shift weight) i k =
      ∑ p, ∑ q, if shift i p = shift k q then weight i p * weight k q else 0 := by
…

Mentions: OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.pathShiftMatrix_first_trace line 67

Source documentation

It is enough that distinct paths reaching the same row have zero weight product. This permits invalid path shifts to be given arbitrary target indices when their weight is zero.

theorem pathShiftMatrix_first_trace [CommSemiring R]
    (shift : I → P → J) (weight : I → P → R)
    (hdisjoint : ∀ i p q, p ≠ q → shift i p = shift i q →
      weight i p * weight i q = 0) :
    Matrix.trace ((pathShiftMatrix shift weight).transpose * pathShiftMatrix shift weight) =
      ∑ i, ∑ p, weight i p ^ 2 := by
…

Mentions: OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.pathShiftMatrix_first_trace_of_injective line 88

Source documentation

Columnwise injectivity of the path shifts implies the first trace identity.

theorem pathShiftMatrix_first_trace_of_injective [CommSemiring R]
    (shift : I → P → J) (weight : I → P → R)
    (hinj : ∀ i, Function.Injective (shift i)) :
    Matrix.trace ((pathShiftMatrix shift weight).transpose * pathShiftMatrix shift weight) =
      ∑ i, ∑ p, weight i p ^ 2 := by
…

Mentions: OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.pathShiftMatrix_second_trace line 98

Source documentation

The second trace is the squared-overlap sum of the weighted path shifts.

theorem pathShiftMatrix_second_trace
    (shift : I → P → J) (weight : I → P → ℝ) :
    Matrix.trace (((pathShiftMatrix shift weight).transpose *
      pathShiftMatrix shift weight) ^ 2) =
      ∑ i, ∑ k, (∑ p, ∑ q,
        if shift i p = shift k q then weight i p * weight k q else 0) ^ 2 := by
…

Mentions: OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.trace_conjTranspose_mul_self_complex line 113

Source documentation

Frobenius expansion over the complex numbers, with the genuine adjoint.

theorem trace_conjTranspose_mul_self_complex {I : Type u_1} {J : Type u_2}
    [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : Matrix J I ℂ) :
    Matrix.trace (A.conjTranspose * A) =
      ∑ i, ∑ j, (Complex.normSq (A j i) : ℂ) := by
…

theorem OAI.Problem335.pathShiftMatrix_second_trace_four_paths line 122

Source documentation

The complete four-path expansion of the second trace moment.

theorem pathShiftMatrix_second_trace_four_paths
    (shift : I → P → J) (weight : I → P → ℝ) :
    Matrix.trace (((pathShiftMatrix shift weight).transpose *
      pathShiftMatrix shift weight) ^ 2) =
      ∑ i, ∑ k, ∑ p, ∑ q, ∑ r, ∑ s,
        if shift i p = shift k q ∧ shift i r = shift k s then
          weight i p * weight k q * weight i r * weight k s else 0 := by
…

Mentions: OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.pathShiftMatrix_first_trace_sqrt line 150

Source documentation

Square-root path weights yield the sum of the underlying occupation masses. Zero-mass invalid paths need not have distinct shifts.

theorem pathShiftMatrix_first_trace_sqrt
    (shift : I → P → J) (mass : I → P → ℝ)
    (hnonneg : ∀ i p, 0 ≤ mass i p)
    (hdisjoint : ∀ i p q, p ≠ q → shift i p = shift i q →
      mass i p = 0 ∨ mass i q = 0) :
    Matrix.trace ((pathShiftMatrix shift (fun i p => Real.sqrt (mass i p))).transpose *
      pathShiftMatrix shift (fun i p => Real.sqrt (mass i p))) =
      ∑ i, ∑ p, mass i p := by
…

Mentions: OAI.Problem335.pathShiftMatrix