Commit 2023-05-26 22:04 65926b16

View on Github →

feat: port Analysis.NormedSpace.PiLp (#4345)

Estimated changes

added theorem PiLp.add_apply
added theorem PiLp.aux_cobounded_eq
added theorem PiLp.aux_uniformity_eq
added def PiLp.basisFun
added theorem PiLp.basisFun_apply
added theorem PiLp.basisFun_equivFun
added theorem PiLp.basisFun_map
added theorem PiLp.basisFun_repr
added theorem PiLp.continuous_equiv
added theorem PiLp.dist_eq_card
added theorem PiLp.dist_eq_iSup
added theorem PiLp.dist_eq_of_L2
added theorem PiLp.dist_eq_sum
added theorem PiLp.edist_eq_card
added theorem PiLp.edist_eq_iSup
added theorem PiLp.edist_eq_of_L2
added theorem PiLp.edist_eq_sum
added theorem PiLp.equiv_add
added theorem PiLp.equiv_apply
added theorem PiLp.equiv_neg
added theorem PiLp.equiv_smul
added theorem PiLp.equiv_sub
added theorem PiLp.equiv_symm_add
added theorem PiLp.equiv_symm_apply
added theorem PiLp.equiv_symm_neg
added theorem PiLp.equiv_symm_smul
added theorem PiLp.equiv_symm_sub
added theorem PiLp.equiv_symm_zero
added theorem PiLp.equiv_zero
added def PiLp.equivₗᵢ
added theorem PiLp.neg_apply
added theorem PiLp.nndist_eq_iSup
added theorem PiLp.nndist_eq_of_L2
added theorem PiLp.nndist_eq_sum
added theorem PiLp.nnnorm_eq_ciSup
added theorem PiLp.nnnorm_eq_of_L2
added theorem PiLp.nnnorm_eq_sum
added theorem PiLp.norm_eq_card
added theorem PiLp.norm_eq_ciSup
added theorem PiLp.norm_eq_of_L2
added theorem PiLp.norm_eq_of_nat
added theorem PiLp.norm_eq_sum
added theorem PiLp.norm_sq_eq_of_L2
added theorem PiLp.smul_apply
added theorem PiLp.sub_apply
added theorem PiLp.zero_apply
added def PiLp