OAI/Analysis/MatrixScaling/Spectrum.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.spectralForm line 17
2. theorem OAI.Kaplansky.basis_norm_sq line 20
3. theorem OAI.Kaplansky.basis_intersection_vector line 27

   Source documentation

   Two full bases have a nonzero vector in the first k+1 coordinates of one basis and in the last r-k coordinates of the other.

   theorem basis_intersection_vector (a b : OrthonormalBasis (Fin r) ℂ E) (k : Fin r) :
       ∃ x : E, x ≠ 0 ∧ (∀ i : Fin r, k < i → a.repr x i = 0) ∧
         (∀ i : Fin r, i < k → b.repr x i = 0) := by
   …

4. theorem OAI.Kaplansky.spectralForm_eigenvalue_mono line 77

   Source documentation

   The min--max comparison, proved by a dimension intersection and quadratic-form bounds in two orthonormal bases.

   theorem spectralForm_eigenvalue_mono
       (a b : OrthonormalBasis (Fin r) ℂ E) (e f : Fin r → ℝ)
       (he : Antitone e) (hf : Antitone f)
       (horder : ∀ x, spectralForm a e x ≤ spectralForm b f x) (k : Fin r) : e k ≤ f k := by
   …

   Mentions: OAI.Kaplansky.spectralForm

5. theorem OAI.Kaplansky.symmetric_spectralForm line 99
6. theorem OAI.Kaplansky.symmetric_eigenvalues_mono line 120

   Source documentation

   Eigenvalue monotonicity for symmetric operators from quadratic-form order.

   theorem symmetric_eigenvalues_mono [FiniteDimensional ℂ E]
       {T S : E →ₗ[ℂ] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
       (hn : Module.finrank ℂ E = r)
       (horder : ∀ x, (inner ℂ x (T x)).re ≤ (inner ℂ x (S x)).re) (k : Fin r) :
       hT.eigenvalues hn k ≤ hS.eigenvalues hn k := by
   …

7. theorem OAI.Kaplansky.decreasingEigenvalues_mono line 130
8. theorem OAI.Kaplansky.symmetric_eigenvalues_smul_le line 154
9. theorem OAI.Kaplansky.decreasingEigenvalues_smul_le line 170
10. theorem OAI.Kaplansky.quadraticForm_norm_bound line 195
11. theorem OAI.Kaplansky.spectralForm_add_const line 204
12. theorem OAI.Kaplansky.symmetric_eigenvalue_le_add_norm line 210
13. theorem OAI.Kaplansky.decreasingEigenvalues_sub_le_norm line 225

    Source documentation

    Ordered eigenvalues are 1-Lipschitz in the actual operator norm.

    theorem decreasingEigenvalues_sub_le_norm {A B : Matrix (Fin r) (Fin r) ℂ}
        (hA : A.IsHermitian) (hB : B.IsHermitian) (k : Fin r) :
        |decreasingEigenvalues hA k - decreasingEigenvalues hB k| ≤ ‖A-B‖ := by
    …

    Mentions: OAI.Kaplansky.decreasingEigenvalues

14. theorem OAI.Kaplansky.lipschitz_decreasingEigenvalues line 242
15. theorem OAI.Kaplansky.continuous_decreasingEigenvalues line 250
16. theorem OAI.Kaplansky.projection_eigenvalue_zero_or_one line 268
17. theorem OAI.Kaplansky.projection_trace_eq_rank line 283
18. abbrev OAI.Kaplansky.projectionSpace line 296

    Source documentation

    Orthogonal rank-s projections, represented by equations with continuous left-hand sides; the trace equation is equivalent to the rank condition.

    abbrev projectionSpace (d s : ℕ) :=
    …

19. theorem OAI.Kaplansky.projectionSpace_rank line 299
20. theorem OAI.Kaplansky.isCompact_projectionSpace line 304
21. instance OAI.Kaplansky.(instance at line 320) line 320