OAI/Analysis/JiangSu/Nonunital/CompactTraceBase.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalGamma.NormalizedTrace.toWeakDual_injective line 15
2. lemma OAI.NonunitalGamma.NormalizedTrace.continuous_eval line 24
3. lemma OAI.NonunitalGamma.NormalizedTrace.continuous_eval_re line 29
4. abbrev OAI.NonunitalGamma.StrictPositiveContraction line 33
5. lemma OAI.NonunitalGamma.strictPositiveContraction_directed line 36
6. theorem OAI.NonunitalGamma.uniform_trace_approximate_unit line 43
7. lemma OAI.NonunitalGamma.NormalizedTrace.unitized_inr line 79
8. lemma OAI.NonunitalGamma.nonunital_lp_unitized_nonneg line 85
9. theorem OAI.NonunitalGamma.exists_unit_representative line 100
10. lemma OAI.NonunitalGamma.weightBounded_denselyFinite line 161