OAI/Analysis/MatrixScaling/Determinant.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.scalingScalar line 15
2. theorem OAI.Kaplansky.scalingScalar_lower_small line 18

   Source documentation

   The endpoint lower bound which controls t approaching zero.

   theorem scalingScalar_lower_small {ε t : ℝ} (hε : 0 < ε) (ht : 0 < t) :
       -(3/2)*Real.log t ≤ scalingScalar ε t := by
   …

   Mentions: OAI.Kaplansky.scalingScalar

3. theorem OAI.Kaplansky.scalingScalar_lower_large line 25

   Source documentation

   The endpoint lower bound which controls t approaching infinity.

   theorem scalingScalar_lower_large {ε t : ℝ} (hε : 0 < ε) (ht : 0 < t) :
       2*Real.log ε + (1/2)*Real.log t ≤ scalingScalar ε t := by
   …

   Mentions: OAI.Kaplansky.scalingScalar

4. theorem OAI.Kaplansky.scalingScalar_bounded_below line 34

   Source documentation

   A uniform lower bound, without importing a minimizer assumption.

   theorem scalingScalar_bounded_below {ε t : ℝ} (hε : 0 < ε) (ht : 0 < t) :
       (3/2)*Real.log ε ≤ scalingScalar ε t := by
   …

   Mentions: OAI.Kaplansky.scalingScalar

5. theorem OAI.Kaplansky.scalingScalar_sublevel line 40
6. theorem OAI.Kaplansky.scaling_eigenvalue_bounds line 53
7. def OAI.Kaplansky.decreasingEigenvalues line 82

   Source documentation

   The ordered spectrum, with the matrix cardinality reduced to its size.

   def decreasingEigenvalues {r : ℕ} {A : Matrix (Fin r) (Fin r) ℂ}
       (hA : A.IsHermitian) : Fin r → ℝ :=
   …

8. theorem OAI.Kaplansky.decreasingEigenvalues_antitone line 86
9. theorem OAI.Kaplansky.det_one_add_eq_prod line 91
10. theorem OAI.Kaplansky.decreasingEigenvalues_nonneg line 109
11. theorem OAI.Kaplansky.log_det_one_add line 119

    Source documentation

    Real logarithm of the positive determinant, not the complex logarithm.

    theorem log_det_one_add {r : ℕ} {A : Matrix (Fin r) (Fin r) ℂ}
        (hA : A.PosSemidef) :
        Real.log ((1 + A).det.re) = ∑ i, Real.log (1 + decreasingEigenvalues hA.1 i) := by
    …

    Mentions: OAI.Kaplansky.decreasingEigenvalues

12. theorem OAI.Kaplansky.paired_log_sum line 125
13. theorem OAI.Kaplansky.scaling_log_det_of_spectral_bound line 160
14. def OAI.Kaplansky.scalingMap line 183
15. theorem OAI.Kaplansky.scalingMap_positive line 187
16. theorem OAI.Kaplansky.scalingMap_sub line 192
17. theorem OAI.Kaplansky.scalingMap_smul line 197
18. theorem OAI.Kaplansky.scalingMap_comparison line 202
19. theorem OAI.Kaplansky.sum_gram_mulVec_zero_iff line 209

    Source documentation

    A sum of Gram matrices has exactly the common kernel.

    theorem sum_gram_mulVec_zero_iff (B : Fin n → Matrix (Fin d) (Fin r) ℂ)
        (v : Fin r → ℂ) :
        (∑ i, (B i)ᴴ * B i) *ᵥ v = 0 ↔ ∀ i, B i *ᵥ v = 0 := by
    …

20. theorem OAI.Kaplansky.scalingMap_projection_kernel line 227
21. theorem OAI.Kaplansky.decreasingEigenvalues_pos_of_lt_rank line 239
22. def OAI.Kaplansky.collectiveMatrix line 282

    Source documentation

    Concatenation of all projected maps, whose range is their collective image.

    def collectiveMatrix (T : Fin n → Matrix (Fin r) (Fin d) ℂ)
        (p : Matrix (Fin d) (Fin d) ℂ) : Matrix (Fin r) (Fin n × Fin d) ℂ :=
    …

23. theorem OAI.Kaplansky.collectiveMatrix_mulVec line 286
24. theorem OAI.Kaplansky.collectiveMatrix_range line 292
25. theorem OAI.Kaplansky.scalingMap_eq_collective_gram line 318
26. theorem OAI.Kaplansky.scalingMap_projection_rank line 328
27. theorem OAI.Kaplansky.scalingMap_projection_positive line 345
28. theorem OAI.Kaplansky.scalingMap_projection_eigenvalue_pos line 353

    Source documentation

    Pointwise positivity of the 2s-th eigenvalue, with s=rank(p)>0. The uniform positive minimum over the projection bundle is still separate.

    theorem scalingMap_projection_eigenvalue_pos
        (T : Fin n → Matrix (Fin r) (Fin d) ℂ)
        (hexpand : ∀ S : Submodule ℂ (Fin d → ℂ),
          2 * Module.finrank ℂ S ≤ Module.finrank ℂ (⨆ i, S.map (T i).mulVecLin : Submodule ℂ (Fin r → ℂ)))
        {p : Matrix (Fin d) (Fin d) ℂ} (hp : p.IsHermitian) (hpp : p*p=p)
        (hpos : 0 < p.rank) :
        ∃ k : Fin r, k.val+1 = 2*p.rank ∧
          0 < decreasingEigenvalues (scalingMap_projection_positive T hp hpp).1 k := by
    …

    Mentions: OAI.Kaplansky.decreasingEigenvalues, OAI.Kaplansky.scalingMap_projection_positive