L^p distance on finite products of metric spaces

Given finitely many metric spaces, one can put the max distance on their product, but there is also a whole family of natural distances, indexed by a parameter p : ℝ≥0∞, that also induce the product topology. We define them in this file. For 0 < p < ∞, the distance on Π i, α i is given by $$ d(x, y) = \left(\sum d(x_i, y_i)^p\right)^{1/p}. $$, whereas for p = 0 it is the cardinality of the set ${i | d (x_i, y_i) ≠ 0}$. For p = ∞ the distance is the supremum of the distances.

We give instances of this construction for emetric spaces, metric spaces, normed groups and normed spaces.

To avoid conflicting instances, all these are defined on a copy of the original Π-type, named PiLp p α. The assumption [Fact (1 ≤ p)] is required for the metric and normed space instances.

We ensure that the topology, bornology and uniform structure on PiLp p α are (defeq to) the product topology, product bornology and product uniformity, to be able to use freely continuity statements for the coordinate functions, for instance.

Implementation notes

We only deal with the L^p distance on a product of finitely many metric spaces, which may be distinct. A closely related construction is lp, the L^p norm on a product of (possibly infinitely many) normed spaces, where the norm is $$ \left(\sum ‖f (x)‖^p \right)^{1/p}. $$ However, the topology induced by this construction is not the product topology, and some functions have infinite L^p norm. These subtleties are not present in the case of finitely many metric spaces, hence it is worth devoting a file to this specific case which is particularly well behaved.

Another related construction is MeasureTheory.Lp, the L^p norm on the space of functions from a measure space to a normed space, where the norm is $$ \left(\int ‖f (x)‖^p dμ\right)^{1/p}. $$ This has all the same subtleties as lp, and the further subtlety that this only defines a seminorm (as almost everywhere zero functions have zero L^p norm). The construction PiLp corresponds to the special case of MeasureTheory.Lp in which the basis is a finite space equipped with the counting measure.

To prove that the topology (and the uniform structure) on a finite product with the L^p distance are the same as those coming from the L^∞ distance, we could argue that the L^p and L^∞ norms are equivalent on ℝ^n for abstract (norm equivalence) reasons. Instead, we give a more explicit (easy) proof which provides a comparison between these two norms with explicit constants.

We also set up the theory for PseudoEMetricSpace and PseudoMetricSpace.

@[reducible, inline]

abbrev PiLp (p : ENNReal) {ι : Type u_1} (α : ι → Type u_2) : Type (max u_1 u_2)

A copy of a Pi type, on which we will put the L^p distance. Since the Pi type itself is already endowed with the L^∞ distance, we need the type synonym to avoid confusing typeclass resolution. Also, we let it depend on p, to get a whole family of type on which we can put different distances.

Equations

• PiLp p α = WithLp p ((i : ι) → α i)

instance instCoeFunPiLpForall (p : ENNReal) {ι : Type u_1} (α : ι → Type u_2) : CoeFun (PiLp p α) fun (x : PiLp p α) => (i : ι) → α i

Equations

• instCoeFunPiLpForall p α = { coe := ⇑(WithLp.equiv p ((i : ι) → α i)) }

instance instInhabitedPiLp (p : ENNReal) {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → Inhabited (α i)] : Inhabited (PiLp p α)

Equations

• instInhabitedPiLp p α = { default := fun (x : ι) => default }

theorem PiLp.ext {p : ENNReal} {ι : Type u_1} {α : ι → Type u_2} {x : PiLp p α} {y : PiLp p α} (h : ∀ (i : ι), x i = y i) : x = y

@[simp]

theorem PiLp.zero_apply {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → SeminormedAddCommGroup (β i)] (i : ι) : 0 i = 0

@[simp]

theorem PiLp.add_apply {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp p β) (y : PiLp p β) (i : ι) : (x + y) i = x i + y i

@[simp]

theorem PiLp.sub_apply {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp p β) (y : PiLp p β) (i : ι) : (x - y) i = x i - y i

@[simp]

theorem PiLp.smul_apply {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} (β : ι → Type u_4) [SeminormedRing 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (β i)] (c : 𝕜) (x : PiLp p β) (i : ι) : (c • x) i = c • x i

