SpectralEntropy.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GAD.trace_unitary_conj line 22

Source documentation

Trace invariance under a unitary change of basis.

theorem trace_unitary_conj (U : Matrix.unitaryGroup ι ℂ) (A : Matrix ι ι ℂ) :
    (Unitary.conjStarAlgAut ℂ _ U A).trace = A.trace := by
…

theorem OAI.GAD.trace_cfc_eq line 28

Source documentation

Spectral trace for any function on the finite real spectrum.

theorem trace_cfc_eq {A : Matrix ι ι ℂ} (hA : A.IsHermitian) (f : ℝ → ℝ) :
    (cfc f A).trace = ∑ i, (f (hA.eigenvalues i) : ℂ) := by
…

theorem OAI.GAD.entropy_eq_sum line 33
theorem OAI.GAD.entropy_nonneg line 37
theorem OAI.GAD.unitary_row_sq_sum line 49
Source documentation
The square-moduli in each row of a unitary matrix sum to one.
```
theorem unitary_row_sq_sum (U : Matrix.unitaryGroup ι ℂ) (i : ι) :
    ∑ j, Complex.normSq (U i j) = 1 := by
…
```
theorem OAI.GAD.unitary_col_sq_sum line 56
Source documentation
The square-moduli in each column of a unitary matrix sum to one.
```
theorem unitary_col_sq_sum (U : Matrix.unitaryGroup ι ℂ) (j : ι) :
    ∑ i, Complex.normSq (U i j) = 1 := by
…
```

theorem OAI.GAD.diag_eq_spectral_mix line 63

Source documentation

The ordinary diagonal is a doubly stochastic mixing of the spectral diagonal.

theorem diag_eq_spectral_mix {A : Matrix ι ι ℂ} (hA : A.IsHermitian) (i : ι) :
    (A i i).re = ∑ j, Complex.normSq (hA.eigenvectorUnitary i j) * hA.eigenvalues j := by
…

theorem OAI.GAD.entropy_le_diagonal line 75
Source documentation
Pinching in any fixed orthonormal coordinate basis increases entropy.
```
theorem entropy_le_diagonal {A : Matrix ι ι ℂ} (hA : A.PosSemidef) :
    entropy A ≤ ∑ i, Real.negMulLog (A i i).re := by
…
```
Mentions: OAI.GAD.entropy

theorem OAI.GAD.entropy_unitary_conj line 95

Source documentation

Entropy is invariant under every unitary basis change.

theorem entropy_unitary_conj (U : Matrix.unitaryGroup ι ℂ)
    {A : Matrix ι ι ℂ} (hA : A.IsHermitian) :
    entropy (Unitary.conjStarAlgAut ℂ _ U A) = entropy A := by
…

Mentions: OAI.GAD.entropy

theorem OAI.GAD.concaveOn_entropy line 114
Source documentation
The full matrix entropy, not just normalized-state entropy, is concave on positive semidefinite matrices.
```
theorem concaveOn_entropy :
    ConcaveOn ℝ {A : Matrix ι ι ℂ | A.PosSemidef} entropy := by
…
```
Mentions: OAI.GAD.entropy