Commit 2023-09-29 14:27 6d73bdfd

View on Github →

feat(Analysis): add WithLp for products (#6136) The file NormedSpace.ProdLp is copied from NormedSpace.PiLp with a two changes

  • For p = 0 we define the distance by using and if-else block which in turn makes it necessary to add some classicality assumptions
  • We omit the sections about basis and constant maps

Estimated changes

added theorem WithLp.add_fst
added theorem WithLp.add_snd
added theorem WithLp.equiv_fst
added theorem WithLp.equiv_snd
added theorem WithLp.equiv_symm_fst
added theorem WithLp.equiv_symm_snd
added theorem WithLp.neg_fst
added theorem WithLp.neg_snd
added theorem WithLp.prod_edist_comm
added theorem WithLp.prod_edist_self
added theorem WithLp.smul_fst
added theorem WithLp.smul_snd
added theorem WithLp.sub_fst
added theorem WithLp.sub_snd
added theorem WithLp.zero_fst
added theorem WithLp.zero_snd