OAI/Analysis/KadisonKastler/UnitaryExponentialBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.exponentialPath line 17
2. theorem OAI.KadisonKastler.exponentialPath_deriv line 20
3. theorem OAI.KadisonKastler.exponentialPath_deriv_left line 30
4. theorem OAI.KadisonKastler.norm_expUnitary_sub_expUnitary_le line 40
5. theorem OAI.KadisonKastler.exponentialPath_zero line 70
6. theorem OAI.KadisonKastler.exponentialPath_one line 76
7. theorem OAI.KadisonKastler.exponentialPath_sub_one_le line 83
8. def OAI.KadisonKastler.exponentialGenerator line 89
9. theorem OAI.KadisonKastler.exponentialGenerator_star line 92
10. theorem OAI.KadisonKastler.exponentialGenerator_norm line 98
11. def OAI.KadisonKastler.conjugationPath line 102
12. theorem OAI.KadisonKastler.conjugationPath_deriv line 105
13. theorem OAI.KadisonKastler.conjugationPath_sub_le line 126
14. def OAI.KadisonKastler.conjugationRemainder line 137
15. def OAI.KadisonKastler.conjugationRemainderDerivative line 142
16. theorem OAI.KadisonKastler.conjugationRemainder_deriv line 147
17. theorem OAI.KadisonKastler.conjugationRemainderDerivative_norm_le line 158
18. theorem OAI.KadisonKastler.conjugationRemainder_norm_le line 175

    Source documentation

    The first-order conjugation formula with a uniform quadratic remainder.

    private theorem conjugationRemainder_norm_le
        (h : selfAdjoint (H →L[ℂ] H)) (x : H →L[ℂ] H) :
        ‖conjugationRemainder h x 1‖ ≤
            4 * ‖(h : H →L[ℂ] H)‖ ^ 2 * ‖x‖ := by
    …

    Mentions: OAI.KadisonKastler.conjugationRemainder

19. theorem OAI.KadisonKastler.norm_expUnitary_conjugation_remainder_le line 186

    Source documentation

    First-order conjugation by an exponential, with a quadratic norm remainder.

    theorem norm_expUnitary_conjugation_remainder_le
        (h : selfAdjoint (H →L[ℂ] H)) (x : H →L[ℂ] H) :
        ‖unitaryConj (H := H) (selfAdjoint.expUnitary h) x - x -
    …

    Mentions: OAI.KadisonKastler.unitaryConj