OAI/Analysis/MatrixScaling/Bounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.spectralIndex line 14
2. theorem OAI.Kaplansky.eigenvalues_spectralIndex line 18
3. theorem OAI.Kaplansky.decreasingEigenvalues_pos line 25
4. theorem OAI.Kaplansky.exists_top_spectral_projection line 30
5. theorem OAI.Kaplansky.continuous_scalingMap line 95
6. theorem OAI.Kaplansky.uniform_projection_spectral_bound line 104
7. theorem OAI.Kaplansky.expansion_dimension line 163
8. theorem OAI.Kaplansky.scaling_spectral_bound line 174
9. theorem OAI.Kaplansky.uniform_scaling_estimate line 196
10. theorem OAI.Kaplansky.uniform_scaling_log_det line 218

    Source documentation

    The uniform determinant bound with no extra dimension or nonempty-base hypothesis. The dimension inequality is deduced from expansion when needed.

    theorem uniform_scaling_log_det {Y : Type*} [TopologicalSpace Y] [CompactSpace Y]
        (T : Y → Fin n → Matrix (Fin r) (Fin d) ℂ) (hT : Continuous T)
        (hexpand : ∀ y (S : Submodule ℂ (Fin d → ℂ)),
          2 * Module.finrank ℂ S ≤
            Module.finrank ℂ (⨆ i, S.map (T y i).mulVecLin : Submodule ℂ (Fin r → ℂ))) :
        ∃ ε : ℝ, 0 < ε ∧ ∀ y (P : Matrix (Fin d) (Fin d) ℂ) (hP : P.PosDef),
          2 * ∑ s, Real.log (1+ε*decreasingEigenvalues hP.1 s) ≤
            Real.log ((1+scalingMap (T y) P).det.re) := by
    …

    Mentions: OAI.Kaplansky.decreasingEigenvalues, OAI.Kaplansky.scalingMap

11. theorem OAI.Kaplansky.det_eq_prod_decreasing line 247
12. theorem OAI.Kaplansky.log_det_posDef line 255
13. def OAI.Kaplansky.scalingPotential line 260
14. theorem OAI.Kaplansky.scalingScalar_sum_le_potential line 264
15. theorem OAI.Kaplansky.uniform_scaling_sublevels line 274
16. abbrev OAI.Kaplansky.HermitianMatrices line 301
17. instance OAI.Kaplansky.(instance at line 303) line 303
18. def OAI.Kaplansky.spectralWindow line 306
19. theorem OAI.Kaplansky.isClosed_spectralWindow line 309
20. theorem OAI.Kaplansky.norm_le_of_decreasingEigenvalues line 316
21. theorem OAI.Kaplansky.isCompact_spectralWindow line 330
22. theorem OAI.Kaplansky.spectralWindow_posDef line 340