OAI/Analysis/Cotype/ProjectionSemigroup.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.projectionSemigroup line 10
  2. def OAI.Cotype.projectionWeight line 13
  3. def OAI.Cotype.projectionLinearCoefficient line 16
  4. theorem OAI.Cotype.projectionSemigroup_average line 19
  5. theorem OAI.Cotype.projectionWeight_nonneg line 29
  6. theorem OAI.Cotype.projectionWeight_sum line 37
  7. theorem OAI.Cotype.projectionSubset_idempotent line 45
  8. theorem OAI.Cotype.projectionSubset_pairwise_commute line 50
  9. theorem OAI.Cotype.projectionSemigroup_power_bound_of_sign_deficit line 59
  10. theorem OAI.Cotype.projectionSemigroup_power_gap_of_bConvex line 72