mathlibdocumentation

analysis.normed_space.lp_space

ℓp space #

This file describes properties of elements `f` of a pi-type `Π i, E i` with finite "norm", defined for `p:ℝ≥0∞` as the size of the support of `f` if `p=0`, `(∑' a, ‖f a‖^p) ^ (1/p)` for `0 < p < ∞` and `⨆ a, ‖f a‖` for `p=∞`.

The Prop-valued `mem_ℓp f p` states that a function `f : Π i, E i` has finite norm according to the above definition; that is, `f` has finite support if `p = 0`, `summable (λ a, ‖f a‖^p)` if `0 < p < ∞`, and `bdd_above (norm '' (set.range f))` if `p = ∞`.

The space `lp E p` is the subtype of elements of `Π i : α, E i` which satisfy `mem_ℓp f p`. For `1 ≤ p`, the "norm" is genuinely a norm and `lp` is a complete metric space.

Main definitions #

• `mem_ℓp f p` : property that the function `f` satisfies, as appropriate, `f` finitely supported if `p = 0`, `summable (λ a, ‖f a‖^p)` if `0 < p < ∞`, and `bdd_above (norm '' (set.range f))` if `p = ∞`.
• `lp E p` : elements of `Π i : α, E i` such that `mem_ℓp f p`. Defined as an `add_subgroup` of a type synonym `pre_lp` for `Π i : α, E i`, and equipped with a `normed_add_comm_group` structure. Under appropriate conditions, this is also equipped with the instances `lp.normed_space`, `lp.complete_space`. For `p=∞`, there is also `lp.infty_normed_ring`, `lp.infty_normed_algebra`, `lp.infty_star_ring` and `lp.infty_cstar_ring`.

Main results #

• `mem_ℓp.of_exponent_ge`: For `q ≤ p`, a function which is `mem_ℓp` for `q` is also `mem_ℓp` for `p`
• `lp.mem_ℓp_of_tendsto`, `lp.norm_le_of_tendsto`: A pointwise limit of functions in `lp`, all with `lp` norm `≤ C`, is itself in `lp` and has `lp` norm `≤ C`.
• `lp.tsum_mul_le_mul_norm`: basic form of Hölder's inequality

Implementation #

Since `lp` is defined as an `add_subgroup`, dot notation does not work. Use `lp.norm_neg f` to say that `‖-f‖ = ‖f‖`, instead of the non-working `f.norm_neg`.

TODO #

• More versions of Hölder's inequality (for example: the case `p = 1`, `q = ∞`; a version for normed rings which has `‖∑' i, f i * g i‖` rather than `∑' i, ‖f i‖ * g i‖` on the RHS; a version for three exponents satisfying `1 / r = 1 / p + 1 / q`)

`mem_ℓp` predicate #

def mem_ℓp {α : Type u_1} {E : α Type u_2} [Π (i : α), ] (f : Π (i : α), E i) (p : ennreal) :
Prop

The property that `f : Π i : α, E i`

