LogDetConvexity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GAD.hasDerivAt_trace line 19

Source documentation

Trace commutes with differentiation of finite-dimensional matrix curves.

theorem hasDerivAt_trace {A : ℝ → Matrix ι ι ℂ} {H : Matrix ι ι ℂ} {t : ℝ}
    (hA : HasDerivAt A H t) :
    HasDerivAt (fun s ↦ (A s).trace) H.trace t := by
…

theorem OAI.GAD.hasDerivAt_trace_inv_mul line 28

Source documentation

The first derivative term in Jacobi's formula has the expected noncommutative derivative.

theorem hasDerivAt_trace_inv_mul {A : ℝ → Matrix ι ι ℂ} {H : Matrix ι ι ℂ} {t : ℝ}
    (hA : HasDerivAt A H t) (hdet : (A t).det ≠ 0) :
    HasDerivAt (fun s ↦ (Matrix.trace ((A s)⁻¹ * H)).re)
      (-(Matrix.trace (((A t)⁻¹ * H) * ((A t)⁻¹ * H))).re) t := by
…

def OAI.GAD.skewLogDet line 39
Source documentation
The skew-shift log-determinant deficit, including non-real determinants.
```
def skewLogDet (Z D : Matrix ι ι ℂ) : ℝ :=
…
```

theorem OAI.GAD.posDef_segment line 44

Source documentation

Positivity is preserved throughout a segment, including both endpoints.

theorem posDef_segment {D E : Matrix ι ι ℂ} (hD : D.PosDef) (hE : E.PosDef)
    {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    (a • D + b • E).PosDef := by
…

theorem OAI.GAD.convexOn_skewLogDet line 53
Source documentation
Joint convexity mechanism: a fixed skew-Hermitian perturbation has convex logdet deficit.
```
theorem convexOn_skewLogDet (Z : Matrix ι ι ℂ) (hZ : Z.conjTranspose = -Z) :
    ConvexOn ℝ {D : Matrix ι ι ℂ | D.PosDef} (skewLogDet Z) := by
…
```
Mentions: OAI.GAD.skewLogDet

theorem OAI.GAD.posDef_fromBlocks_zero line 113

Source documentation

A direct sum of strictly positive matrices is strictly positive.

theorem posDef_fromBlocks_zero {D : Matrix ι ι ℂ} {E : Matrix κ κ ℂ}
    (hD : D.PosDef) (hE : E.PosDef) :
    (Matrix.fromBlocks D 0 0 E).PosDef := by
…

def OAI.GAD.blockLogDet line 139
theorem OAI.GAD.skewLogDet_fromBlocks line 142

theorem OAI.GAD.convexOn_blockLogDet line 162

Source documentation

Main log-determinant lemma, in all finite rectangular block dimensions.

theorem convexOn_blockLogDet (Z : Matrix ι κ ℂ) :
    ConvexOn ℝ {p : Matrix ι ι ℂ × Matrix κ κ ℂ | p.1.PosDef ∧ p.2.PosDef}
      (fun p ↦ blockLogDet Z p.1 p.2) := by
…

Mentions: OAI.GAD.blockLogDet