L^p distance on products of two metric spaces

Given two 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 α × β is given by $$ d(x, y) = \left(d(x_1, y_1)^p + d(x_2, y_2)^p\right)^{1/p}. $$ For p = ∞ the distance is the supremum of the distances and p = 0 the distance is the cardinality of the elements that are not equal.

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 Prod-type, named WithLp 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 WithLp 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.

If you wish to endow a type synonym of α × β with the L^p distance, you can use pseudoMetricSpaceToProd and the declarations below that one.

Implementation notes

This file is a straight-forward adaptation of Mathlib/Analysis/Normed/Lp/PiLp.lean.

TODO

TODO: the results about uniformity and bornology in the Aux section should be using the tools in Mathlib.Topology.MetricSpace.Bilipschitz, so that they can be inlined in the next section and the only remaining results are about Lipschitz and Antilipschitz.

def WithLp.fst {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : WithLp p (α × β)) : α

The projection on the first coordinate in WithLp.

Equations

• x.fst = x.ofLp.1

def WithLp.snd {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : WithLp p (α × β)) : β

The projection on the second coordinate in WithLp.

Equations

• x.snd = x.ofLp.2

@[simp]

theorem WithLp.zero_fst {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] : WithLp.fst 0 = 0

@[simp]

theorem WithLp.zero_snd {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] : WithLp.snd 0 = 0

@[simp]

