OAI/Analysis/JiangSu/Nonunital/TraceRays.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NonunitalGamma.functionalWeight line 15
  2. lemma OAI.NonunitalGamma.functionalWeight_bounded line 30
  3. lemma OAI.NonunitalGamma.functionalWeight_recover line 40
  4. lemma OAI.NonunitalGamma.positiveFunctional_ext_of_nonneg line 49
  5. lemma OAI.NonunitalGamma.functionalWeight_injective line 59
  6. lemma OAI.NonunitalGamma.normalizedWeight_ray line 72
  7. def OAI.NonunitalGamma.NormalizedTrace.twoNorm line 100
  8. lemma OAI.NonunitalGamma.NormalizedTrace.twoNorm_nonneg line 103
  9. lemma OAI.NonunitalGamma.NormalizedTrace.twoNorm_zero line 106
  10. lemma OAI.NonunitalGamma.NormalizedTrace.twoNorm_add_le line 109
  11. lemma OAI.NonunitalGamma.NormalizedTrace.twoNorm_neg line 114
  12. lemma OAI.NonunitalGamma.NormalizedTrace.twoNorm_mul_left line 118
  13. lemma OAI.NonunitalGamma.NormalizedTrace.twoNorm_mul_right line 123
  14. lemma OAI.NonunitalGamma.NormalizedTrace.norm_le_twoNorm line 128
  15. lemma OAI.NonunitalGamma.NormalizedTrace.twoNorm_eq line 132
  16. lemma OAI.NonunitalGamma.NormalizedTrace.continuous_twoNorm line 137
  17. def OAI.NonunitalGamma.NormalizedTrace.nullIdeal line 142
  18. lemma OAI.NonunitalGamma.NormalizedTrace.nullIdeal_isClosed line 155
  19. lemma OAI.NonunitalGamma.NormalizedTrace.nullIdeal_eq_bot line 160
  20. theorem OAI.NonunitalGamma.NormalizedTrace.faithful line 173