OAI/Analysis/CharacterCriterion/SignObstruction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.derivative_eq_zero_of_concave_bddBelow line 22
2. def OAI.KirchbergRordam.GenericRW.DoubleCommutator.bracket line 50
3. def OAI.KirchbergRordam.GenericRW.DoubleCommutator.orbit line 52
4. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.derivative_orbit line 54
5. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.bracket_smul_left line 68
6. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.bracket_smul_right line 72
7. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.bracket_I_twice line 76
8. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.star_rotation line 82
9. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.norm_orbit line 88
10. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.selfAdjoint_I_bracket line 98
11. def OAI.KirchbergRordam.GenericRW.DoubleCommutator.quadratic line 110
12. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.quadratic_apply line 115
13. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.quadratic_derivative line 118
14. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.quadratic_orbit_lower line 123
15. lemma OAI.KirchbergRordam.GenericRW.DoubleCommutator.quadratic_orbit_nonneg line 129
16. theorem OAI.KirchbergRordam.GenericRW.commute_of_positive_double_commutator line 141
17. theorem OAI.KirchbergRordam.GenericRW.commute_of_negative_double_commutator line 182
18. lemma OAI.KirchbergRordam.GenericRW.Fullness.doubleBracket_selfAdjoint line 198
19. theorem OAI.KirchbergRordam.GenericRW.Fullness.full_parts line 205