Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-01 02:32 1594b0ca

View on Github →

feat(normed_space/lp_space): Lp space for Π i, E i (#11015) For a family Π i, E i of normed spaces, define the subgroup with finite lp norm, and prove it is a normed_group. Many parts adapted from the development of measure_theory.Lp by @RemyDegenne. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lp.20space

Estimated changes

added theorem lp.coe_fn_add
added theorem lp.coe_fn_neg
added theorem lp.coe_fn_smul
added theorem lp.coe_fn_sub
added theorem lp.coe_fn_zero
added theorem lp.coe_lp_submodule
added theorem lp.eq_zero'
added theorem lp.ext
added theorem lp.has_sum_norm
added theorem lp.is_lub_norm
added def lp.lp_submodule
added theorem lp.mem_lp_const_smul
added theorem lp.norm_const_smul
added theorem lp.norm_eq_csupr
added theorem lp.norm_eq_tsum_rpow
added theorem lp.norm_eq_zero_iff
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 theorem mem_ℓp.add
added theorem mem_ℓp.bdd_above
added theorem mem_ℓp.const_mul
added theorem mem_ℓp.const_smul
added theorem mem_ℓp.finset_sum
added theorem mem_ℓp.neg
added theorem mem_ℓp.neg_iff
added theorem mem_ℓp.sub
added theorem mem_ℓp.summable
added def mem_ℓp
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 def pre_lp
added theorem zero_mem_ℓp'
added theorem zero_mem_ℓp
added theorem real.rpow_left_inj_on