JacobiMatrixLoss.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The scalar determinant deficit applied to the actual symmetric matrix.

theorem OAI.PositiveEinsteinFour.Jacobi.trace_unitary_conj line 16
theorem OAI.PositiveEinsteinFour.Jacobi.det_unitary_conj line 21
theorem OAI.PositiveEinsteinFour.Jacobi.posSemidef_unitary_conj line 30
theorem OAI.PositiveEinsteinFour.Jacobi.frobenius_sq_eq_trace_square line 37
theorem OAI.PositiveEinsteinFour.Jacobi.frobenius_sq_eq_sum_eigenvalues line 53
Source documentation
The concrete Frobenius norm is the sum of the three eigenvalue squares.
```
theorem frobenius_sq_eq_sum_eigenvalues {A : NormalMatrix} (hA : A.IsHermitian) :
    ‖A‖ ^ 2 = ∑ i, (hA.eigenvalues i) ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix
theorem OAI.PositiveEinsteinFour.Jacobi.matrix_preconjugate_loss line 68
Source documentation
Matrix form of the preconjugate determinant loss. The two semidefinite hypotheses are exactly the lower curvature bound and the first-mode compression.
```
theorem matrix_preconjugate_loss {A : NormalMatrix} {β : ℝ} (hA : A.IsHermitian)
    (hβ : 0 ≤ β) (htrace : A.trace = 0)
    (hlower : (A + 1).PosSemidef) (hupper : (1 - β • A).PosSemidef) :
    (1 - β • A).det ≤ 1 - lossFactor β / 6 * ‖A‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.lossFactor
theorem OAI.PositiveEinsteinFour.Jacobi.matrix_postconjugate_loss line 110
Source documentation
The positive curvature lower bound and trace normalization also control the postconjugate branch, where radial density is set to zero.
```
theorem matrix_postconjugate_loss {A : NormalMatrix} (hA : A.IsHermitian)
    (β : ℝ) (htrace : A.trace = 0) (hlower : (A + 1).PosSemidef) :
    lossFactor β / 6 * ‖A‖ ^ 2 ≤ 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.lossFactor