OAI/Analysis/BoundedHochschild/DiffuseProjections.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Diffuse projections of prescribed trace and conjugation estimates.

  1. def OAI.HochschildDiffuse.NoMinimalProjections line 35
  2. lemma OAI.HochschildDiffuse.projection_trace_pos line 39
  3. theorem OAI.HochschildDiffuse.exists_half_subprojection line 52
  4. theorem OAI.HochschildDiffuse.exists_small_subprojection line 66
  5. lemma OAI.HochschildDiffuse.projection_le_of_comparable_trace_le line 88
  6. theorem OAI.HochschildDiffuse.projection_chain_upper line 110
  7. theorem OAI.HochschildDiffuse.exists_projection_of_trace line 154
  8. theorem OAI.HochschildDixmier.norm_sub_trace_le_of_conjugations line 215