OAI/Analysis/Quasitrace/Order.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kaplansky.OneQuasitrace.map_nonneg line 18

   Source documentation

   Positivity on all positive elements follows from the square axiom.

   theorem OneQuasitrace.map_nonneg (τ : OneQuasitrace A) {a : A} (ha : 0 ≤ a) :
       0 ≤ τ a := by
   …

   Mentions: OAI.Kaplansky.OneQuasitrace

2. theorem OAI.Kaplansky.OneQuasitrace.scalar_upper_bound line 23
3. theorem OAI.Kaplansky.OneQuasitrace.unit_nonneg line 46
4. theorem OAI.Kaplansky.OneQuasitrace.selfAdjoint_re_upper line 51

   Source documentation

   The scalar upper estimate also applies to arbitrary self-adjoints; positivity is needed only for the scalar difference.

   theorem OneQuasitrace.selfAdjoint_re_upper (τ : OneQuasitrace A)
       {a : A} (ha : IsSelfAdjoint a) : (τ a).re ≤ ‖a‖ * (τ 1).re := by
   …

   Mentions: OAI.Kaplansky.OneQuasitrace

5. theorem OAI.Kaplansky.OneQuasitrace.selfAdjoint_im_zero line 63
6. theorem OAI.Kaplansky.OneQuasitrace.norm_selfAdjoint_le line 76
7. theorem OAI.Kaplansky.OneQuasitrace.norm_le_twice line 88

   Source documentation

   A uniform pointwise bound without global additivity or continuity of τ. This supplies compact coordinate disks for the existence problem.

   theorem OneQuasitrace.norm_le_twice (τ : OneQuasitrace A) (a : A) :
       ‖τ a‖ ≤ 2 * ‖a‖ * (τ 1).re := by
   …

   Mentions: OAI.Kaplansky.OneQuasitrace

8. theorem OAI.Kaplansky.OneQuasitrace.normalized_norm_le line 107