OAI/Analysis/MatrixScaling/Canonical.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.frameTuple line 14
2. theorem OAI.Kaplansky.scalingMap_frame line 18
3. theorem OAI.Kaplansky.det_unitary_conjugate line 28
4. theorem OAI.Kaplansky.scalingPotential_frame line 37
5. theorem OAI.Kaplansky.posDef_unitary_conjugate line 47
6. theorem OAI.Kaplansky.scaling_minimizer_frame line 56

   Source documentation

   A minimizer transports to any other unitary frame.

   theorem scaling_minimizer_frame (T : Fin n → Matrix (Fin r) (Fin d) ℂ)
       (U : Matrix (Fin d) (Fin d) ℂ) (V : Matrix (Fin r) (Fin r) ℂ)
       (hU : Uᴴ * U = 1) (hU' : U * Uᴴ = 1)
       (hV : Vᴴ * V = 1) (hV' : V * Vᴴ = 1)
       (P : Matrix (Fin d) (Fin d) ℂ) (hP : P.PosDef)
       (hmin : ∀ R, R.PosDef → scalingPotential T P ≤ scalingPotential T R) :
       (U * P * Uᴴ).PosDef ∧ ∀ R, R.PosDef →
         scalingPotential (frameTuple T U V) (U * P * Uᴴ) ≤
           scalingPotential (frameTuple T U V) R := by
   …

   Mentions: OAI.Kaplansky.scalingPotential, OAI.Kaplansky.frameTuple

7. theorem OAI.Kaplansky.sqrt_unitary_conjugate line 77

   Source documentation

   The positive square root, not an arbitrary Gram factor, is equivariant.

   theorem sqrt_unitary_conjugate (U P : Matrix (Fin d) (Fin d) ℂ)
       (hU : Uᴴ * U = 1) (hP : P.PosSemidef) :
       CFC.sqrt (U * P * Uᴴ) = U * CFC.sqrt P * Uᴴ := by
   …

8. def OAI.Kaplansky.Expanding line 98
9. def OAI.Kaplansky.canonicalMinimizer line 102
10. theorem OAI.Kaplansky.canonicalMinimizer_spec line 105
11. theorem OAI.Kaplansky.canonicalMinimizer_frame line 110
12. def OAI.Kaplansky.canonicalScaling line 121
13. theorem OAI.Kaplansky.canonicalScaling_relations line 125
14. theorem OAI.Kaplansky.inverse_unitary_conjugate line 135
15. theorem OAI.Kaplansky.canonicalScaling_frame line 144

    Source documentation

    The normalized maps obey precisely the bundle transition law.

    theorem canonicalScaling_frame (T : Fin n → Matrix (Fin r) (Fin d) ℂ)
        (U : Matrix (Fin d) (Fin d) ℂ) (V : Matrix (Fin r) (Fin r) ℂ)
        (hU : Uᴴ * U = 1) (hU' : U * Uᴴ = 1)
        (hV : Vᴴ * V = 1) (hV' : V * Vᴴ = 1)
        (h : Expanding T) (h' : Expanding (frameTuple T U V)) :
        canonicalScaling (frameTuple T U V) h' = frameTuple (canonicalScaling T h) U V := by
    …

    Mentions: OAI.Kaplansky.Expanding, OAI.Kaplansky.frameTuple, OAI.Kaplansky.canonicalScaling

16. theorem OAI.Kaplansky.continuous_canonicalMinimizer line 164

    Source documentation

    Continuity of the canonical, hence frame-compatible, choice.

    theorem continuous_canonicalMinimizer {Y : Type*} [TopologicalSpace Y] [CompactSpace Y]
        (T : Y → Fin n → Matrix (Fin r) (Fin d) ℂ) (hT : Continuous T)
        (h : ∀ y, Expanding (T y)) : Continuous (fun y => canonicalMinimizer (T y) (h y)) := by
    …

    Mentions: OAI.Kaplansky.Expanding, OAI.Kaplansky.canonicalMinimizer

17. theorem OAI.Kaplansky.continuous_canonicalScaling line 173
18. theorem OAI.Kaplansky.continuous_canonicalScaling_local line 200
19. theorem OAI.Kaplansky.continuous_canonicalMinimizer_local line 215

    Source documentation

    The same localization for the positive endomorphism before normalization.

    theorem continuous_canonicalMinimizer_local {Y : Type*} [TopologicalSpace Y]
        [WeaklyLocallyCompactSpace Y]
        (T : Y → Fin n → Matrix (Fin r) (Fin d) ℂ) (hT : Continuous T)
        (h : ∀ y, Expanding (T y)) : Continuous (fun y => canonicalMinimizer (T y) (h y)) := by
    …

    Mentions: OAI.Kaplansky.Expanding, OAI.Kaplansky.canonicalMinimizer