OAI/Analysis/DiamondDistortion/LpDual.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DiamondDistortion.LpDual.finite line 21
  2. lemma OAI.DiamondDistortion.LpDual.finite_apply line 29
  3. lemma OAI.DiamondDistortion.LpDual.finite_injective line 30
  4. lemma OAI.DiamondDistortion.LpDual.finite_norm_add line 34
  5. lemma OAI.DiamondDistortion.LpDual.small_tail_upper line 52
  6. lemma OAI.DiamondDistortion.LpDual.small_tail line 115
  7. lemma OAI.DiamondDistortion.LpDual.finite_single line 126
  8. lemma OAI.DiamondDistortion.LpDual.finite_dense line 134
  9. def OAI.DiamondDistortion.LpDual.dualInclude line 143
  10. lemma OAI.DiamondDistortion.LpDual.dualInclude_apply line 145
  11. def OAI.DiamondDistortion.LpDual.dualHead line 148
  12. lemma OAI.DiamondDistortion.LpDual.dualHead_apply line 150
  13. lemma OAI.DiamondDistortion.LpDual.finite_filter line 156
  14. lemma OAI.DiamondDistortion.LpDual.finite_filter_norm line 174
  15. lemma OAI.DiamondDistortion.LpDual.dual_approximation line 181
  16. lemma OAI.DiamondDistortion.LpDual.dual_separable line 212