Comparisons of finite product norms and distances

The finite Lᵖ norm is nonnegative for every exponent and respects coordinatewise bounds on norms, including when the two families have different target spaces. This compares scalar evaluations of a vector family with the vector family's Lᵖ norm. For constant fibres we deduce the bound for the image of a family under a map of bounded growth, the norm of a family of multiples of one vector, and the invariance of the norm under reindexing.

For p ≥ 1, the Lᵖ distance dominates the sup distance. In the other direction, the L² distance is at most the square root of the number of coordinates times the sup distance. These estimates give inclusions between balls in the two metrics. The corresponding Cauchy–Schwarz estimate bounds the sum of coordinate norms by √(card ι) times the L² norm. The coordinate spaces may be different seminormed groups, or pseudometric spaces for the distance comparisons.

Extending a vector of Lᵖ(ι, E) by zero along an embedding f : ι ↪ ι' places its coordinate i in the slot f i, and the vectors so obtained are those whose coordinates outside the range of f vanish. In particular, extending a vector of Lᵖ(Fin k, E) by zero onto the first k coordinates of Lᵖ(Fin n, E), for k ≤ n, places its coordinates in the slots j < k; the vectors so obtained are those whose coordinates j ≥ k vanish. The finite sum against a zero-extended vector reduces to the sum over its original coordinates.

Source

The coordinate-norm estimate is adapted from ForTauCeti/Analysis/Matrix/EntrywiseOpNorm.lean in the AIQ-Kitware DKPS formalization. Original copyright (c) 2026 Kitware, Inc.; Apache-2.0.

theorem PiLp.norm_mono {ι : Type u_1} [Fintype ι] {p : ENNReal} {E : ι → Type u_2} {F : ι → Type u_3} [(i : ι) → SeminormedAddGroup (E i)] [(i : ι) → Norm (F i)] {x : PiLp p E} {y : PiLp p F} (h : ∀ (i : ι), ‖x.ofLp i‖ ≤ ‖y.ofLp i‖) : ‖x‖ ≤ ‖y‖

Coordinatewise domination of norms implies domination of finite Lᵖ norms. The dominating family only needs a norm: the coordinate bounds ensure its nonnegativity.

theorem PiLp.norm_nonneg' {ι : Type u_1} [Fintype ι] {p : ENNReal} {E : ι → Type u_2} [(i : ι) → SeminormedAddGroup (E i)] (x : PiLp p E) : 0 ≤ ‖x‖

The finite Lᵖ norm is nonnegative for every exponent, including p < 1, where PiLp p E carries a norm but no seminormed group structure.

@[simp]

theorem PiLp.norm_norm {ι : Type u_1} [Fintype ι] {p : ENNReal} {E : ι → Type u_2} [(i : ι) → SeminormedAddCommGroup (E i)] (x : PiLp p E) : ‖WithLp.toLp p fun (i : ι) => ‖x.ofLp i‖‖ = ‖x‖

Taking coordinate norms preserves the finite Lᵖ norm.

theorem PiLp.sum_norm_le_sqrt_card_mul_norm {ι : Type u_1} [Fintype ι] {E : ι → Type u_2} [(i : ι) → SeminormedAddCommGroup (E i)] (x : PiLp 2 E) : ∑ i : ι, ‖x.ofLp i‖ ≤ √↑(Fintype.card ι) * ‖x‖

The sum of coordinate norms of a vector is at most √(card ι) times its L² norm.

theorem PiLp.norm_toLp_comp_equiv {ι : Type u_1} [Fintype ι] {p : ENNReal} {E : Type u_4} [SeminormedAddCommGroup E] {κ : Type u_5} [Fintype κ] (e : κ ≃ ι) (x : ι → E) : ‖WithLp.toLp p (x ∘ ⇑e)‖ = ‖WithLp.toLp p x‖

Reindexing a finite family along an equivalence preserves its Lᵖ norm, for every exponent.

theorem PiLp.norm_toLp_comp_le {ι : Type u_1} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {g : E → F} {C : ℝ} (hC : 0 ≤ C) (hg : ∀ (v : E), ‖g v‖ ≤ C * ‖v‖) (x : ι → E) : ‖WithLp.toLp p fun (i : ι) => g (x i)‖ ≤ C * ‖WithLp.toLp p x‖

Applying a map with ‖g v‖ ≤ C * ‖v‖ to each member of a finite family multiplies its Lᵖ norm by at most C.

theorem PiLp.norm_toLp_smul_const {ι : Type u_1} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {F : Type u_5} [SeminormedAddCommGroup F] {𝕜 : Type u_6} [NormedField 𝕜] [NormedSpace 𝕜 F] (a : ι → 𝕜) (y : F) : ‖WithLp.toLp p fun (i : ι) => a i • y‖ = ‖WithLp.toLp p a‖ * ‖y‖

A finite family of multiples of one vector has Lᵖ norm equal to the Lᵖ norm of the coefficients times the norm of the vector.

theorem PiLp.dist_ofLp_le {ι : Type u_1} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {β : ι → Type u_4} [(i : ι) → PseudoMetricSpace (β i)] (x y : PiLp p β) : dist x.ofLp y.ofLp ≤ dist x y

