OAI/Analysis/Cotype/Moments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.average_sum line 12
  2. theorem OAI.Cotype.average_smul_const line 17
  3. def OAI.Cotype.unitIndex line 22
  4. theorem OAI.Cotype.character_unitIndex line 24
  5. theorem OAI.Cotype.unitIndex_injective line 28
  6. theorem OAI.Cotype.coordinate_orthogonality line 33
  7. theorem OAI.Cotype.moment_rademacherSum line 39
  8. theorem OAI.Cotype.moment_surjective line 46
  9. theorem OAI.Cotype.radProjection_rademacherSum line 51
  10. theorem OAI.Cotype.radProjection_idempotent line 58