MatrixDifferentiation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GAD.detMultilinear line 16
Source documentation
The determinant as a continuous multilinear map in its rows.
```
def detMultilinear : ContinuousMultilinearMap ℂ (fun _ : ι ↦ ι → ℂ) ℂ :=
…
```

theorem OAI.GAD.det_linearDeriv line 23

Source documentation

Jacobi's differential, without an invertibility assumption.

theorem det_linearDeriv (A H : Matrix ι ι ℂ) :
    detMultilinear.linearDeriv A H = Matrix.trace (H * A.adjugate) := by
…

theorem OAI.GAD.hasDerivAt_det line 39

Source documentation

Jacobi's formula along any differentiable complex-matrix curve.

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

theorem OAI.GAD.hasDerivAt_matrix_mul line 48

Source documentation

Product differentiation with the entrywise matrix topology.

theorem hasDerivAt_matrix_mul {A B : ℝ → Matrix ι ι ℂ}
    {H K : Matrix ι ι ℂ} {t : ℝ}
    (hA : HasDerivAt A H t) (hB : HasDerivAt B K t) :
    HasDerivAt (fun s ↦ A s * B s) (H * B t + A t * K) t := by
…

theorem OAI.GAD.hasDerivAt_updateRow line 65

Source documentation

The row replacement operation is affine.

theorem hasDerivAt_updateRow {A : ℝ → Matrix ι ι ℂ} {H : Matrix ι ι ℂ} {t : ℝ}
    (hA : HasDerivAt A H t) (i : ι) (x : ι → ℂ) :
    HasDerivAt (fun s ↦ (A s).updateRow i x) (H.updateRow i 0) t := by
…

theorem OAI.GAD.differentiableAt_adjugate line 76

Source documentation

Polynomial differentiability of the adjugate, with no nonsingularity restriction.

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

theorem OAI.GAD.hasDerivAt_matrix_inv line 87

Source documentation

The full noncommutative derivative of matrix inversion.

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

theorem OAI.GAD.hasDerivAt_log_norm_of_mul line 109

Source documentation

Logarithmic norm differentiation, without choosing a complex logarithm branch.

theorem hasDerivAt_log_norm_of_mul {z : ℝ → ℂ} {w : ℂ} {t : ℝ}
    (hz : HasDerivAt z (z t * w) t) (h0 : z t ≠ 0) :
    HasDerivAt (fun s ↦ Real.log ‖z s‖) w.re t := by
…

theorem OAI.GAD.hasDerivAt_logNormDet line 130

Source documentation

Jacobi's formula for log absolute determinant, valid for every nonsingular complex matrix.

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

theorem OAI.GAD.trace_square_re_le line 149

Source documentation

Entrywise real trace bound, avoiding any norm convention for matrices.

theorem trace_square_re_le (B : Matrix ι ι ℂ) :
    (Matrix.trace (B * B)).re ≤ (Matrix.trace (B.conjTranspose * B)).re := by
…

theorem OAI.GAD.skew_one_add_isUnit line 169
Source documentation
A skew-Hermitian perturbation of the identity is nonsingular.
```
theorem skew_one_add_isUnit (K : Matrix ι ι ℂ) (hK : K.conjTranspose = -K) :
    IsUnit (1 + K) := by
…
```

theorem OAI.GAD.skew_resolvent_contraction line 182

Source documentation

The resolvent of a skew-Hermitian matrix is a contraction in quadratic-form order.

theorem skew_resolvent_contraction (K : Matrix ι ι ℂ) (hK : K.conjTranspose = -K) :
    (1 - ((1 + K)⁻¹).conjTranspose * (1 + K)⁻¹).PosSemidef := by
…

theorem OAI.GAD.skew_resolvent_trace_bound line 207

theorem OAI.GAD.skew_shift_trace_bound line 225

Source documentation

The Hessian bound at an arbitrary positive definite base point.

theorem skew_shift_trace_bound (D Z H : Matrix ι ι ℂ)
    (hD : D.PosDef) (hZ : Z.conjTranspose = -Z) (hH : H.IsHermitian) :
    IsUnit (D + Z) ∧
      (Matrix.trace (((D + Z)⁻¹ * H) * ((D + Z)⁻¹ * H))).re ≤
        (Matrix.trace ((D⁻¹ * H) * (D⁻¹ * H))).re := by
…