The sup distance of the coordinate vectors is at most the Lᵖ distance, p ≥ 1.

theorem PiLp.closedBall_subset_preimage_ofLp_closedBall {ι : Type u_1} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {β : ι → Type u_4} [(i : ι) → PseudoMetricSpace (β i)] (x : PiLp p β) (r : ℝ) : Metric.closedBall x r ⊆ WithLp.ofLp ⁻¹' Metric.closedBall x.ofLp r

The closed ball of radius r about x lies in the closed sup-metric ball of radius r about ofLp x.

theorem PiLp.ball_subset_preimage_ofLp_ball {ι : Type u_1} [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {β : ι → Type u_4} [(i : ι) → PseudoMetricSpace (β i)] (x : PiLp p β) (r : ℝ) : Metric.ball x r ⊆ WithLp.ofLp ⁻¹' Metric.ball x.ofLp r

The open ball of radius r about x lies in the open sup-metric ball of radius r about ofLp x.

theorem PiLp.dist_le_sqrt_card_mul_dist_ofLp {ι : Type u_1} [Fintype ι] {β : ι → Type u_4} [(i : ι) → PseudoMetricSpace (β i)] (x y : PiLp 2 β) : dist x y ≤ √↑(Fintype.card ι) * dist x.ofLp y.ofLp

The L² distance is at most the square root of the coordinate count times the sup distance between the coordinate vectors.

theorem PiLp.preimage_ofLp_closedBall_subset_closedBall {ι : Type u_1} [Fintype ι] {β : ι → Type u_4} [(i : ι) → PseudoMetricSpace (β i)] (x : PiLp 2 β) (r : ℝ) : WithLp.ofLp ⁻¹' Metric.closedBall x.ofLp r ⊆ Metric.closedBall x (√↑(Fintype.card ι) * r)

A sup-metric closed ball of radius r pulls back into the L² closed ball of radius √(card ι) * r.

theorem PiLp.preimage_ofLp_ball_subset_ball {ι : Type u_1} [Fintype ι] {β : ι → Type u_4} [(i : ι) → PseudoMetricSpace (β i)] [Nonempty ι] (x : PiLp 2 β) (r : ℝ) : WithLp.ofLp ⁻¹' Metric.ball x.ofLp r ⊆ Metric.ball x (√↑(Fintype.card ι) * r)

A sup-metric open ball of radius r pulls back into the L² open ball of radius √(card ι) * r. The index type must be nonempty so that this scale factor is positive.

theorem LinearIsometry.piLpExtendByZero_apply_apply {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {ι : Type u_3} {ι' : Type u_4} [Fintype ι] [Fintype ι'] (f : ι ↪ ι') (v : PiLp p fun (x : ι) => E) (i : ι) : ((piLpExtendByZero p 𝕜 E f) v).ofLp (f i) = v.ofLp i

Extending a vector of Lᵖ(ι, E) by zero along an embedding f : ι ↪ ι' puts its coordinate i in the slot f i.

theorem LinearIsometry.range_piLpExtendByZero {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {ι : Type u_3} {ι' : Type u_4} [Fintype ι] [Fintype ι'] (f : ι ↪ ι') : Set.range ⇑(piLpExtendByZero p 𝕜 E f) = {y : PiLp p fun (x : ι') => E | ∀ j ∉ Set.range ⇑f, y.ofLp j = 0}

The vectors of Lᵖ(ι', E) obtained by extending a vector of Lᵖ(ι, E) by zero along an embedding f : ι ↪ ι' are those whose coordinates outside the range of f vanish.

theorem LinearIsometry.piLpExtendByZero_castLEEmb_apply {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {k n : ℕ} (hk : k ≤ n) (w : PiLp p fun (x : Fin k) => E) (j : Fin n) : ((piLpExtendByZero p 𝕜 E (Fin.castLEEmb hk)) w).ofLp j = if h : ↑j < k then w.ofLp ⟨↑j, h⟩ else 0

Extending a vector of Lᵖ(Fin k, E) by zero onto the first k coordinates of Lᵖ(Fin n, E) puts its coordinates in the slots j < k and zeros elsewhere.

theorem LinearIsometry.range_piLpExtendByZero_castLEEmb {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {k n : ℕ} (hk : k ≤ n) : Set.range ⇑(piLpExtendByZero p 𝕜 E (Fin.castLEEmb hk)) = {y : PiLp p fun (x : Fin n) => E | ∀ (j : Fin n), k ≤ ↑j → y.ofLp j = 0}

The vectors of Lᵖ(Fin n, E) obtained by extending a vector of Lᵖ(Fin k, E) by zero are those whose coordinates j ≥ k vanish.

theorem LinearIsometry.sum_mul_piLpExtendByZero {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_1} [NormedRing 𝕜] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Fintype ι'] (f : ι ↪ ι') (x : PiLp p fun (x : ι) => 𝕜) (h : ι' → 𝕜) : ∑ b : ι', h b * ((piLpExtendByZero p 𝕜 𝕜 f) x).ofLp b = ∑ a : ι, h (f a) * x.ofLp a

A finite sum paired with a vector extended by zero along an embedding reduces to the sum over the original coordinates.