theorem WithLp.add_fst {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (x y : WithLp p (α × β)) : (x + y).fst = x.fst + y.fst

@[simp]

theorem WithLp.add_snd {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (x y : WithLp p (α × β)) : (x + y).snd = x.snd + y.snd

@[simp]

theorem WithLp.sub_fst {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (x y : WithLp p (α × β)) : (x - y).fst = x.fst - y.fst

@[simp]

theorem WithLp.sub_snd {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (x y : WithLp p (α × β)) : (x - y).snd = x.snd - y.snd

@[simp]

theorem WithLp.neg_fst {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (x : WithLp p (α × β)) : (-x).fst = -x.fst

@[simp]

theorem WithLp.neg_snd {p : ENNReal} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (x : WithLp p (α × β)) : (-x).snd = -x.snd

@[simp]

theorem WithLp.smul_fst {p : ENNReal} {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] (x : WithLp p (α × β)) (c : 𝕜) [Module 𝕜 α] [Module 𝕜 β] : (c • x).fst = c • x.fst

@[simp]

theorem WithLp.smul_snd {p : ENNReal} {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] (x : WithLp p (α × β)) (c : 𝕜) [Module 𝕜 α] [Module 𝕜 β] : (c • x).snd = c • x.snd

def WithLp.fstₗ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] : WithLp p (α × β) →ₗ[𝕜] α

WithLp.fst as a linear map.

Equations

• WithLp.fstₗ p 𝕜 α β = { toFun := WithLp.fst, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem WithLp.fstₗ_apply (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] (x : WithLp p (α × β)) : (fstₗ p 𝕜 α β) x = x.fst

def WithLp.sndₗ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] : WithLp p (α × β) →ₗ[𝕜] β

WithLp.snd as a linear map.

Equations

• WithLp.sndₗ p 𝕜 α β = { toFun := WithLp.snd, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem WithLp.sndₗ_apply (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] (x : WithLp p (α × β)) : (sndₗ p 𝕜 α β) x = x.snd

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

@[simp]

theorem WithLp.toLp_fst {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : α × β) : (toLp p x).fst = x.1

@[simp]

theorem WithLp.toLp_snd {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : α × β) : (toLp p x).snd = x.2

@[simp]

theorem WithLp.ofLp_fst {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : WithLp p (α × β)) : x.ofLp.1 = x.fst

@[simp]

theorem WithLp.ofLp_snd {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : WithLp p (α × β)) : x.ofLp.2 = x.snd

Definition of edist, dist and norm on WithLp p (α × β)

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

instance WithLp.instProdEDist (p : ENNReal) (α : Type u_2) (β : Type u_3) [EDist α] [EDist β] : EDist (WithLp p (α × β))

Endowing the space WithLp p (α × β) with the L^p edistance. We register this instance separate from WithLp.instProdPseudoEMetric 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 WithLp 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.

@[simp]

theorem WithLp.prod_edist_eq_card {α : Type u_2} {β : Type u_3} [EDist α] [EDist β] (f g : WithLp 0 (α × β)) : edist f g = (if edist f.fst g.fst = 0 then 0 else 1) + if edist f.snd g.snd = 0 then 0 else 1

theorem WithLp.prod_edist_eq_add {p : ENNReal} {α : Type u_2} {β : Type u_3} [EDist α] [EDist β] (hp : 0 < p.toReal) (f g : WithLp p (α × β)) : edist f g = (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)

theorem WithLp.prod_edist_eq_sup {α : Type u_2} {β : Type u_3} [EDist α] [EDist β] (f g : WithLp ⊤ (α × β)) : edist f g = max (edist f.fst g.fst) (edist f.snd g.snd)

theorem WithLp.prod_edist_self (p : ENNReal) {α : Type u_2} {β : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : WithLp p (α × β)) : edist f f = 0

The distance from one point to itself is always zero.

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

theorem WithLp.prod_edist_comm (p : ENNReal) {α : Type u_2} {β : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f g : WithLp p (α × β)) : edist f g = edist g f

The distance is symmetric.

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

instance WithLp.instProdDist (p : ENNReal) (α : Type u_2) (β : Type u_3) [Dist α] [Dist β] : Dist (WithLp p (α × β))

Endowing the space WithLp p (α × β) with the L^p distance. We register this instance separate from WithLp.instProdPseudoMetricSpace 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 WithLp 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 WithLp.prod_dist_eq_card {α : Type u_2} {β : Type u_3} [Dist α] [Dist β] (f g : WithLp 0 (α × β)) : dist f g = (if dist f.fst g.fst = 0 then 0 else 1) + if dist f.snd g.snd = 0 then 0 else 1

theorem WithLp.prod_dist_eq_add {p : ENNReal} {α : Type u_2} {β : Type u_3} [Dist α] [Dist β] (hp : 0 < p.toReal) (f g : WithLp p (α × β)) : dist f g = (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)

theorem WithLp.prod_dist_eq_sup {α : Type u_2} {β : Type u_3} [Dist α] [Dist β] (f g : WithLp ⊤ (α × β)) : dist f g = max (dist f.fst g.fst) (dist f.snd g.snd)

instance WithLp.instProdNorm (p : ENNReal) (α : Type u_2) (β : Type u_3) [Norm α] [Norm β] : Norm (WithLp p (α × β))

Endowing the space WithLp p (α × β) with the L^p norm. We register this instance separate from WithLp.instProdSeminormedAddCommGroup 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 WithLp p (α × β) for p < 1 satisfying a relaxed triangle inequality. These are called quasi-norms.

Equations

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

@[simp]

theorem WithLp.prod_norm_eq_card {α : Type u_2} {β : Type u_3} [Norm α] [Norm β] (f : WithLp 0 (α × β)) : ‖f‖ = (if ‖f.fst‖ = 0 then 0 else 1) + if ‖f.snd‖ = 0 then 0 else 1

theorem WithLp.prod_norm_eq_sup {α : Type u_2} {β : Type u_3} [Norm α] [Norm β] (f : WithLp ⊤ (α × β)) : ‖f‖ = max ‖f.fst‖ ‖f.snd‖

theorem WithLp.prod_norm_eq_add {p : ENNReal} {α : Type u_2} {β : Type u_3} [Norm α] [Norm β] (hp : 0 < p.toReal) (f : WithLp p (α × β)) : ‖f‖ = (‖f.fst‖ ^ p.toReal + ‖f.snd‖ ^ 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 WithLp p (α × β), and we check that the uniformity coming from this edistance coincides with the product uniformity, by showing that the canonical map to the Prod 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.

TODO: the results about uniformity and bornology should be using the tools in Mathlib.Topology.MetricSpace.Bilipschitz, so that they can be inlined in the next section and the only remaining results are about Lipschitz and Antilipschitz.

def WithLp.prodPseudoEMetricAux (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] : PseudoEMetricSpace (WithLp p (α × β))

Endowing the space WithLp 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

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

theorem WithLp.prod_sup_edist_ne_top_aux {α : Type u_2} {β : Type u_3} [PseudoMetricSpace α] [PseudoMetricSpace β] (f g : WithLp ⊤ (α × β)) : max (edist f.fst g.fst) (edist f.snd g.snd) ≠ ⊤

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

@[reducible, inline]

abbrev WithLp.prodPseudoMetricAux (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoMetricSpace α] [PseudoMetricSpace β] : PseudoMetricSpace (WithLp p (α × β))

Endowing the space WithLp 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

• WithLp.prodPseudoMetricAux p α β = PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯

instance WithLp.instProdBornology (p : ENNReal) (α : Type u_4) (β : Type u_5) [Bornology α] [Bornology β] : Bornology (WithLp p (α × β))

Equations

• WithLp.instProdBornology p α β = Bornology.induced WithLp.ofLp

Instances on L^p products

instance WithLp.instProdTopologicalSpace (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] : TopologicalSpace (WithLp p (α × β))

Equations

• WithLp.instProdTopologicalSpace p α β = TopologicalSpace.induced WithLp.ofLp instTopologicalSpaceProd

theorem WithLp.prod_continuous_toLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] : Continuous (toLp p)

theorem WithLp.prod_continuous_ofLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] : Continuous ofLp

def WithLp.homeomorphProd (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] : WithLp p (α × β) ≃ₜ α × β

WithLp.equiv as a homeomorphism.

Equations

• WithLp.homeomorphProd p α β = { toEquiv := WithLp.equiv p (α × β), continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem WithLp.toEquiv_homeomorphProd (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] : (homeomorphProd p α β).toEquiv = WithLp.equiv p (α × β)

theorem WithLp.continuous_fst (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] : Continuous WithLp.fst

theorem WithLp.continuous_snd (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] : Continuous WithLp.snd

instance WithLp.instProdT0Space (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [T0Space α] [T0Space β] : T0Space (WithLp p (α × β))

instance WithLp.secondCountableTopology (p : ENNReal) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology α] [SecondCountableTopology β] : SecondCountableTopology (WithLp p (α × β))

instance WithLp.instProdUniformSpace (p : ENNReal) (α : Type u_2) (β : Type u_3) [UniformSpace α] [UniformSpace β] : UniformSpace (WithLp p (α × β))

Equations

• WithLp.instProdUniformSpace p α β = UniformSpace.comap WithLp.ofLp instUniformSpaceProd

theorem WithLp.prod_uniformContinuous_toLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [UniformSpace α] [UniformSpace β] : UniformContinuous (toLp p)

theorem WithLp.prod_uniformContinuous_ofLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [UniformSpace α] [UniformSpace β] : UniformContinuous ofLp

def WithLp.uniformEquivProd (p : ENNReal) (α : Type u_2) (β : Type u_3) [UniformSpace α] [UniformSpace β] : WithLp p (α × β) ≃ᵤ α × β

WithLp.equiv as a uniform isomorphism.

Equations

• WithLp.uniformEquivProd p α β = { toEquiv := WithLp.equiv p (α × β), uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

@[simp]

theorem WithLp.toHomeomorph_uniformEquivProd (p : ENNReal) (α : Type u_2) (β : Type u_3) [UniformSpace α] [UniformSpace β] : (uniformEquivProd p α β).toHomeomorph = homeomorphProd p α β

@[simp]

theorem WithLp.toEquiv_uniformEquivProd (p : ENNReal) (α : Type u_2) (β : Type u_3) [UniformSpace α] [UniformSpace β] : (uniformEquivProd p α β).toEquiv = WithLp.equiv p (α × β)

instance WithLp.instProdCompleteSpace (p : ENNReal) (α : Type u_2) (β : Type u_3) [UniformSpace α] [UniformSpace β] [CompleteSpace α] [CompleteSpace β] : CompleteSpace (WithLp p (α × β))

def WithLp.prodContinuousLinearEquiv (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] : WithLp p (α × β) ≃L[𝕜] α × β

WithLp.equiv as a continuous linear equivalence.

Equations

• WithLp.prodContinuousLinearEquiv p 𝕜 α β = { toLinearEquiv := WithLp.linearEquiv p 𝕜 (α × β), continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem WithLp.prodContinuousLinearEquiv_apply (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] (a✝ : WithLp p (α × β)) : (prodContinuousLinearEquiv p 𝕜 α β) a✝ = a✝.ofLp

@[simp]

theorem WithLp.prodContinuousLinearEquiv_symm_apply_ofLp (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] (a✝ : α × β) : ((prodContinuousLinearEquiv p 𝕜 α β).symm a✝).ofLp = a✝

@[simp]

theorem WithLp.prodContinuousLinearEquiv_symm_apply (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] (x : α × β) : (prodContinuousLinearEquiv p 𝕜 α β).symm x = toLp p x

def WithLp.fstL (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] : WithLp p (α × β) →L[𝕜] α

WithLp.fst as a continuous linear map.

Equations

• WithLp.fstL p 𝕜 α β = { toLinearMap := WithLp.fstₗ p 𝕜 α β, cont := ⋯ }

@[simp]

theorem WithLp.fstL_apply (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] (x : WithLp p (α × β)) : (fstL p 𝕜 α β) x = x.fst

@[simp]

theorem WithLp.coe_fstL (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] : ↑(fstL p 𝕜 α β) = fstₗ p 𝕜 α β

def WithLp.sndL (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] : WithLp p (α × β) →L[𝕜] β

WithLp.snd as a continuous linear map.

Equations

• WithLp.sndL p 𝕜 α β = { toLinearMap := WithLp.sndₗ p 𝕜 α β, cont := ⋯ }

@[simp]

theorem WithLp.sndL_apply (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] (x : WithLp p (α × β)) : (sndL p 𝕜 α β) x = x.snd

@[simp]

theorem WithLp.coe_sndL (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [Semiring 𝕜] [AddCommGroup α] [AddCommGroup β] [Module 𝕜 α] [Module 𝕜 β] : ↑(sndL p 𝕜 α β) = sndₗ p 𝕜 α β

Throughout the rest of the file, we assume 1 ≤ p.

instance WithLp.instProdPseudoEMetricSpace (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] : PseudoEMetricSpace (WithLp p (α × β))

PseudoEMetricSpace instance on the product of two pseudoemetric spaces, using the L^p pseudoedistance, and having as uniformity the product uniformity.

Equations

• WithLp.instProdPseudoEMetricSpace p α β = (WithLp.prodPseudoEMetricAux p α β).replaceUniformity ⋯

instance WithLp.instProdEMetricSpace (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [EMetricSpace α] [EMetricSpace β] : EMetricSpace (WithLp p (α × β))

EMetricSpace instance on the product of two emetric spaces, using the L^p edistance, and having as uniformity the product uniformity.

Equations

• WithLp.instProdEMetricSpace p α β = EMetricSpace.ofT0PseudoEMetricSpace (WithLp p (α × β))

instance WithLp.instProdPseudoMetricSpace (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoMetricSpace α] [PseudoMetricSpace β] : PseudoMetricSpace (WithLp p (α × β))

PseudoMetricSpace instance on the product of two pseudometric spaces, using the L^p distance, and having as uniformity the product uniformity.

Equations

• WithLp.instProdPseudoMetricSpace p α β = ((WithLp.prodPseudoMetricAux p α β).replaceUniformity ⋯).replaceBornology ⋯

instance WithLp.instProdMetricSpace (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [MetricSpace α] [MetricSpace β] : MetricSpace (WithLp p (α × β))

MetricSpace instance on the product of two metric spaces, using the L^p distance, and having as uniformity the product uniformity.

Equations

• WithLp.instProdMetricSpace p α β = MetricSpace.ofT0PseudoMetricSpace (WithLp p (α × β))

theorem WithLp.prod_nndist_eq_add {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [PseudoMetricSpace α] [PseudoMetricSpace β] : p ≠ ⊤ → ∀ (x y : WithLp p (α × β)), nndist x y = (nndist x.fst y.fst ^ p.toReal + nndist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

theorem WithLp.prod_nndist_eq_sup {α : Type u_2} {β : Type u_3} [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp ⊤ (α × β)) : nndist x y = max (nndist x.fst y.fst) (nndist x.snd y.snd)

theorem WithLp.edist_fst_le {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x y : WithLp p (α × β)) : edist x.fst y.fst ≤ edist x y

theorem WithLp.edist_snd_le {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x y : WithLp p (α × β)) : edist x.snd y.snd ≤ edist x y

theorem WithLp.nndist_fst_le {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp p (α × β)) : nndist x.fst y.fst ≤ nndist x y

theorem WithLp.nndist_snd_le {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp p (α × β)) : nndist x.snd y.snd ≤ nndist x y

theorem WithLp.dist_fst_le {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp p (α × β)) : dist x.fst y.fst ≤ dist x y

theorem WithLp.dist_snd_le {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp p (α × β)) : dist x.snd y.snd ≤ dist x y

theorem WithLp.prod_lipschitzWith_ofLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] : LipschitzWith 1 ofLp

theorem WithLp.prod_antilipschitzWith_toLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] : AntilipschitzWith 1 (toLp p)

theorem WithLp.prod_antilipschitzWith_ofLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] : AntilipschitzWith (2 ^ (1 / p).toReal) ofLp

theorem WithLp.prod_lipschitzWith_toLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] : LipschitzWith (2 ^ (1 / p).toReal) (toLp p)

theorem WithLp.prod_isometry_ofLp_infty (α : Type u_2) (β : Type u_3) [PseudoEMetricSpace α] [PseudoEMetricSpace β] : Isometry ofLp

instance WithLp.instProdSeminormedAddCommGroup (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] : SeminormedAddCommGroup (WithLp p (α × β))

Seminormed group instance on the product of two normed groups, using the L^p norm.

Equations

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

theorem WithLp.isUniformInducing_toLp (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [PseudoEMetricSpace α] [PseudoEMetricSpace β] : IsUniformInducing (toLp p)

theorem WithLp.enorm_fst_le {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.fst‖ₑ ≤ ‖x‖ₑ

theorem WithLp.enorm_snd_le {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.snd‖ₑ ≤ ‖x‖ₑ

theorem WithLp.nnnorm_fst_le {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.fst‖₊ ≤ ‖x‖₊

theorem WithLp.nnnorm_snd_le {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.snd‖₊ ≤ ‖x‖₊

theorem WithLp.norm_fst_le {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.fst‖ ≤ ‖x‖

theorem WithLp.norm_snd_le {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.snd‖ ≤ ‖x‖

instance WithLp.instProdNormedAddCommGroup (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [NormedAddCommGroup α] [NormedAddCommGroup β] : NormedAddCommGroup (WithLp p (α × β))

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

Equations

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

theorem WithLp.prod_norm_eq_of_nat {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [Norm α] [Norm β] (n : ℕ) (h : p = ↑n) (f : WithLp p (α × β)) : ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ (1 / ↑n)

theorem WithLp.prod_nnnorm_eq_add {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] : p ≠ ⊤ → ∀ (f : WithLp p (α × β)), ‖f‖₊ = (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)

theorem WithLp.prod_nnnorm_eq_sup {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (f : WithLp ⊤ (α × β)) : ‖f‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊

@[simp]

theorem WithLp.prod_nnnorm_ofLp {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (f : WithLp ⊤ (α × β)) : ‖f.ofLp‖₊ = ‖f‖₊

@[simp]

theorem WithLp.prod_nnnorm_toLp {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (f : α × β) : ‖toLp ⊤ f‖₊ = ‖f‖₊

@[simp]

theorem WithLp.prod_norm_ofLp {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (f : WithLp ⊤ (α × β)) : ‖f.ofLp‖ = ‖f‖

@[simp]

theorem WithLp.prod_norm_toLp {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (f : α × β) : ‖toLp ⊤ f‖ = ‖f‖

theorem WithLp.prod_norm_eq_of_L1 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp 1 (α × β)) : ‖x‖ = ‖x.fst‖ + ‖x.snd‖

theorem WithLp.prod_nnnorm_eq_of_L1 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp 1 (α × β)) : ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊

theorem WithLp.prod_dist_eq_of_L1 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x y : WithLp 1 (α × β)) : dist x y = dist x.fst y.fst + dist x.snd y.snd

theorem WithLp.prod_nndist_eq_of_L1 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x y : WithLp 1 (α × β)) : nndist x y = nndist x.fst y.fst + nndist x.snd y.snd

theorem WithLp.prod_edist_eq_of_L1 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x y : WithLp 1 (α × β)) : edist x y = edist x.fst y.fst + edist x.snd y.snd

theorem WithLp.prod_norm_eq_of_L2 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp 2 (α × β)) : ‖x‖ = √(‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2)

theorem WithLp.prod_nnnorm_eq_of_L2 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp 2 (α × β)) : ‖x‖₊ = NNReal.sqrt (‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2)

theorem WithLp.prod_norm_sq_eq_of_L2 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp 2 (α × β)) : ‖x‖ ^ 2 = ‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2

theorem WithLp.prod_dist_eq_of_L2 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x y : WithLp 2 (α × β)) : dist x y = √(dist x.fst y.fst ^ 2 + dist x.snd y.snd ^ 2)

theorem WithLp.prod_nndist_eq_of_L2 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x y : WithLp 2 (α × β)) : nndist x y = NNReal.sqrt (nndist x.fst y.fst ^ 2 + nndist x.snd y.snd ^ 2)

theorem WithLp.prod_edist_eq_of_L2 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x y : WithLp 2 (α × β)) : edist x y = (edist x.fst y.fst ^ 2 + edist x.snd y.snd ^ 2) ^ (1 / 2)

@[simp]

theorem WithLp.nnnorm_toLp_inl (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : α) : ‖toLp p (x, 0)‖₊ = ‖x‖₊

@[simp]

theorem WithLp.nnnorm_toLp_inr (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (y : β) : ‖toLp p (0, y)‖₊ = ‖y‖₊

@[simp]

theorem WithLp.norm_toLp_fst (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : α) : ‖toLp p (x, 0)‖ = ‖x‖

@[simp]

theorem WithLp.norm_toLp_snd (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (y : β) : ‖toLp p (0, y)‖ = ‖y‖

@[simp]

theorem WithLp.nndist_toLp_fst (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x₁ x₂ : α) : nndist (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂

@[simp]

theorem WithLp.nndist_toLp_snd (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (y₁ y₂ : β) : nndist (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂

@[simp]

theorem WithLp.dist_toLp_fst (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x₁ x₂ : α) : dist (toLp p (x₁, 0)) (toLp p (x₂, 0)) = dist x₁ x₂

@[simp]

theorem WithLp.dist_toLp_snd (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (y₁ y₂ : β) : dist (toLp p (0, y₁)) (toLp p (0, y₂)) = dist y₁ y₂

@[simp]

theorem WithLp.edist_toLp_fst (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x₁ x₂ : α) : edist (toLp p (x₁, 0)) (toLp p (x₂, 0)) = edist x₁ x₂

@[simp]

theorem WithLp.edist_toLp_snd (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (y₁ y₂ : β) : edist (toLp p (0, y₁)) (toLp p (0, y₂)) = edist y₁ y₂

instance WithLp.instProdIsBoundedSMul (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] [SeminormedRing 𝕜] [Module 𝕜 α] [Module 𝕜 β] [IsBoundedSMul 𝕜 α] [IsBoundedSMul 𝕜 β] : IsBoundedSMul 𝕜 (WithLp p (α × β))

def WithLp.prodEquivₗᵢ {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] [SeminormedRing 𝕜] [Module 𝕜 α] [Module 𝕜 β] : WithLp ⊤ (α × β) ≃ₗᵢ[𝕜] α × β

The canonical map WithLp.equiv between WithLp ∞ (α × β) and α × β as a linear isometric equivalence.

Equations

• WithLp.prodEquivₗᵢ = { toFun := (WithLp.equiv ⊤ (α × β)).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (WithLp.equiv ⊤ (α × β)).invFun, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

instance WithLp.instProdNormSMulClass (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] [SeminormedRing 𝕜] [Module 𝕜 α] [Module 𝕜 β] [NormSMulClass 𝕜 α] [NormSMulClass 𝕜 β] : NormSMulClass 𝕜 (WithLp p (α × β))

def WithLp.idemFst {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} : AddMonoid.End (WithLp p (α × β))

Projection on WithLp p (α × β) with range α and kernel β

Equations

• WithLp.idemFst = { toFun := fun (x : WithLp p (α × β)) => WithLp.toLp p (x.fst, 0), map_zero' := ⋯, map_add' := ⋯ }

def WithLp.idemSnd {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} : AddMonoid.End (WithLp p (α × β))

Projection on WithLp p (α × β) with range β and kernel α

Equations

• WithLp.idemSnd = { toFun := fun (x : WithLp p (α × β)) => WithLp.toLp p (0, x.snd), map_zero' := ⋯, map_add' := ⋯ }

theorem WithLp.idemFst_apply {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} (x : WithLp p (α × β)) : idemFst x = toLp p (x.fst, 0)

theorem WithLp.idemSnd_apply {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} (x : WithLp p (α × β)) : idemSnd x = toLp p (0, x.snd)

@[simp]

theorem WithLp.idemFst_add_idemSnd {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} : idemFst + idemSnd = 1

theorem WithLp.idemFst_compl {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} : 1 - idemFst = idemSnd

theorem WithLp.idemSnd_compl {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} : 1 - idemSnd = idemFst

theorem WithLp.prod_norm_eq_idemFst_sup_idemSnd {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp ⊤ (α × β)) : ‖x‖ = max ‖idemFst x‖ ‖idemSnd x‖

theorem WithLp.prod_norm_eq_add_idemFst {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {p : ENNReal} [Fact (1 ≤ p)] (hp : 0 < p.toReal) (x : WithLp p (α × β)) : ‖x‖ = (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)

theorem WithLp.prod_norm_eq_idemFst_of_L1 {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp 1 (α × β)) : ‖x‖ = ‖idemFst x‖ + ‖idemSnd x‖

instance WithLp.instProdNormedSpace (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] [NormedField 𝕜] [NormedSpace 𝕜 α] [NormedSpace 𝕜 β] : NormedSpace 𝕜 (WithLp p (α × β))

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

Equations

• WithLp.instProdNormedSpace p 𝕜 α β = { toModule := WithLp.instModule p 𝕜 (α × β), norm_smul_le := ⋯ }

L^p distance on a product space

In this section we define a pseudometric space structure on α × β, as well as a seminormed group structure. These are meant to be used to put the desired instances on type synonyms of α × β. See for instance TrivSqZeroExt.instL1SeminormedAddCommGroup.

@[reducible, inline]

abbrev WithLp.pseudoMetricSpaceToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [PseudoMetricSpace α] [PseudoMetricSpace β] : PseudoMetricSpace (α × β)

This definition allows to endow α × β with the Lp distance with the uniformity and bornology being defeq to the product ones. It is useful to endow a type synonym of a × β with the Lp distance.

Equations

• WithLp.pseudoMetricSpaceToProd p α β = (IsUniformInducing.comapPseudoMetricSpace (WithLp.toLp p) ⋯).replaceBornology ⋯

theorem WithLp.dist_pseudoMetricSpaceToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : α × β) : dist x y = dist (toLp p x) (toLp p y)

@[reducible, inline]

abbrev WithLp.seminormedAddCommGroupToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] : SeminormedAddCommGroup (α × β)

This definition allows to endow α × β with the Lp norm with the uniformity and bornology being defeq to the product ones. It is useful to endow a type synonym of a × β with the Lp norm.

Equations

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

theorem WithLp.norm_seminormedAddCommGroupToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : α × β) : ‖x‖ = ‖toLp p x‖

theorem WithLp.nnnorm_seminormedAddCommGroupToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : α × β) : ‖x‖₊ = ‖toLp p x‖₊

theorem WithLp.isBoundedSMulSeminormedAddCommGroupToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {R : Type u_6} [SeminormedRing R] [Module R α] [Module R β] [IsBoundedSMul R α] [IsBoundedSMul R β] : IsBoundedSMul R (α × β)

theorem WithLp.normSMulClassSeminormedAddCommGroupToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {R : Type u_6} [SeminormedRing R] [Module R α] [Module R β] [NormSMulClass R α] [NormSMulClass R β] : NormSMulClass R (α × β)

@[reducible, inline]

abbrev WithLp.normedSpaceSeminormedAddCommGroupToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] {R : Type u_6} [NormedField R] [NormedSpace R α] [NormedSpace R β] : NormedSpace R (α × β)

This definition allows to endow α × β with a normed space structure corresponding to the Lp norm. It is useful for type synonyms of α × β.

Equations

• WithLp.normedSpaceSeminormedAddCommGroupToProd p α β = { toModule := Prod.instModule, norm_smul_le := ⋯ }

@[reducible, inline]

abbrev WithLp.normedAddCommGroupToProd (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [NormedAddCommGroup α] [NormedAddCommGroup β] : NormedAddCommGroup (α × β)

This definition allows to endow α × β with the Lp norm with the uniformity and bornology being defeq to the product ones. It is useful to endow a type synonym of α × β with the Lp norm.

Equations

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