OAI/Analysis/Cotype/FiniteL2Dual.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.finiteL2DualLinear line 14
  2. theorem OAI.Cotype.finiteL2DualLinear_bound line 19
  3. def OAI.Cotype.finiteL2Dual line 28
  4. theorem OAI.Cotype.finiteL2Dual_apply line 32
  5. theorem OAI.Cotype.finiteL2Dual_norm_le line 35
  6. def OAI.Cotype.probabilityL2Vector line 39
  7. def OAI.Cotype.probabilityL2Dual line 42
  8. theorem OAI.Cotype.probabilityL2Vector_norm line 46
  9. theorem OAI.Cotype.probabilityL2Dual_norm_le line 51
  10. theorem OAI.Cotype.probabilityL2Dual_amplification line 57