• is finitely supported, if `p = 0`, or
• admits an upper bound for `set.range (λ i, ‖f i‖)`, if `p = ∞`, or
• has the series `∑' i, ‖f i‖ ^ p` be summable, if `0 < p < ∞`.
Equations
theorem mem_ℓp_zero_iff {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {f : Π (i : α), E i} :
0 {i : α | f i 0}.finite
theorem mem_ℓp_zero {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {f : Π (i : α), E i} (hf : {i : α | f i 0}.finite) :
0
theorem mem_ℓp_infty_iff {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {f : Π (i : α), E i} :
bdd_above (set.range (λ (i : α), f i))
theorem mem_ℓp_infty {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {f : Π (i : α), E i} (hf : bdd_above (set.range (λ (i : α), f i))) :
theorem mem_ℓp_gen_iff {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) {f : Π (i : α), E i} :
p summable (λ (i : α), f i ^ p.to_real)
theorem mem_ℓp_gen {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f : Π (i : α), E i} (hf : summable (λ (i : α), f i ^ p.to_real)) :
p
theorem mem_ℓp_gen' {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {C : } {f : Π (i : α), E i} (hf : (s : finset α), s.sum (λ (i : α), f i ^ p.to_real) C) :
p
theorem zero_mem_ℓp {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] :
p
theorem zero_mem_ℓp' {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] :
mem_ℓp (λ (i : α), 0) p
theorem mem_ℓp.finite_dsupport {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {f : Π (i : α), E i} (hf : 0) :
{i : α | f i 0}.finite
theorem mem_ℓp.bdd_above {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {f : Π (i : α), E i} (hf : ) :
bdd_above (set.range (λ (i : α), f i))
theorem mem_ℓp.summable {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) {f : Π (i : α), E i} (hf : p) :
summable (λ (i : α), f i ^ p.to_real)
theorem mem_ℓp.neg {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f : Π (i : α), E i} (hf : p) :
mem_ℓp (-f) p
@[simp]
theorem mem_ℓp.neg_iff {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f : Π (i : α), E i} :
mem_ℓp (-f) p p
theorem mem_ℓp.of_exponent_ge {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p q : ennreal} {f : Π (i : α), E i} (hfq : q) (hpq : q p) :
p
theorem mem_ℓp.add {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f g : Π (i : α), E i} (hf : p) (hg : p) :
mem_ℓp (f + g) p
theorem mem_ℓp.sub {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f g : Π (i : α), E i} (hf : p) (hg : p) :
mem_ℓp (f - g) p
theorem mem_ℓp.finset_sum {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {ι : Type u_3} (s : finset ι) {f : ι Π (i : α), E i} (hf : (i : ι), i s mem_ℓp (f i) p) :
mem_ℓp (λ (a : α), s.sum (λ (i : ι), f i a)) p
theorem mem_ℓp.const_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] {f : Π (i : α), E i} (hf : p) (c : 𝕜) :
mem_ℓp (c f) p
theorem mem_ℓp.const_mul {α : Type u_1} {p : ennreal} {𝕜 : Type u_3} [normed_field 𝕜] {f : α 𝕜} (hf : p) (c : 𝕜) :
mem_ℓp (λ (x : α), c * f x) p

lp space #

The space of elements of `Π i, E i` satisfying the predicate `mem_ℓp`.

@[protected, instance]
def pre_lp.add_comm_group {α : Type u_1} (E : α Type u_2) [Π (i : α), ] :
@[nolint]
def pre_lp {α : Type u_1} (E : α Type u_2) [Π (i : α), ] :
Type (max u_1 u_2)

We define `pre_lp E` to be a type synonym for `Π i, E i` which, importantly, does not inherit the `pi` topology on `Π i, E i` (otherwise this topology would descend to `lp E p` and conflict with the normed group topology we will later equip it with.)

We choose to deal with this issue by making a type synonym for `Π i, E i` rather than for the `lp` subgroup itself, because this allows all the spaces `lp E p` (for varying `p`) to be subgroups of the same ambient group, which permits lemma statements like `lp.monotone` (below).

Equations
• = Π (i : α), E i
Instances for `pre_lp`
@[protected, instance]
def pre_lp.unique {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [is_empty α] :
Equations
def lp {α : Type u_1} (E : α Type u_2) [Π (i : α), ] (p : ennreal) :

lp space

Equations
Instances for `↥lp`
@[protected, instance]
def lp.pi.has_coe {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] :
has_coe (lp E p) (Π (i : α), E i)
Equations
@[protected, instance]
def lp.has_coe_to_fun {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] :
has_coe_to_fun (lp E p) (λ (_x : (lp E p)), Π (i : α), E i)
Equations
@[ext]
theorem lp.ext {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f g : (lp E p)} (h : f = g) :
f = g
@[protected]
theorem lp.ext_iff {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f g : (lp E p)} :
f = g f = g
theorem lp.eq_zero' {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [is_empty α] (f : (lp E p)) :
f = 0
@[protected]
theorem lp.monotone {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p q : ennreal} (hpq : q p) :
lp E q lp E p
@[protected]
theorem lp.mem_ℓp {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (f : (lp E p)) :
p
@[simp]
theorem lp.coe_fn_zero {α : Type u_1} (E : α Type u_2) (p : ennreal) [Π (i : α), ] :
0 = 0
@[simp]
theorem lp.coe_fn_neg {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (f : (lp E p)) :
@[simp]
theorem lp.coe_fn_add {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (f g : (lp E p)) :
(f + g) = f + g
@[simp]
theorem lp.coe_fn_sum {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {ι : Type u_3} (f : ι (lp E p)) (s : finset ι) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp]
theorem lp.coe_fn_sub {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (f g : (lp E p)) :
(f - g) = f - g
@[protected, instance]
noncomputable def lp.has_norm {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] :
Equations
theorem lp.norm_eq_card_dsupport {α : Type u_1} {E : α Type u_2} [Π (i : α), ] (f : (lp E 0)) :
theorem lp.norm_eq_csupr {α : Type u_1} {E : α Type u_2} [Π (i : α), ] (f : (lp E )) :
f = (i : α), f i
theorem lp.is_lub_norm {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [nonempty α] (f : (lp E )) :
is_lub (set.range (λ (i : α), f i)) f
theorem lp.norm_eq_tsum_rpow {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) (f : (lp E p)) :
f = (∑' (i : α), f i ^ p.to_real) ^ (1 / p.to_real)
theorem lp.norm_rpow_eq_tsum {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) (f : (lp E p)) :
theorem lp.has_sum_norm {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) (f : (lp E p)) :
has_sum (λ (i : α), f i ^ p.to_real) (f ^ p.to_real)
theorem lp.norm_nonneg' {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (f : (lp E p)) :
@[simp]
theorem lp.norm_zero {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] :
theorem lp.norm_eq_zero_iff {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f : (lp E p)} :
f = 0 f = 0
theorem lp.eq_zero_iff_coe_fn_eq_zero {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {f : (lp E p)} :
f = 0 f = 0
@[simp]
theorem lp.norm_neg {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] ⦃f : (lp E p) :
@[protected, instance]
noncomputable def lp.normed_add_comm_group {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [hp : fact (1 p)] :
Equations
@[protected]
theorem lp.tsum_mul_le_mul_norm {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p q : ennreal} (hpq : p.to_real.is_conjugate_exponent q.to_real) (f : (lp E p)) (g : (lp E q)) :
summable (λ (i : α), f i * g i) ∑' (i : α), f i * g i f * g

Hölder inequality

@[protected]
theorem lp.summable_mul {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p q : ennreal} (hpq : p.to_real.is_conjugate_exponent q.to_real) (f : (lp E p)) (g : (lp E q)) :
summable (λ (i : α), f i * g i)
@[protected]
theorem lp.tsum_mul_le_mul_norm' {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {p q : ennreal} (hpq : p.to_real.is_conjugate_exponent q.to_real) (f : (lp E p)) (g : (lp E q)) :
theorem lp.norm_apply_le_norm {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : p 0) (f : (lp E p)) (i : α) :
theorem lp.sum_rpow_le_norm_rpow {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
s.sum (λ (i : α), f i ^ p.to_real) f ^ p.to_real
theorem lp.norm_le_of_forall_le' {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [nonempty α] {f : (lp E )} (C : ) (hCf : (i : α), f i C) :
theorem lp.norm_le_of_forall_le {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {f : (lp E )} {C : } (hC : 0 C) (hCf : (i : α), f i C) :
theorem lp.norm_le_of_tsum_le {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) {C : } (hC : 0 C) {f : (lp E p)} (hf : ∑' (i : α), f i ^ p.to_real C ^ p.to_real) :
theorem lp.norm_le_of_forall_sum_le {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] (hp : 0 < p.to_real) {C : } (hC : 0 C) {f : (lp E p)} (hf : (s : finset α), s.sum (λ (i : α), f i ^ p.to_real) C ^ p.to_real) :
@[protected, instance]
def lp.pre_lp.module {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] :
(pre_lp E)
Equations
theorem lp.mem_lp_const_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] (c : 𝕜) (f : (lp E p)) :
c f lp E p
def lp_submodule {α : Type u_1} (E : α Type u_2) (p : ennreal) [Π (i : α), ] (𝕜 : Type u_3) [normed_field 𝕜] [Π (i : α), (E i)] :
(pre_lp E)

The `𝕜`-submodule of elements of `Π i : α, E i` whose `lp` norm is finite. This is `lp E p`, with extra structure.

Equations
theorem lp.coe_lp_submodule {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] :
p 𝕜).to_add_subgroup = lp E p
@[protected, instance]
def lp.module {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] :
(lp E p)
Equations
@[simp]
theorem lp.coe_fn_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] (c : 𝕜) (f : (lp E p)) :
(c f) = c f
theorem lp.norm_const_smul {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] (hp : p 0) {c : 𝕜} (f : (lp E p)) :
@[protected, instance]
def lp.normed_space {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] [fact (1 p)] :
(lp E p)
Equations
@[protected, instance]
def lp.is_scalar_tower {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] {𝕜' : Type u_4} [normed_field 𝕜'] [Π (i : α), (E i)] [has_smul 𝕜' 𝕜] [ (i : α), 𝕜 (E i)] :
𝕜 (lp E p)
theorem mem_ℓp.star_mem {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] {f : Π (i : α), E i} (hf : p) :
p
@[simp]
theorem mem_ℓp.star_iff {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] {f : Π (i : α), E i} :
p p
@[protected, instance]
def lp.has_star {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] :
Equations
@[simp]
theorem lp.coe_fn_star {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] (f : (lp E p)) :
@[protected, simp]
theorem lp.star_apply {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] (f : (lp E p)) (i : α) :
@[protected, instance]
def lp.has_involutive_star {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] :
Equations
@[protected, instance]
def lp.star_add_monoid {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] :
Equations
@[protected, instance]
def lp.normed_star_group {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] [hp : fact (1 p)] :
@[protected, instance]
def lp.star_module {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [Π (i : α), star_add_monoid (E i)] [ (i : α), normed_star_group (E i)] {𝕜 : Type u_3} [has_star 𝕜] [normed_field 𝕜] [Π (i : α), (E i)] [ (i : α), (E i)] :
(lp E p)
theorem mem_ℓp.infty_mul {I : Type u_3} {B : I Type u_4} [Π (i : I), ] {f g : Π (i : I), B i} (hf : ) (hg : ) :
mem_ℓp (f * g)
@[protected, instance]
noncomputable def lp.has_mul {I : Type u_3} {B : I Type u_4} [Π (i : I), ] :
Equations
@[simp]
theorem lp.infty_coe_fn_mul {I : Type u_3} {B : I Type u_4} [Π (i : I), ] (f g : (lp B )) :
(f * g) = f * g
@[protected, instance]
noncomputable def lp.non_unital_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), ] :
Equations
• lp.non_unital_ring = lp.non_unital_ring._proof_1 lp.non_unital_ring._proof_2 lp.non_unital_ring._proof_3 lp.non_unital_ring._proof_4 lp.non_unital_ring._proof_5 lp.non_unital_ring._proof_6 lp.non_unital_ring._proof_7 lp.non_unital_ring._proof_8
@[protected, instance]
noncomputable def lp.non_unital_normed_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), ] :
Equations
@[protected, instance]
def lp.infty_is_scalar_tower {I : Type u_3} {B : I Type u_4} [Π (i : I), ] {𝕜 : Type u_1} [normed_field 𝕜] [Π (i : I), (B i)] [ (i : I), (B i) (B i)] :
(lp B ) (lp B )
@[protected, instance]
def lp.infty_smul_comm_class {I : Type u_3} {B : I Type u_4} [Π (i : I), ] {𝕜 : Type u_1} [normed_field 𝕜] [Π (i : I), (B i)] [ (i : I), (B i) (B i)] :
(lp B ) (lp B )
@[protected, instance]
noncomputable def lp.infty_star_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), ] [Π (i : I), star_ring (B i)] [ (i : I), normed_star_group (B i)] :
Equations
@[protected, instance]
def lp.infty_cstar_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), ] [Π (i : I), star_ring (B i)] [ (i : I), normed_star_group (B i)] [ (i : I), cstar_ring (B i)] :
@[protected, instance]
def pre_lp.ring {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] :
Equations
theorem one_mem_ℓp_infty {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] :
def lp_infty_subring {I : Type u_3} (B : I Type u_4) [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] :

The `𝕜`-subring of elements of `Π i : α, B i` whose `lp` norm is finite. This is `lp E ∞`, with extra structure.

Equations
@[protected, instance]
def lp.infty_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] :
Equations
theorem mem_ℓp.infty_pow {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] {f : Π (i : I), B i} (hf : ) (n : ) :
mem_ℓp (f ^ n)
theorem nat_cast_mem_ℓp_infty {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] (n : ) :
theorem int_cast_mem_ℓp_infty {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] (z : ) :
@[simp]
theorem lp.infty_coe_fn_one {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] :
1 = 1
@[simp]
theorem lp.infty_coe_fn_pow {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] (f : (lp B )) (n : ) :
(f ^ n) = f ^ n
@[simp]
theorem lp.infty_coe_fn_nat_cast {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] (n : ) :
@[simp]
theorem lp.infty_coe_fn_int_cast {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] (z : ) :
@[protected, instance]
def lp.norm_one_class {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] [nonempty I] :
@[protected, instance]
noncomputable def lp.infty_normed_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_ring (B i)] [ (i : I), norm_one_class (B i)] :
Equations
@[protected, instance]
def lp.infty_comm_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_comm_ring (B i)] [ (i : I), norm_one_class (B i)] :
Equations
@[protected, instance]
noncomputable def lp.infty_normed_comm_ring {I : Type u_3} {B : I Type u_4} [Π (i : I), normed_comm_ring (B i)] [ (i : I), norm_one_class (B i)] :
Equations
@[protected, instance]
def pi.algebra_of_normed_algebra {I : Type u_3} {𝕜 : Type u_4} {B : I Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] :
(Π (i : I), B i)

A variant of `pi.algebra` that lean can't find otherwise.

Equations
@[protected, instance]
def pre_lp.algebra {I : Type u_3} {𝕜 : Type u_4} {B : I Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] :
(pre_lp B)
Equations
theorem algebra_map_mem_ℓp_infty {I : Type u_3} {𝕜 : Type u_4} {B : I Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] [ (i : I), norm_one_class (B i)] (k : 𝕜) :
mem_ℓp ( (Π (i : I), B i)) k)
def lp_infty_subalgebra {I : Type u_3} (𝕜 : Type u_4) (B : I Type u_5) [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] [ (i : I), norm_one_class (B i)] :
(pre_lp B)

The `𝕜`-subalgebra of elements of `Π i : α, B i` whose `lp` norm is finite. This is `lp E ∞`, with extra structure.

Equations
@[protected, instance]
def lp.infty_normed_algebra {I : Type u_3} {𝕜 : Type u_4} {B : I Type u_5} [normed_field 𝕜] [Π (i : I), normed_ring (B i)] [Π (i : I), (B i)] [ (i : I), norm_one_class (B i)] :
(lp B )
Equations
@[protected]
def lp.single {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) :
(lp E p)

The element of `lp E p` which is `a : E i` at the index `i`, and zero elsewhere.

Equations
• i a = λ (j : α), dite (j = i) (λ (h : j = i), eq.rec a _) (λ (h : ¬j = i), 0), _⟩
@[protected]
theorem lp.single_apply {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) (j : α) :
i a) j = dite (j = i) (λ (h : j = i), eq.rec a _) (λ (h : ¬j = i), 0)
@[protected]
theorem lp.single_apply_self {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) :
i a) i = a
@[protected]
theorem lp.single_apply_ne {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) {j : α} (hij : j i) :
i a) j = 0
@[protected, simp]
theorem lp.single_neg {α : Type u_1} {E : α Type u_2} [Π (i : α), ] [decidable_eq α] (p : ennreal) (i : α) (a : E i) :
i (-a) = - i a
@[protected, simp]
theorem lp.single_smul {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {𝕜 : Type u_3} [normed_field 𝕜] [Π (i : α), (E i)] [decidable_eq α] (p : ennreal) (i : α) (a : E i) (c : 𝕜) :
i (c a) = c i a
@[protected]
theorem lp.norm_sum_single {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : Π (i : α), E i) (s : finset α) :
s.sum (λ (i : α), i (f i)) ^ p.to_real = s.sum (λ (i : α), f i ^ p.to_real)
@[protected]
theorem lp.norm_single {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : Π (i : α), E i) (i : α) :
i (f i) = f i
@[protected]
theorem lp.norm_sub_norm_compl_sub_single {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
f ^ p.to_real - f - s.sum (λ (i : α), i (f i)) ^ p.to_real = s.sum (λ (i : α), f i ^ p.to_real)
@[protected]
theorem lp.norm_compl_sum_single {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [decidable_eq α] (hp : 0 < p.to_real) (f : (lp E p)) (s : finset α) :
f - s.sum (λ (i : α), i (f i)) ^ p.to_real = f ^ p.to_real - s.sum (λ (i : α), f i ^ p.to_real)
@[protected]
theorem lp.has_sum_single {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [decidable_eq α] [fact (1 p)] (hp : p ) (f : (lp E p)) :
has_sum (λ (i : α), i (f i)) f

The canonical finitely-supported approximations to an element `f` of `lp` converge to it, in the `lp` topology.

theorem lp.uniform_continuous_coe {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [fact (1 p)] :

The coercion from `lp E p` to `Π i, E i` is uniformly continuous.

theorem lp.norm_apply_le_of_tendsto {α : Type u_1} {E : α Type u_2} [Π (i : α), ] {ι : Type u_3} {l : filter ι} [l.ne_bot] {C : } {F : ι (lp E )} (hCF : ∀ᶠ (k : ι) in l, F k C) {f : Π (a : α), E a} (hf : filter.tendsto (id (λ (i : ι), (F i))) l (nhds f)) (a : α) :
f a C
theorem lp.sum_rpow_le_of_tendsto {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {ι : Type u_3} {l : filter ι} [l.ne_bot] [fact (1 p)] (hp : p ) {C : } {F : ι (lp E p)} (hCF : ∀ᶠ (k : ι) in l, F k C) {f : Π (a : α), E a} (hf : filter.tendsto (id (λ (i : ι), (F i))) l (nhds f)) (s : finset α) :
s.sum (λ (i : α), f i ^ p.to_real) C ^ p.to_real
theorem lp.norm_le_of_tendsto {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {ι : Type u_3} {l : filter ι} [l.ne_bot] [fact (1 p)] {C : } {F : ι (lp E p)} (hCF : ∀ᶠ (k : ι) in l, F k C) {f : (lp E p)} (hf : filter.tendsto (id (λ (i : ι), (F i))) l (nhds f)) :

"Semicontinuity of the `lp` norm": If all sufficiently large elements of a sequence in `lp E p` have `lp` norm `≤ C`, then the pointwise limit, if it exists, also has `lp` norm `≤ C`.

theorem lp.mem_ℓp_of_tendsto {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] {ι : Type u_3} {l : filter ι} [l.ne_bot] [fact (1 p)] {F : ι (lp E p)} (hF : metric.bounded (set.range F)) {f : Π (a : α), E a} (hf : filter.tendsto (id (λ (i : ι), (F i))) l (nhds f)) :
p

If `f` is the pointwise limit of a bounded sequence in `lp E p`, then `f` is in `lp E p`.

theorem lp.tendsto_lp_of_tendsto_pi {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [fact (1 p)] {F : (lp E p)} (hF : cauchy_seq F) {f : (lp E p)} (hf : filter.tendsto (id (λ (i : ), (F i))) filter.at_top (nhds f)) :

If a sequence is Cauchy in the `lp E p` topology and pointwise convergent to a element `f` of `lp E p`, then it converges to `f` in the `lp E p` topology.

@[protected, instance]
def lp.complete_space {α : Type u_1} {E : α Type u_2} {p : ennreal} [Π (i : α), ] [fact (1 p)] [ (a : α), complete_space (E a)] :