TraceComplexification.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The real nonnegative path matrix can be read over the complex numbers without changing either of its two trace moments.

theorem OAI.Problem335.complexify_gram line 17

Source documentation

Real entrywise complexification sends the real Gram matrix to the complex Gram matrix.

theorem complexify_gram {I : Type u_1} {J : Type u_2}
    [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : Matrix J I ℝ) :
    (A.map Complex.ofReal).conjTranspose * A.map Complex.ofReal =
      (A.transpose * A).map Complex.ofReal := by
…

theorem OAI.Problem335.trace_complexify_re line 26

Source documentation

Entrywise complexification preserves the real part of the trace.

theorem trace_complexify_re {I : Type u_1} [Fintype I] [DecidableEq I]
    (A : Matrix I I ℝ) :
    (A.map Complex.ofReal).trace.re = A.trace := by
…

theorem OAI.Problem335.complexify_first_trace line 32

Source documentation

First moment agrees over the real and complex coefficient fields.

theorem complexify_first_trace (A : Matrix J I ℝ) :
    ((A.map Complex.ofReal).conjTranspose * A.map Complex.ofReal).trace.re =
      (A.transpose * A).trace := by
…

theorem OAI.Problem335.complexify_second_trace line 38

Source documentation

Second moment agrees over the real and complex coefficient fields.

theorem complexify_second_trace (A : Matrix J I ℝ) :
    (((A.map Complex.ofReal).conjTranspose * A.map Complex.ofReal) ^ 2).trace.re =
      ((A.transpose * A) ^ 2).trace := by
…

theorem OAI.Problem335.pathShiftMatrix_complexify line 48

Source documentation

Complexifying a path matrix complexifies just its weights.

theorem pathShiftMatrix_complexify {I : Type u_1} {J : Type u_2} {P : Type u_3}
    [Fintype I] [Fintype J] [Fintype P] [DecidableEq I] [DecidableEq J]
    (shift : I → P → J) (weight : I → P → ℝ) :
    (pathShiftMatrix shift weight).map Complex.ofReal =
      pathShiftMatrix shift (fun i p => (weight i p : ℂ)) := by
…

Mentions: OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.complex_path_first_trace_sqrt line 60

Source documentation

First complex trace of the square-root mass path matrix.

theorem complex_path_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) :
    let A := pathShiftMatrix shift (fun i p => (Real.sqrt (mass i p) : ℂ))
…

Mentions: OAI.Problem335.pathShiftMatrix

theorem OAI.Problem335.complex_path_second_trace_four_paths line 72
Source documentation
Four-path expression of the second complex trace for real path weights.
```
theorem complex_path_second_trace_four_paths
    (shift : I → P → J) (weight : I → P → ℝ) :
    let A := pathShiftMatrix shift (fun i p => (weight i p : ℂ))
…
```
Mentions: OAI.Problem335.pathShiftMatrix