Critical.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Log-determinant derivatives, critical points, and normalized tuple relations.

theorem OAI.Kaplansky.posDef_iff_decreasing_pos line 16
theorem OAI.Kaplansky.isOpen_posDef_hermitian line 27
theorem OAI.Kaplansky.eventually_posDef_add_smul line 39
Source documentation
A Hermitian direction remains in the positive cone near a positive point, providing the open domain needed for the critical-point argument.
```
theorem eventually_posDef_add_smul {P K : Matrix (Fin d) (Fin d) ℂ}
    (hP : P.PosDef) (hK : K.IsHermitian) :
    ∀ᶠ u : ℝ in 𝓝 0, (P+(u : ℂ) • K).PosDef := by
…
```
theorem OAI.Kaplansky.hasDerivAt_det_add_smul line 66
Source documentation
Jacobi's directional formula, derived from the polynomial determinant expansion at the identity and an actual inverse factorization.
```
theorem hasDerivAt_det_add_smul (P K : Matrix (Fin d) (Fin d) ℂ) (hP : IsUnit P) :
    HasDerivAt (fun z : ℂ => (P+z • K).det) (P.det * (P⁻¹*K).trace) 0 := by
…
```
theorem OAI.Kaplansky.hasDerivAt_log_det_add_smul line 88
def OAI.Kaplansky.scalingAdjoint line 114
theorem OAI.Kaplansky.scalingAdjoint_trace line 118
theorem OAI.Kaplansky.scalingAdjoint_positive line 127
theorem OAI.Kaplansky.hasDerivAt_scalingPotential line 132
theorem OAI.Kaplansky.scaling_minimizer_critical line 151
def OAI.Kaplansky.normalizedTuple line 200
theorem OAI.Kaplansky.normalizedTuple_column line 205
theorem OAI.Kaplansky.normalizedTuple_row line 219