@[simp]

theorem PiLp.neg_apply {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp p β) (i : ι) : (-x) i = -x i

Note that the unapplied versions of these lemmas are deliberately omitted, as they break the use of the type synonym.

@[simp]

theorem WithLp.equiv_pi_apply (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) (x : PiLp p α) (i : ι) : (WithLp.equiv p ((i : ι) → α i)) x i = x i

@[simp]

theorem WithLp.equiv_symm_pi_apply (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) (x : (i : ι) → α i) (i : ι) : (WithLp.equiv p ((i : ι) → α i)).symm x i = x i

Definition of edist, dist and norm on PiLp

In this section we define the edist, dist and norm functions on PiLp p α without assuming [Fact (1 ≤ p)] or metric properties of the spaces α i. This allows us to provide the rewrite lemmas for each of three cases p = 0, p = ∞ and 0 < p.to_real.

instance PiLp.instEDist (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fintype ι] [(i : ι) → EDist (β i)] : EDist (PiLp p β)

Endowing the space PiLp p β with the L^p edistance. We register this instance separate from pi_Lp.pseudo_emetric since the latter requires the type class hypothesis [Fact (1 ≤ p)] in order to prove the triangle inequality.

Registering this separately allows for a future emetric-like structure on PiLp p β for p < 1 satisfying a relaxed triangle inequality. The terminology for this varies throughout the literature, but it is sometimes called a quasi-metric or semi-metric.

Equations

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

theorem PiLp.edist_eq_card {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → EDist (β i)] (f : PiLp 0 β) (g : PiLp 0 β) : edist f g = ↑⋯.toFinset.card

theorem PiLp.edist_eq_sum {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → EDist (β i)] {p : ENNReal} (hp : 0 < p.toReal) (f : PiLp p β) (g : PiLp p β) : edist f g = (∑ i : ι, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)

theorem PiLp.edist_eq_iSup {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → EDist (β i)] (f : PiLp ⊤ β) (g : PiLp ⊤ β) : edist f g = ⨆ (i : ι), edist (f i) (g i)

theorem PiLp.edist_self (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → PseudoEMetricSpace (β i)] (f : PiLp p β) : edist f f = 0

This holds independent of p and does not require [Fact (1 ≤ p)]. We keep it separate from pi_Lp.pseudo_emetric_space so it can be used also for p < 1.

theorem PiLp.edist_comm (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → PseudoEMetricSpace (β i)] (f : PiLp p β) (g : PiLp p β) : edist f g = edist g f

This holds independent of p and does not require [Fact (1 ≤ p)]. We keep it separate from pi_Lp.pseudo_emetric_space so it can be used also for p < 1.

