Documentation

Mathlib.Analysis.NormedSpace.lpSpace

ℓ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 (fun a ↦ ‖f a‖^p) if 0 < p < ∞, and BddAbove (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 #

Main results #

Implementation #

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

TODO #

Memℓp predicate #

def Memℓp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] (f : (i : α) → E i) (p : ENNReal) :

The property that f : ∀ i : α, E i

  • is finitely supported, if p = 0, or
  • admits an upper bound for Set.range (fun i ↦ ‖f i‖), if p = ∞, or
  • has the series ∑' i, ‖f i‖ ^ p be summable, if 0 < p < ∞.
Equations
Instances For
    theorem memℓp_zero_iff {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} :
    Memℓp f 0 {i : α | f i 0}.Finite
    theorem memℓp_zero {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : {i : α | f i 0}.Finite) :
    theorem memℓp_infty_iff {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} :
    Memℓp f BddAbove (Set.range fun (i : α) => f i)
    theorem memℓp_infty {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : BddAbove (Set.range fun (i : α) => f i)) :
    theorem memℓp_gen_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {f : (i : α) → E i} :
    Memℓp f p Summable fun (i : α) => f i ^ p.toReal
    theorem memℓp_gen {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Summable fun (i : α) => f i ^ p.toReal) :
    theorem memℓp_gen' {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {C : } {f : (i : α) → E i} (hf : ∀ (s : Finset α), is, f i ^ p.toReal C) :
    theorem zero_memℓp {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
    theorem zero_mem_ℓp' {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
    Memℓp (fun (i : α) => 0) p
    theorem Memℓp.finite_dsupport {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f 0) :
    {i : α | f i 0}.Finite
    theorem Memℓp.bddAbove {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f ) :
    BddAbove (Set.range fun (i : α) => f i)
    theorem Memℓp.summable {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {f : (i : α) → E i} (hf : Memℓp f p) :
    Summable fun (i : α) => f i ^ p.toReal
    theorem Memℓp.neg {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f p) :
    Memℓp (-f) p
    @[simp]
    theorem Memℓp.neg_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} :
    Memℓp (-f) p Memℓp f p
    theorem Memℓp.of_exponent_ge {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} {f : (i : α) → E i} (hfq : Memℓp f q) (hpq : q p) :
    theorem Memℓp.add {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} {g : (i : α) → E i} (hf : Memℓp f p) (hg : Memℓp g p) :
    Memℓp (f + g) p
    theorem Memℓp.sub {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i} {g : (i : α) → E i} (hf : Memℓp f p) (hg : Memℓp g p) :
    Memℓp (f - g) p
    theorem Memℓp.finset_sum {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} (s : Finset ι) {f : ι(i : α) → E i} (hf : is, Memℓp (f i) p) :
    Memℓp (fun (a : α) => is, f i a) p
    theorem Memℓp.const_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] {f : (i : α) → E i} (hf : Memℓp f p) (c : 𝕜) :
    Memℓp (c f) p
    theorem Memℓp.const_mul {α : Type u_1} {p : ENNReal} {𝕜 : Type u_3} [NormedRing 𝕜] {f : α𝕜} (hf : Memℓp f p) (c : 𝕜) :
    Memℓp (fun (x : α) => c * f x) p

    lp space #

    The space of elements of ∀ i, E i satisfying the predicate Memℓp.

    def PreLp {α : Type u_1} (E : αType u_3) [(i : α) → NormedAddCommGroup (E i)] :
    Type (max u_1 u_3)

    We define PreLp 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
    Instances For
      instance instAddCommGroupPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] :
      Equations
      • instAddCommGroupPreLp = id inferInstance
      instance PreLp.unique {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [IsEmpty α] :
      Equations
      def lp {α : Type u_1} (E : αType u_3) [(i : α) → NormedAddCommGroup (E i)] (p : ENNReal) :

      lp space

      Equations
      • lp E p = { carrier := {f : PreLp E | Memℓp f p}, add_mem' := , zero_mem' := , neg_mem' := }
      Instances For

        lp space

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          lp space

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            instance lp.instCoeOutSubtypePreLpMemAddSubgroupForall {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
            CoeOut ((lp E p)) ((i : α) → E i)
            Equations
            • lp.instCoeOutSubtypePreLpMemAddSubgroupForall = { coe := Subtype.val }
            instance lp.coeFun {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
            CoeFun (lp E p) fun (x : (lp E p)) => (i : α) → E i
            Equations
            • lp.coeFun = { coe := fun (f : (lp E p)) => f }
            theorem lp.ext {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (lp E p)} {g : (lp E p)} (h : f = g) :
            f = g
            theorem lp.ext_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (lp E p)} {g : (lp E p)} :
            f = g f = g
            theorem lp.eq_zero' {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [IsEmpty α] (f : (lp E p)) :
            f = 0
            theorem lp.monotone {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : q p) :
            lp E q lp E p
            theorem lp.memℓp {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) :
            Memℓp (f) p
            @[simp]
            theorem lp.coeFn_zero {α : Type u_1} (E : αType u_2) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] :
            0 = 0
            @[simp]
            theorem lp.coeFn_neg {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) :
            (-f) = -f
            @[simp]
            theorem lp.coeFn_add {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) (g : (lp E p)) :
            (f + g) = f + g
            theorem lp.coeFn_sum {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} (f : ι(lp E p)) (s : Finset ι) :
            (is, f i) = is, (f i)
            @[simp]
            theorem lp.coeFn_sub {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) (g : (lp E p)) :
            (f - g) = f - g
            instance lp.instNormSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
            Norm (lp E p)
            Equations
            • One or more equations did not get rendered due to their size.
            theorem lp.norm_eq_card_dsupport {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E 0)) :
            f = .toFinset.card
            theorem lp.norm_eq_ciSup {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E )) :
            f = ⨆ (i : α), f i
            theorem lp.isLUB_norm {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [Nonempty α] (f : (lp E )) :
            IsLUB (Set.range fun (i : α) => f i) f
            theorem lp.norm_eq_tsum_rpow {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : (lp E p)) :
            f = (∑' (i : α), f i ^ p.toReal) ^ (1 / p.toReal)
            theorem lp.norm_rpow_eq_tsum {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : (lp E p)) :
            f ^ p.toReal = ∑' (i : α), f i ^ p.toReal
            theorem lp.hasSum_norm {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : (lp E p)) :
            HasSum (fun (i : α) => f i ^ p.toReal) (f ^ p.toReal)
            theorem lp.norm_nonneg' {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (f : (lp E p)) :
            @[simp]
            theorem lp.norm_zero {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] :
            theorem lp.norm_eq_zero_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (lp E p)} :
            f = 0 f = 0
            theorem lp.eq_zero_iff_coeFn_eq_zero {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {f : (lp E p)} :
            f = 0 f = 0
            @[simp]
            theorem lp.norm_neg {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] ⦃f : (lp E p) :
            instance lp.normedAddCommGroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [hp : Fact (1 p)] :
            Equations
            • lp.normedAddCommGroup = { toFun := norm, map_zero' := , add_le' := , neg' := , eq_zero_of_map_eq_zero' := }.toNormedAddCommGroup
            theorem lp.tsum_mul_le_mul_norm {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : p.toReal.IsConjExponent q.toReal) (f : (lp E p)) (g : (lp E q)) :
            (Summable fun (i : α) => f i * g i) ∑' (i : α), f i * g i f * g

            Hölder inequality

            theorem lp.summable_mul {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : p.toReal.IsConjExponent q.toReal) (f : (lp E p)) (g : (lp E q)) :
            Summable fun (i : α) => f i * g i
            theorem lp.tsum_mul_le_mul_norm' {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {q : ENNReal} (hpq : p.toReal.IsConjExponent q.toReal) (f : (lp E p)) (g : (lp E q)) :
            ∑' (i : α), f i * g i f * g
            theorem lp.norm_apply_le_norm {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E 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 : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) (f : (lp E p)) (s : Finset α) :
            is, f i ^ p.toReal f ^ p.toReal
            theorem lp.norm_le_of_forall_le' {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E 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 : α) → NormedAddCommGroup (E 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 : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {C : } (hC : 0 C) {f : (lp E p)} (hf : ∑' (i : α), f i ^ p.toReal C ^ p.toReal) :
            theorem lp.norm_le_of_forall_sum_le {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] (hp : 0 < p.toReal) {C : } (hC : 0 C) {f : (lp E p)} (hf : ∀ (s : Finset α), is, f i ^ p.toReal C ^ p.toReal) :
            instance lp.instModulePreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] :
            Module 𝕜 (PreLp E)
            Equations
            instance lp.instSMulCommClassPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)] :
            SMulCommClass 𝕜' 𝕜 (PreLp E)
            Equations
            • =
            instance lp.instIsScalarTowerPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)] :
            IsScalarTower 𝕜' 𝕜 (PreLp E)
            Equations
            • =
            instance lp.instIsCentralScalarPreLp {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜ᵐᵒᵖ (E i)] [∀ (i : α), IsCentralScalar 𝕜 (E i)] :
            Equations
            • =
            theorem lp.mem_lp_const_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (c : 𝕜) (f : (lp E p)) :
            c f lp E p
            def lpSubmodule {α : Type u_1} (E : αType u_2) (p : ENNReal) [(i : α) → NormedAddCommGroup (E i)] (𝕜 : Type u_3) [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :
            Submodule 𝕜 (PreLp E)

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

            Equations
            • lpSubmodule E p 𝕜 = let __src := lp E p; { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := }
            Instances For
              theorem lp.coe_lpSubmodule {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :
              (lpSubmodule E p 𝕜).toAddSubgroup = lp E p
              instance lp.instModuleSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] :
              Module 𝕜 (lp E p)
              Equations
              @[simp]
              theorem lp.coeFn_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (c : 𝕜) (f : (lp E p)) :
              (c f) = c f
              instance lp.instSMulCommClassSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)] :
              SMulCommClass 𝕜' 𝕜 (lp E p)
              Equations
              • =
              instance lp.instIsScalarTowerSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} {𝕜' : Type u_4} [NormedRing 𝕜] [NormedRing 𝕜'] [(i : α) → Module 𝕜 (E i)] [(i : α) → Module 𝕜' (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜' (E i)] [SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)] :
              IsScalarTower 𝕜' 𝕜 (lp E p)
              Equations
              • =
              instance lp.instIsCentralScalarSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [(i : α) → Module 𝕜ᵐᵒᵖ (E i)] [∀ (i : α), IsCentralScalar 𝕜 (E i)] :
              IsCentralScalar 𝕜 (lp E p)
              Equations
              • =
              theorem lp.norm_const_smul_le {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (hp : p 0) (c : 𝕜) (f : (lp E p)) :
              instance lp.instBoundedSMulSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [Fact (1 p)] :
              BoundedSMul 𝕜 (lp E p)
              Equations
              • =
              theorem lp.norm_const_smul {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] (hp : p 0) {c : 𝕜} (f : (lp E p)) :
              instance lp.instNormedSpace {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedField 𝕜] [(i : α) → NormedSpace 𝕜 (E i)] [Fact (1 p)] :
              NormedSpace 𝕜 (lp E p)
              Equations
              theorem Memℓp.star_mem {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i} (hf : Memℓp f p) :
              @[simp]
              theorem Memℓp.star_iff {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i} :
              instance lp.instStarSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] :
              Star (lp E p)
              Equations
              • lp.instStarSubtypePreLpMemAddSubgroup = { star := fun (f : (lp E p)) => star f, }
              @[simp]
              theorem lp.coeFn_star {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] (f : (lp E p)) :
              (star f) = star f
              @[simp]
              theorem lp.star_apply {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] (f : (lp E p)) (i : α) :
              (star f) i = star (f i)
              instance lp.instInvolutiveStar {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] :
              Equations
              instance lp.instStarAddMonoid {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] :
              StarAddMonoid (lp E p)
              Equations
              instance lp.instNormedStarGroupSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] [hp : Fact (1 p)] :
              Equations
              • =
              instance lp.instStarModuleSubtypePreLpMemAddSubgroup {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [(i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {𝕜 : Type u_3} [Star 𝕜] [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [∀ (i : α), StarModule 𝕜 (E i)] :
              StarModule 𝕜 (lp E p)
              Equations
              • =
              theorem Memℓp.infty_mul {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] {f : (i : I) → B i} {g : (i : I) → B i} (hf : Memℓp f ) (hg : Memℓp g ) :
              Memℓp (f * g)
              instance lp.instMulSubtypePreLpMemAddSubgroupTopENNReal {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] :
              Mul (lp B )
              Equations
              • lp.instMulSubtypePreLpMemAddSubgroupTopENNReal = { mul := fun (f g : (lp B )) => (fun (i : I) => f i) * fun (i : I) => g i, }
              @[simp]
              theorem lp.infty_coeFn_mul {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] (f : (lp B )) (g : (lp B )) :
              (f * g) = f * g
              instance lp.nonUnitalRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] :
              Equations
              instance lp.nonUnitalNormedRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] :
              Equations
              • lp.nonUnitalNormedRing = let __src := lp.normedAddCommGroup; let __src_1 := lp.nonUnitalRing; NonUnitalNormedRing.mk
              instance lp.infty_isScalarTower {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_5} [NormedRing 𝕜] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), BoundedSMul 𝕜 (B i)] [∀ (i : I), IsScalarTower 𝕜 (B i) (B i)] :
              IsScalarTower 𝕜 (lp B ) (lp B )
              Equations
              • =
              instance lp.infty_smulCommClass {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_5} [NormedRing 𝕜] [(i : I) → Module 𝕜 (B i)] [∀ (i : I), BoundedSMul 𝕜 (B i)] [∀ (i : I), SMulCommClass 𝕜 (B i) (B i)] :
              SMulCommClass 𝕜 (lp B ) (lp B )
              Equations
              • =
              instance lp.inftyStarRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] :
              StarRing (lp B )
              Equations
              • lp.inftyStarRing = let __src := lp.instStarAddMonoid; StarRing.mk
              instance lp.inftyCstarRing {I : Type u_3} {B : IType u_4} [(i : I) → NonUnitalNormedRing (B i)] [(i : I) → StarRing (B i)] [∀ (i : I), NormedStarGroup (B i)] [∀ (i : I), CstarRing (B i)] :
              Equations
              • =
              instance PreLp.ring {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] :
              Equations
              • PreLp.ring = Pi.ring
              theorem one_memℓp_infty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
              def lpInftySubring {I : Type u_3} (B : IType u_4) [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :

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

              Equations
              Instances For
                instance lp.inftyRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
                Ring (lp B )
                Equations
                theorem Memℓp.infty_pow {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] {f : (i : I) → B i} (hf : Memℓp f ) (n : ) :
                Memℓp (f ^ n)
                theorem natCast_memℓp_infty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ) :
                theorem intCast_memℓp_infty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ) :
                @[simp]
                theorem lp.infty_coeFn_one {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
                1 = 1
                @[simp]
                theorem lp.infty_coeFn_pow {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (f : (lp B )) (n : ) :
                (f ^ n) = f ^ n
                @[simp]
                theorem lp.infty_coeFn_natCast {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (n : ) :
                n = n
                @[simp]
                theorem lp.infty_coeFn_intCast {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] (z : ) :
                z = z
                instance lp.instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] [Nonempty I] :
                Equations
                • =
                instance lp.inftyNormedRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)] :
                Equations
                • lp.inftyNormedRing = let __src := lp.inftyRing; let __src_1 := lp.nonUnitalNormedRing; NormedRing.mk
                instance lp.inftyCommRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedCommRing (B i)] [∀ (i : I), NormOneClass (B i)] :
                CommRing (lp B )
                Equations
                • lp.inftyCommRing = let __src := lp.inftyRing; CommRing.mk
                instance lp.inftyNormedCommRing {I : Type u_3} {B : IType u_4} [(i : I) → NormedCommRing (B i)] [∀ (i : I), NormOneClass (B i)] :
                Equations
                • lp.inftyNormedCommRing = let __src := lp.inftyCommRing; let __src_1 := lp.inftyNormedRing; NormedCommRing.mk
                instance Pi.algebraOfNormedAlgebra {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] :
                Algebra 𝕜 ((i : I) → B i)

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

                Equations
                instance PreLp.algebra {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] :
                Algebra 𝕜 (PreLp B)
                Equations
                • PreLp.algebra = Pi.algebraOfNormedAlgebra
                theorem algebraMap_memℓp_infty {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] (k : 𝕜) :
                Memℓp ((algebraMap 𝕜 ((i : I) → B i)) k)
                def lpInftySubalgebra {I : Type u_3} (𝕜 : Type u_4) (B : IType u_5) [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] :
                Subalgebra 𝕜 (PreLp B)

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

                Equations
                Instances For
                  instance lp.inftyNormedAlgebra {I : Type u_3} {𝕜 : Type u_4} {B : IType u_5} [NormedField 𝕜] [(i : I) → NormedRing (B i)] [(i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] :
                  NormedAlgebra 𝕜 (lp B )
                  Equations
                  def lp.single {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (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
                  • lp.single p i a = fun (j : α) => if h : j = i then a else 0,
                  Instances For
                    theorem lp.single_apply {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) (j : α) :
                    (lp.single p i a) j = if h : j = i then a else 0
                    theorem lp.single_apply_self {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) :
                    (lp.single p i a) i = a
                    theorem lp.single_apply_ne {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) {j : α} (hij : j i) :
                    (lp.single p i a) j = 0
                    @[simp]
                    theorem lp.single_neg {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) :
                    lp.single p i (-a) = -lp.single p i a
                    @[simp]
                    theorem lp.single_smul {α : Type u_1} {E : αType u_2} [(i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3} [NormedRing 𝕜] [(i : α) → Module 𝕜 (E i)] [∀ (i : α), BoundedSMul 𝕜 (E i)] [DecidableEq α] (p : ENNReal) (i : α) (a : E i) (c : 𝕜) :
                    lp.single p i (c a) = c lp.single p i a
                    theorem lp.norm_sum_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p.toReal) (f : (i : α) → E i) (s : Finset α) :
                    is, lp.single p i (f i) ^ p.toReal = is, f i ^ p.toReal
                    theorem lp.norm_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p.toReal) (f : (i : α) → E i) (i : α) :
                    lp.single p i (f i) = f i
                    theorem lp.norm_sub_norm_compl_sub_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p.toReal) (f : (lp E p)) (s : Finset α) :
                    f ^ p.toReal - f - is, lp.single p i (f i) ^ p.toReal = is, f i ^ p.toReal
                    theorem lp.norm_compl_sum_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] (hp : 0 < p.toReal) (f : (lp E p)) (s : Finset α) :
                    f - is, lp.single p i (f i) ^ p.toReal = f ^ p.toReal - is, f i ^ p.toReal
                    theorem lp.hasSum_single {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [DecidableEq α] [Fact (1 p)] (hp : p ) (f : (lp E p)) :
                    HasSum (fun (i : α) => lp.single p i (f i)) f

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

                    theorem lp.uniformContinuous_coe {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 p)] :
                    UniformContinuous Subtype.val

                    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 : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : Filter ι} [l.NeBot] {C : } {F : ι(lp E )} (hCF : ∀ᶠ (k : ι) in l, F k C) {f : (a : α) → E a} (hf : Filter.Tendsto (id fun (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 : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : Filter ι} [l.NeBot] [_i : 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 fun (i : ι) => (F i)) l (nhds f)) (s : Finset α) :
                    is, f i ^ p.toReal C ^ p.toReal
                    theorem lp.norm_le_of_tendsto {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : Filter ι} [l.NeBot] [_i : Fact (1 p)] {C : } {F : ι(lp E p)} (hCF : ∀ᶠ (k : ι) in l, F k C) {f : (lp E p)} (hf : Filter.Tendsto (id fun (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 : α) → NormedAddCommGroup (E i)] {ι : Type u_3} {l : Filter ι} [l.NeBot] [_i : Fact (1 p)] {F : ι(lp E p)} (hF : Bornology.IsBounded (Set.range F)) {f : (a : α) → E a} (hf : Filter.Tendsto (id fun (i : ι) => (F i)) l (nhds f)) :

                    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 : α) → NormedAddCommGroup (E i)] [_i : Fact (1 p)] {F : (lp E p)} (hF : CauchySeq F) {f : (lp E p)} (hf : Filter.Tendsto (id fun (i : ) => (F i)) Filter.atTop (nhds f)) :
                    Filter.Tendsto F Filter.atTop (nhds f)

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

                    instance lp.completeSpace {α : Type u_1} {E : αType u_2} {p : ENNReal} [(i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 p)] [∀ (a : α), CompleteSpace (E a)] :
                    CompleteSpace (lp E p)
                    Equations
                    • =
                    theorem LipschitzWith.uniformly_bounded {α : Type u_1} {ι : Type u_3} [PseudoMetricSpace α] (g : αι) {K : NNReal} (hg : ∀ (i : ι), LipschitzWith K fun (x : α) => g x i) (a₀ : α) (hga₀b : Memℓp (g a₀) ) (a : α) :
                    Memℓp (g a)
                    theorem LipschitzOnWith.coordinate {α : Type u_1} {ι : Type u_3} [PseudoMetricSpace α] (f : α(lp (fun (i : ι) => ) )) (s : Set α) (K : NNReal) :
                    LipschitzOnWith K f s ∀ (i : ι), LipschitzOnWith K (fun (a : α) => (f a) i) s
                    theorem LipschitzWith.coordinate {α : Type u_1} {ι : Type u_3} [PseudoMetricSpace α] {f : α(lp (fun (i : ι) => ) )} (K : NNReal) :
                    LipschitzWith K f ∀ (i : ι), LipschitzWith K fun (a : α) => (f a) i