OAI/Analysis/Cotype/DualMomentLifts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.rademacherL1Linear line 12
  2. def OAI.Cotype.momentL1Linear line 18
  3. theorem OAI.Cotype.momentL1_rademacherL1 line 30
  4. theorem OAI.Cotype.rademacherL1_lower line 35
  5. def OAI.Cotype.singleL1Linear line 44
  6. def OAI.Cotype.singleL1 line 50
  7. theorem OAI.Cotype.singleL1_apply line 55
  8. theorem OAI.Cotype.finiteL2Dual_tuple_unit_bound line 58
  9. theorem OAI.Cotype.exists_dual_moment_lift_of_bound line 68
  10. theorem OAI.Cotype.exists_dual_moment_lift line 139