OAI/Analysis/MatrixScaling/Minimizer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kaplansky.posDef_det_re_pos line 13
2. theorem OAI.Kaplansky.continuousOn_scalingPotential line 17
3. theorem OAI.Kaplansky.scaling_minimum_of_sublevel_bound line 38

   Source documentation

   Minimizing on a spectral window gives a global minimum when all points below the comparison value lie in the window.

   theorem scaling_minimum_of_sublevel_bound
       (T : Fin n → Matrix (Fin r) (Fin d) ℂ) {a b C : ℝ} (ha : 0 < a) (hb : 0 ≤ b)
       (hbound : ∀ (P : Matrix (Fin d) (Fin d) ℂ) (hP : P.PosDef),
         scalingPotential T P ≤ C → (⟨P,hP.1⟩ : HermitianMatrices d) ∈ spectralWindow d a b)
       (Q : Matrix (Fin d) (Fin d) ℂ) (hQ : Q.PosDef) (hQC : scalingPotential T Q ≤ C) :
       ∃ P : Matrix (Fin d) (Fin d) ℂ, P.PosDef ∧
         ∀ R : Matrix (Fin d) (Fin d) ℂ, R.PosDef → scalingPotential T P ≤ scalingPotential T R := by
   …

   Mentions: OAI.Kaplansky.scalingPotential, OAI.Kaplansky.HermitianMatrices, OAI.Kaplansky.spectralWindow

4. theorem OAI.Kaplansky.scaling_minimizer_exists line 55
5. theorem OAI.Kaplansky.scaling_minimizer_unique line 84
6. theorem OAI.Kaplansky.existsUnique_scaling_minimizer line 110