OAI/Analysis/Cotype/L2MomentLifts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.momentL2Linear line 11
  2. theorem OAI.Cotype.moment_norm_le_cubeL2 line 22
  3. theorem OAI.Cotype.momentL2Linear_bound line 26
  4. def OAI.Cotype.momentL2 line 38
  5. theorem OAI.Cotype.momentL2_apply line 42
  6. theorem OAI.Cotype.momentL2_surjective line 45
  7. theorem OAI.Cotype.momentL2_adjoint line 51
  8. theorem OAI.Cotype.momentL2_dual_bound line 63
  9. theorem OAI.Cotype.exists_L2_moment_lift line 83