Commit 2023-06-01 05:16 bc20bc99

View on Github →

feat: port Analysis.NormedSpace.LpSpace (#4465) Notes Zulip thread :

  1. There are both CoeOut and CoeFun instances for lp E p. This is consistent with mathlib3, but it seems strange and I would expect it to cause problems.
  2. It seems there is some defeq abuse (identifiying PreLp E with ∀ i, E i in the aforementioned CoeOut instance, for example) happening here which is rather convenient, but it's possible it may cause problems. (this abuse was also present in mathlib3)
  3. What should the name of this file be? LpSpace seems wrong semantically, but lpSpace doesn't seem allowable by our file name conventions.

Estimated changes

added theorem Memℓp.add
added theorem Memℓp.bddAbove
added theorem Memℓp.const_mul
added theorem Memℓp.const_smul
added theorem Memℓp.finset_sum
added theorem Memℓp.infty_mul
added theorem Memℓp.infty_pow
added theorem Memℓp.neg
added theorem Memℓp.neg_iff
added theorem Memℓp.of_exponent_ge
added theorem Memℓp.star_iff
added theorem Memℓp.star_mem
added theorem Memℓp.sub
added theorem Memℓp.summable
added def Memℓp
added def PreLp
added theorem int_cast_memℓp_infty
added theorem lp.coeFn_add
added theorem lp.coeFn_neg
added theorem lp.coeFn_smul
added theorem lp.coeFn_star
added theorem lp.coeFn_sub
added theorem lp.coeFn_sum
added theorem lp.coeFn_zero
added theorem lp.coe_lpSubmodule
added theorem lp.eq_zero'
added theorem lp.ext
added theorem lp.hasSum_norm
added theorem lp.infty_coeFn_mul
added theorem lp.infty_coeFn_one
added theorem lp.infty_coeFn_pow
added theorem lp.isLUB_norm
added theorem lp.mem_lp_const_smul
added theorem lp.memℓp_of_tendsto
added theorem lp.norm_apply_le_norm
added theorem lp.norm_const_smul
added theorem lp.norm_const_smul_le
added theorem lp.norm_eq_ciSup
added theorem lp.norm_eq_tsum_rpow
added theorem lp.norm_eq_zero_iff
added theorem lp.norm_le_of_tendsto
added theorem lp.norm_le_of_tsum_le
added theorem lp.norm_neg
added theorem lp.norm_nonneg'
added theorem lp.norm_rpow_eq_tsum
added theorem lp.norm_zero
added def lp
added def lpInftySubring
added def lpSubmodule
added theorem memℓp_gen'
added theorem memℓp_gen
added theorem memℓp_gen_iff
added theorem memℓp_infty
added theorem memℓp_infty_iff
added theorem memℓp_zero
added theorem memℓp_zero_iff
added theorem nat_cast_memℓp_infty
added theorem one_memℓp_infty
added theorem zero_mem_ℓp'
added theorem zero_memℓp