OAI/Analysis/LipschitzFree/Coefficients.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Absolutely summable coefficients of bounded separated Lipschitz-free spaces

  1. abbrev OAI.DiscreteFree.Coefficients.L1 line 20
  2. theorem OAI.DiscreteFree.Coefficients.norm_eq_tsum line 22
  3. theorem OAI.DiscreteFree.Coefficients.summable_abs line 25
  4. theorem OAI.DiscreteFree.Coefficients.sum_abs_le line 28
  5. def OAI.DiscreteFree.Coefficients.analysisLinear line 34
  6. theorem OAI.DiscreteFree.Coefficients.analysisLinear_apply line 42
  7. theorem OAI.DiscreteFree.Coefficients.analysis_bound line 45
  8. def OAI.DiscreteFree.Coefficients.analysis line 49
  9. theorem OAI.DiscreteFree.Coefficients.analysis_apply line 52
  10. theorem OAI.DiscreteFree.Coefficients.term_bound line 58
  11. theorem OAI.DiscreteFree.Coefficients.summable_term_norm line 63
  12. theorem OAI.DiscreteFree.Coefficients.summable_term line 68
  13. def OAI.DiscreteFree.Coefficients.synthesisLinear line 71
  14. theorem OAI.DiscreteFree.Coefficients.synthesis_bound line 80
  15. def OAI.DiscreteFree.Coefficients.synthesis line 90
  16. theorem OAI.DiscreteFree.Coefficients.synthesis_apply line 93
  17. theorem OAI.DiscreteFree.Coefficients.synthesis_single line 96
  18. theorem OAI.DiscreteFree.Coefficients.analysis_delta line 103
  19. theorem OAI.DiscreteFree.Coefficients.analysis_synthesis line 116
  20. theorem OAI.DiscreteFree.Coefficients.synthesis_analysis line 130
  21. def OAI.DiscreteFree.Coefficients.equiv line 151
  22. theorem OAI.DiscreteFree.Coefficients.equiv_apply line 160
  23. theorem OAI.DiscreteFree.Coefficients.equiv_bounds line 163