instance PiLp.instDist (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [Fintype ι] [(i : ι) → Dist (α i)] : Dist (PiLp p α)

Endowing the space PiLp p β with the L^p distance. We register this instance separate from pi_Lp.pseudo_metric since the latter requires the type class hypothesis [Fact (1 ≤ p)] in order to prove the triangle inequality.

Registering this separately allows for a future metric-like structure on PiLp p β for p < 1 satisfying a relaxed triangle inequality. The terminology for this varies throughout the literature, but it is sometimes called a quasi-metric or semi-metric.

Equations

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

theorem PiLp.dist_eq_card {ι : Type u_2} {α : ι → Type u_3} [Fintype ι] [(i : ι) → Dist (α i)] (f : PiLp 0 α) (g : PiLp 0 α) : dist f g = ↑⋯.toFinset.card

theorem PiLp.dist_eq_sum {ι : Type u_2} {α : ι → Type u_3} [Fintype ι] [(i : ι) → Dist (α i)] {p : ENNReal} (hp : 0 < p.toReal) (f : PiLp p α) (g : PiLp p α) : dist f g = (∑ i : ι, dist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)

theorem PiLp.dist_eq_iSup {ι : Type u_2} {α : ι → Type u_3} [Fintype ι] [(i : ι) → Dist (α i)] (f : PiLp ⊤ α) (g : PiLp ⊤ α) : dist f g = ⨆ (i : ι), dist (f i) (g i)

instance PiLp.instNorm (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fintype ι] [(i : ι) → Norm (β i)] : Norm (PiLp p β)

Endowing the space PiLp p β with the L^p norm. We register this instance separate from PiLp.seminormedAddCommGroup since the latter requires the type class hypothesis [Fact (1 ≤ p)] in order to prove the triangle inequality.

Registering this separately allows for a future norm-like structure on PiLp p β for p < 1 satisfying a relaxed triangle inequality. These are called quasi-norms.

Equations

• PiLp.instNorm p β = { norm := fun (f : PiLp p β) => if p = 0 then ↑⋯.toFinset.card else if p = ⊤ then ⨆ (i : ι), ‖f i‖ else (∑ i : ι, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal) }

theorem PiLp.norm_eq_card {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → Norm (β i)] (f : PiLp 0 β) : ‖f‖ = ↑⋯.toFinset.card

theorem PiLp.norm_eq_ciSup {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → Norm (β i)] (f : PiLp ⊤ β) : ‖f‖ = ⨆ (i : ι), ‖f i‖

theorem PiLp.norm_eq_sum {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → Norm (β i)] (hp : 0 < p.toReal) (f : PiLp p β) : ‖f‖ = (∑ i : ι, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)

The uniformity on finite L^p products is the product uniformity

In this section, we put the L^p edistance on PiLp p α, and we check that the uniformity coming from this edistance coincides with the product uniformity, by showing that the canonical map to the Pi type (with the L^∞ distance) is a uniform embedding, as it is both Lipschitz and antiLipschitz.

We only register this emetric space structure as a temporary instance, as the true instance (to be registered later) will have as uniformity exactly the product uniformity, instead of the one coming from the edistance (which is equal to it, but not defeq). See Note [forgetful inheritance] explaining why having definitionally the right uniformity is often important.

def PiLp.pseudoEmetricAux (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [(i : ι) → PseudoEMetricSpace (β i)] [Fintype ι] : PseudoEMetricSpace (PiLp p β)

Endowing the space PiLp p β with the L^p pseudoemetric structure. This definition is not satisfactory, as it does not register the fact that the topology and the uniform structure coincide with the product one. Therefore, we do not register it as an instance. Using this as a temporary pseudoemetric space instance, we will show that the uniform structure is equal (but not defeq) to the product one, and then register an instance in which we replace the uniform structure by the product one using this pseudoemetric space and PseudoEMetricSpace.replaceUniformity.

Equations

• PiLp.pseudoEmetricAux p β = PseudoEMetricSpace.mk ⋯ ⋯ ⋯ (uniformSpaceOfEDist edist ⋯ ⋯ ⋯) ⋯

theorem PiLp.iSup_edist_ne_top_aux {ι : Type u_5} [Finite ι] {α : ι → Type u_6} [(i : ι) → PseudoMetricSpace (α i)] (f : PiLp ⊤ α) (g : PiLp ⊤ α) : ⨆ (i : ι), edist (f i) (g i) ≠ ⊤

An auxiliary lemma used twice in the proof of PiLp.pseudoMetricAux below. Not intended for use outside this file.

@[reducible, inline]

abbrev PiLp.pseudoMetricAux (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [Fact (1 ≤ p)] [(i : ι) → PseudoMetricSpace (α i)] [Fintype ι] : PseudoMetricSpace (PiLp p α)

Endowing the space PiLp p α with the L^p pseudometric structure. This definition is not satisfactory, as it does not register the fact that the topology, the uniform structure, and the bornology coincide with the product ones. Therefore, we do not register it as an instance. Using this as a temporary pseudoemetric space instance, we will show that the uniform structure is equal (but not defeq) to the product one, and then register an instance in which we replace the uniform structure and the bornology by the product ones using this pseudometric space, PseudoMetricSpace.replaceUniformity, and PseudoMetricSpace.replaceBornology.

See note [reducible non-instances]

Equations

• PiLp.pseudoMetricAux p α = PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯

theorem PiLp.lipschitzWith_equiv_aux (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [(i : ι) → PseudoEMetricSpace (β i)] [Fintype ι] : LipschitzWith 1 ⇑(WithLp.equiv p ((i : ι) → β i))

theorem PiLp.antilipschitzWith_equiv_aux (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [(i : ι) → PseudoEMetricSpace (β i)] [Fintype ι] : AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) ⇑(WithLp.equiv p ((i : ι) → β i))

theorem PiLp.aux_uniformity_eq (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [(i : ι) → PseudoEMetricSpace (β i)] [Fintype ι] : uniformity (PiLp p β) = uniformity ((i : ι) → β i)

theorem PiLp.aux_cobounded_eq (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [Fact (1 ≤ p)] [(i : ι) → PseudoMetricSpace (α i)] [Fintype ι] : Bornology.cobounded (PiLp p α) = Bornology.cobounded ((i : ι) → α i)

Instances on finite L^p products

instance PiLp.uniformSpace (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → UniformSpace (β i)] : UniformSpace (PiLp p β)

Equations

• PiLp.uniformSpace p β = Pi.uniformSpace β

theorem PiLp.uniformContinuous_equiv (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → UniformSpace (β i)] : UniformContinuous ⇑(WithLp.equiv p ((i : ι) → β i))

theorem PiLp.uniformContinuous_equiv_symm (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → UniformSpace (β i)] : UniformContinuous ⇑(WithLp.equiv p ((i : ι) → β i)).symm

theorem PiLp.continuous_equiv (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → UniformSpace (β i)] : Continuous ⇑(WithLp.equiv p ((i : ι) → β i))

theorem PiLp.continuous_equiv_symm (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → UniformSpace (β i)] : Continuous ⇑(WithLp.equiv p ((i : ι) → β i)).symm

instance PiLp.bornology (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [(i : ι) → Bornology (β i)] : Bornology (PiLp p β)

Equations

• PiLp.bornology p β = Pi.instBornology

instance PiLp.instPseudoEMetricSpace (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → PseudoEMetricSpace (β i)] : PseudoEMetricSpace (PiLp p β)

pseudoemetric space instance on the product of finitely many pseudoemetric spaces, using the L^p pseudoedistance, and having as uniformity the product uniformity.

Equations

• PiLp.instPseudoEMetricSpace p β = (PiLp.pseudoEmetricAux p β).replaceUniformity ⋯

instance PiLp.instEMetricSpace (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → EMetricSpace (α i)] : EMetricSpace (PiLp p α)

emetric space instance on the product of finitely many emetric spaces, using the L^p edistance, and having as uniformity the product uniformity.

Equations

• PiLp.instEMetricSpace p α = EMetricSpace.ofT0PseudoEMetricSpace (PiLp p α)

instance PiLp.instPseudoMetricSpace (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → PseudoMetricSpace (β i)] : PseudoMetricSpace (PiLp p β)

pseudometric space instance on the product of finitely many pseudometric spaces, using the L^p distance, and having as uniformity the product uniformity.

Equations

• PiLp.instPseudoMetricSpace p β = ((PiLp.pseudoMetricAux p β).replaceUniformity ⋯).replaceBornology ⋯

instance PiLp.instMetricSpace (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → MetricSpace (α i)] : MetricSpace (PiLp p α)

metric space instance on the product of finitely many metric spaces, using the L^p distance, and having as uniformity the product uniformity.

Equations

• PiLp.instMetricSpace p α = MetricSpace.ofT0PseudoMetricSpace (PiLp p α)

theorem PiLp.nndist_eq_sum {ι : Type u_2} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {β : ι → Type u_5} [(i : ι) → PseudoMetricSpace (β i)] (hp : p ≠ ⊤) (x : PiLp p β) (y : PiLp p β) : nndist x y = (∑ i : ι, nndist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)

theorem PiLp.nndist_eq_iSup {ι : Type u_2} [Fintype ι] {β : ι → Type u_5} [(i : ι) → PseudoMetricSpace (β i)] (x : PiLp ⊤ β) (y : PiLp ⊤ β) : nndist x y = ⨆ (i : ι), nndist (x i) (y i)

theorem PiLp.lipschitzWith_equiv (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → PseudoEMetricSpace (β i)] : LipschitzWith 1 ⇑(WithLp.equiv p ((i : ι) → β i))

theorem PiLp.antilipschitzWith_equiv (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → PseudoEMetricSpace (β i)] : AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) ⇑(WithLp.equiv p ((i : ι) → β i))

theorem PiLp.infty_equiv_isometry {ι : Type u_2} (β : ι → Type u_4) [Fintype ι] [(i : ι) → PseudoEMetricSpace (β i)] : Isometry ⇑(WithLp.equiv ⊤ ((i : ι) → β i))

instance PiLp.seminormedAddCommGroup (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] : SeminormedAddCommGroup (PiLp p β)

seminormed group instance on the product of finitely many normed groups, using the L^p norm.

Equations

• PiLp.seminormedAddCommGroup p β = let __src := Pi.addCommGroup; SeminormedAddCommGroup.mk ⋯

instance PiLp.normedAddCommGroup (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → NormedAddCommGroup (α i)] : NormedAddCommGroup (PiLp p α)

normed group instance on the product of finitely many normed groups, using the L^p norm.

Equations

• PiLp.normedAddCommGroup p α = let __src := PiLp.seminormedAddCommGroup p α; NormedAddCommGroup.mk ⋯

theorem PiLp.nnnorm_eq_sum {ι : Type u_2} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {β : ι → Type u_5} (hp : p ≠ ⊤) [(i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp p β) : ‖f‖₊ = (∑ i : ι, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal)

theorem PiLp.nnnorm_eq_ciSup {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp ⊤ β) : ‖f‖₊ = ⨆ (i : ι), ‖f i‖₊

@[simp]

theorem PiLp.nnnorm_equiv {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp ⊤ β) : ‖(WithLp.equiv ⊤ ((i : ι) → β i)) f‖₊ = ‖f‖₊

@[simp]

theorem PiLp.nnnorm_equiv_symm {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] (f : (i : ι) → β i) : ‖(WithLp.equiv ⊤ ((i : ι) → β i)).symm f‖₊ = ‖f‖₊

@[simp]

theorem PiLp.norm_equiv {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp ⊤ β) : ‖(WithLp.equiv ⊤ ((i : ι) → β i)) f‖ = ‖f‖

@[simp]

theorem PiLp.norm_equiv_symm {ι : Type u_2} {β : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] (f : (i : ι) → β i) : ‖(WithLp.equiv ⊤ ((i : ι) → β i)).symm f‖ = ‖f‖

theorem PiLp.norm_eq_of_nat {ι : Type u_2} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {β : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (β i)] (n : ℕ) (h : p = ↑n) (f : PiLp p β) : ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)

theorem PiLp.norm_eq_of_L2 {ι : Type u_2} [Fintype ι] {β : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β) : ‖x‖ = √(∑ i : ι, ‖x i‖ ^ 2)

theorem PiLp.nnnorm_eq_of_L2 {ι : Type u_2} [Fintype ι] {β : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β) : ‖x‖₊ = NNReal.sqrt (∑ i : ι, ‖x i‖₊ ^ 2)

theorem PiLp.norm_sq_eq_of_L2 {ι : Type u_2} [Fintype ι] (β : ι → Type u_5) [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β) : ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2

theorem PiLp.dist_eq_of_L2 {ι : Type u_2} [Fintype ι] {β : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β) (y : PiLp 2 β) : dist x y = √(∑ i : ι, dist (x i) (y i) ^ 2)

theorem PiLp.nndist_eq_of_L2 {ι : Type u_2} [Fintype ι] {β : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β) (y : PiLp 2 β) : nndist x y = NNReal.sqrt (∑ i : ι, nndist (x i) (y i) ^ 2)

theorem PiLp.edist_eq_of_L2 {ι : Type u_2} [Fintype ι] {β : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β) (y : PiLp 2 β) : edist x y = (∑ i : ι, edist (x i) (y i) ^ 2) ^ (1 / 2)

instance PiLp.instBoundedSMul (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [SeminormedRing 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (β i)] [∀ (i : ι), BoundedSMul 𝕜 (β i)] : BoundedSMul 𝕜 (PiLp p β)

Equations

• ⋯ = ⋯

instance PiLp.normedSpace (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [NormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → NormedSpace 𝕜 (β i)] : NormedSpace 𝕜 (PiLp p β)

The product of finitely many normed spaces is a normed space, with the L^p norm.

Equations

• PiLp.normedSpace p 𝕜 β = NormedSpace.mk ⋯

def PiLp.equivₗᵢ {𝕜 : Type u_1} {ι : Type u_2} (β : ι → Type u_4) [Fintype ι] [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (β i)] : PiLp ⊤ β ≃ₗᵢ[𝕜] (i : ι) → β i

The canonical map WithLp.equiv between PiLp ∞ β and Π i, β i as a linear isometric equivalence.

Equations

• PiLp.equivₗᵢ β = let __src := WithLp.equiv ⊤ ((i : ι) → β i); { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

def LinearIsometryEquiv.piLpCongrLeft (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] {ι' : Type u_5} [Fintype ι'] (E : Type u_6) [SeminormedAddCommGroup E] [Module 𝕜 E] (e : ι ≃ ι') : (PiLp p fun (x : ι) => E) ≃ₗᵢ[𝕜] PiLp p fun (x : ι') => E

An equivalence of finite domains induces a linearly isometric equivalence of finitely supported functions

Equations

• LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e = { toLinearEquiv := LinearEquiv.piCongrLeft' 𝕜 (fun (x : ι) => E) e, norm_map' := ⋯ }

@[simp]

theorem LinearIsometryEquiv.piLpCongrLeft_apply {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] {ι' : Type u_5} [Fintype ι'] {E : Type u_6} [SeminormedAddCommGroup E] [Module 𝕜 E] (e : ι ≃ ι') (v : PiLp p fun (x : ι) => E) : (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) v = (Equiv.piCongrLeft' (fun (x : ι) => E) e) v

@[simp]

theorem LinearIsometryEquiv.piLpCongrLeft_symm {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] {ι' : Type u_5} [Fintype ι'] {E : Type u_6} [SeminormedAddCommGroup E] [Module 𝕜 E] (e : ι ≃ ι') : (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e).symm = LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm

@[simp]

theorem LinearIsometryEquiv.piLpCongrLeft_single {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] {ι' : Type u_5} [Fintype ι'] {E : Type u_6} [SeminormedAddCommGroup E] [Module 𝕜 E] [DecidableEq ι] [DecidableEq ι'] (e : ι ≃ ι') (i : ι) (v : E) : (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) ((WithLp.equiv p (ι → E)).symm (Pi.single i v)) = (WithLp.equiv p (ι' → E)).symm (Pi.single (e i) v)

def LinearIsometryEquiv.piLpCongrRight (p : ENNReal) {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (α i)] [(i : ι) → Module 𝕜 (β i)] (e : (i : ι) → α i ≃ₗᵢ[𝕜] β i) : PiLp p α ≃ₗᵢ[𝕜] PiLp p β

A family of linearly isometric equivalences in the codomain induces an isometric equivalence between Pi types with the Lp norm.

This is the isometry version of LinearEquiv.piCongrRight.

Equations

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

@[simp]

theorem LinearIsometryEquiv.piLpCongrRight_apply {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (α i)] [(i : ι) → Module 𝕜 (β i)] (e : (i : ι) → α i ≃ₗᵢ[𝕜] β i) (x : PiLp p α) : (LinearIsometryEquiv.piLpCongrRight p e) x = (WithLp.equiv p ((i : ι) → β i)).symm fun (i : ι) => (e i) (x i)

@[simp]

theorem LinearIsometryEquiv.piLpCongrRight_refl {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → Module 𝕜 (α i)] : (LinearIsometryEquiv.piLpCongrRight p fun (i : ι) => LinearIsometryEquiv.refl 𝕜 (α i)) = LinearIsometryEquiv.refl 𝕜 (PiLp p α)

@[simp]

theorem LinearIsometryEquiv.piLpCongrRight_symm {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (α i)] [(i : ι) → Module 𝕜 (β i)] (e : (i : ι) → α i ≃ₗᵢ[𝕜] β i) : (LinearIsometryEquiv.piLpCongrRight p e).symm = LinearIsometryEquiv.piLpCongrRight p fun (i : ι) => (e i).symm

@[simp]

theorem LinearIsometryEquiv.piLpCongrRight_single {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} [Fact (1 ≤ p)] [Fintype ι] [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (α i)] [(i : ι) → Module 𝕜 (β i)] (e : (i : ι) → α i ≃ₗᵢ[𝕜] β i) [DecidableEq ι] (i : ι) (v : α i) : (LinearIsometryEquiv.piLpCongrRight p e) ((WithLp.equiv p ((i : ι) → α i)).symm (Pi.single i v)) = (WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i ((e i) v))

def LinearIsometryEquiv.piLpCurry (𝕜 : Type u_1) [Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7) [(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [(i : ι) → (k : κ i) → Module 𝕜 (α i k)] : (PiLp p fun (i : Sigma κ) => α i.fst i.snd) ≃ₗᵢ[𝕜] PiLp p fun (i : ι) => PiLp p (α i)

LinearEquiv.piCurry for PiLp, as an isometry.

Equations

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

@[simp]

theorem LinearIsometryEquiv.piLpCurry_apply {𝕜 : Type u_1} [Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7) [(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [(i : ι) → (k : κ i) → Module 𝕜 (α i k)] (f : PiLp p fun (i : Sigma κ) => α i.fst i.snd) : (LinearIsometryEquiv.piLpCurry 𝕜 p α) f = (WithLp.equiv p ((i : ι) → WithLp p ((y : κ i) → α i y))).symm fun (i : ι) => (WithLp.equiv p ((y : κ i) → α i y)).symm (Sigma.curry ((WithLp.equiv p ((x : Sigma κ) → α x.fst x.snd)) f) i)

@[simp]

theorem LinearIsometryEquiv.piLpCurry_symm_apply {𝕜 : Type u_1} [Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7) [(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [(i : ι) → (k : κ i) → Module 𝕜 (α i k)] (f : PiLp p fun (i : ι) => PiLp p (α i)) : (LinearIsometryEquiv.piLpCurry 𝕜 p α).symm f = (WithLp.equiv p ((x : Sigma κ) → α x.fst x.snd)).symm (Sigma.uncurry fun (i : ι) (j : κ i) => f i j)

@[simp]

theorem PiLp.nnnorm_equiv_symm_single (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] [DecidableEq ι] [hp : Fact (1 ≤ p)] (i : ι) (b : β i) : ‖(WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

@[simp]

theorem PiLp.norm_equiv_symm_single (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] [DecidableEq ι] (i : ι) (b : β i) : ‖(WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b)‖ = ‖b‖

@[simp]

theorem PiLp.nndist_equiv_symm_single_same (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] [DecidableEq ι] (i : ι) (b₁ : β i) (b₂ : β i) : nndist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = nndist b₁ b₂

@[simp]

theorem PiLp.dist_equiv_symm_single_same (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] [DecidableEq ι] (i : ι) (b₁ : β i) (b₂ : β i) : dist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = dist b₁ b₂

@[simp]

theorem PiLp.edist_equiv_symm_single_same (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (β i)] [DecidableEq ι] (i : ι) (b₁ : β i) (b₂ : β i) : edist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = edist b₁ b₂

theorem PiLp.nnnorm_equiv_symm_const {p : ENNReal} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] {β : Type u_5} [SeminormedAddCommGroup β] (hp : p ≠ ⊤) (b : β) : ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

When p = ∞, this lemma does not hold without the additional assumption Nonempty ι because the left-hand side simplifies to 0, while the right-hand side simplifies to ‖b‖₊. See PiLp.nnnorm_equiv_symm_const' for a version which exchanges the hypothesis p ≠ ∞ for Nonempty ι.

theorem PiLp.nnnorm_equiv_symm_const' {p : ENNReal} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] {β : Type u_5} [SeminormedAddCommGroup β] [Nonempty ι] (b : β) : ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

When IsEmpty ι, this lemma does not hold without the additional assumption p ≠ ∞ because the left-hand side simplifies to 0, while the right-hand side simplifies to ‖b‖₊. See PiLp.nnnorm_equiv_symm_const for a version which exchanges the hypothesis Nonempty ι. for p ≠ ∞.

theorem PiLp.norm_equiv_symm_const {p : ENNReal} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] {β : Type u_5} [SeminormedAddCommGroup β] (hp : p ≠ ⊤) (b : β) : ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖

When p = ∞, this lemma does not hold without the additional assumption Nonempty ι because the left-hand side simplifies to 0, while the right-hand side simplifies to ‖b‖₊. See PiLp.norm_equiv_symm_const' for a version which exchanges the hypothesis p ≠ ∞ for Nonempty ι.

theorem PiLp.norm_equiv_symm_const' {p : ENNReal} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] {β : Type u_5} [SeminormedAddCommGroup β] [Nonempty ι] (b : β) : ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖

When IsEmpty ι, this lemma does not hold without the additional assumption p ≠ ∞ because the left-hand side simplifies to 0, while the right-hand side simplifies to ‖b‖₊. See PiLp.norm_equiv_symm_const for a version which exchanges the hypothesis Nonempty ι. for p ≠ ∞.

theorem PiLp.nnnorm_equiv_symm_one {p : ENNReal} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] {β : Type u_5} [SeminormedAddCommGroup β] (hp : p ≠ ⊤) [One β] : ‖(WithLp.equiv p (ι → β)).symm 1‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖1‖₊

theorem PiLp.norm_equiv_symm_one {p : ENNReal} {ι : Type u_2} [Fact (1 ≤ p)] [Fintype ι] {β : Type u_5} [SeminormedAddCommGroup β] (hp : p ≠ ⊤) [One β] : ‖(WithLp.equiv p (ι → β)).symm 1‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖1‖

@[simp]

theorem PiLp.continuousLinearEquiv_symm_apply (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (β i)] : ⇑(PiLp.continuousLinearEquiv p 𝕜 β).symm = ⇑(WithLp.equiv p ((i : ι) → β i)).symm

@[simp]

theorem PiLp.continuousLinearEquiv_apply (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (β i)] : ⇑(PiLp.continuousLinearEquiv p 𝕜 β) = ⇑(WithLp.equiv p ((i : ι) → β i))

def PiLp.continuousLinearEquiv (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [Semiring 𝕜] [(i : ι) → SeminormedAddCommGroup (β i)] [(i : ι) → Module 𝕜 (β i)] : PiLp p β ≃L[𝕜] (i : ι) → β i

WithLp.equiv as a continuous linear equivalence.

Equations

• PiLp.continuousLinearEquiv p 𝕜 β = { toLinearEquiv := WithLp.linearEquiv p 𝕜 ((i : ι) → β i), continuous_toFun := ⋯, continuous_invFun := ⋯ }

def PiLp.basisFun (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] : Basis ι 𝕜 (PiLp p fun (x : ι) => 𝕜)

A version of Pi.basisFun for PiLp.

Equations

• PiLp.basisFun p 𝕜 ι = Basis.ofEquivFun (WithLp.linearEquiv p 𝕜 (ι → 𝕜))

@[simp]

theorem PiLp.basisFun_apply (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] [DecidableEq ι] (i : ι) : (PiLp.basisFun p 𝕜 ι) i = (WithLp.equiv p (ι → 𝕜)).symm (Pi.single i 1)

@[simp]

theorem PiLp.basisFun_repr (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] (x : PiLp p fun (x : ι) => 𝕜) (i : ι) : ((PiLp.basisFun p 𝕜 ι).repr x) i = x i

@[simp]

theorem PiLp.basisFun_equivFun (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] : (PiLp.basisFun p 𝕜 ι).equivFun = WithLp.linearEquiv p 𝕜 (ι → 𝕜)

theorem PiLp.basisFun_eq_pi_basisFun (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] : PiLp.basisFun p 𝕜 ι = (Pi.basisFun 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm

@[simp]

theorem PiLp.basisFun_map (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] : (PiLp.basisFun p 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) = Pi.basisFun 𝕜 ι

theorem PiLp.basis_toMatrix_basisFun_mul (p : ENNReal) {ι : Type u_2} [Fintype ι] {𝕜 : Type u_5} [SeminormedCommRing 𝕜] (b : Basis ι 𝕜 (PiLp p fun (x : ι) => 𝕜)) (A : Matrix ι ι 𝕜) : b.toMatrix ⇑(PiLp.basisFun p 𝕜 ι) * A = Matrix.of fun (i j : ι) => (b.repr ((WithLp.equiv p ((i : ι) → (fun (x : ι) => 𝕜) i)).symm (A.transpose j))) i