OAI/Analysis/Cotype/ProjectionGenerator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.complexSpectralEval_const line 13
  2. def OAI.Cotype.complexProjectionSpectralHom line 19
  3. def OAI.Cotype.projectionGenerator line 35
  4. def OAI.Cotype.complexProjectionTime line 39
  5. theorem OAI.Cotype.complexProjectionTime_eq_exp line 43
  6. theorem OAI.Cotype.complexProjectionTime_real line 59
  7. theorem OAI.Cotype.complexProjectionTime_real_norm_le line 65
  8. theorem OAI.Cotype.complexProjectionTime_real_power_gap line 74