Weighted ℓᵖ_ν Sequence Spaces

This file defines the weighted ℓᵖ space with weight ν > 0:

ℓᵖ_ν = { a : ℕ → ℝ | ‖a‖_{p,ν} := (Σₙ |aₙ|^p · ν^{pn})^{1/p} < ∞ }

Architecture Overview

The formalization separates algebraic and analytic concerns:

┌─────────────────────────────────────────────────────────────┐
│                     CauchyProduct.lean                      │
│  Pure algebra: ring axioms transported from PowerSeries     │
│  - assoc, comm, left_distrib, right_distrib                 │
│  - one, one_mul, mul_one                                    │
│  - smul_mul, mul_smul (scalar compatibility)                │
└─────────────────────────────────────────────────────────────┘
                              ↓
┌─────────────────────────────────────────────────────────────┐
│                      lpWeighted.lean                        │
│  Analysis: norms, membership, submultiplicativity           │
│  - Weighted ℓᵖ space as lp (ScaledReal ν) p                 │
│  - Closure under Cauchy product (mem)                       │
│  - Submultiplicativity: ‖a ⋆ b‖ ≤ ‖a‖ · ‖b‖                 │
│  - Typeclass instances: Ring, CommRing, NormedRing          │
└─────────────────────────────────────────────────────────────┘

Design Philosophy: "Transport from PowerSeries"

Ring axioms (associativity, distributivity, etc.) are not reproven manually. Instead, CauchyProduct.lean establishes that the Cauchy product equals PowerSeries multiplication via toPowerSeries_mul, then transports the axioms. This file only proves the analytic properties:

1. Membership closure: a, b ∈ ℓ¹_ν ⟹ a ⋆ b ∈ ℓ¹_ν
2. Submultiplicativity: ‖a ⋆ b‖ ≤ ‖a‖ · ‖b‖ (Mertens + weight factorization)
3. Norm of identity: ‖1‖ = 1

The ring axiom lemmas in this file are thin wrappers that lift the CauchyProduct lemmas to l1Weighted via lpWeighted.ext and congrFun.

Main Definitions

• lpWeighted ν p: The Banach space ℓᵖ_ν, defined as lp (ScaledReal ν) p
• l1Weighted ν: Specialization to p = 1
• l1Weighted.mul: Cauchy product multiplication on ℓ¹_ν
• l1Weighted.one: Identity element for the Banach algebra
• l1Weighted.single: Standard basis vectors

Main Results

Banach Space Structure

• lpWeighted.instCompleteSpace: ℓᵖ_ν is complete (inherited from Mathlib)

Banach Algebra Structure (ℓ¹_ν only)

• l1Weighted.mem: Cauchy product preserves membership
• l1Weighted.norm_mul_le: Submultiplicativity ‖a ⋆ b‖ ≤ ‖a‖ · ‖b‖
• l1Weighted.instCommRing: ℓ¹_ν is a commutative ring
• l1Weighted.instNormedRing: ℓ¹_ν is a normed ring
• l1Weighted.instNormOneClass: ‖1‖ = 1
• l1Weighted.instSMulCommClass: Scalar-ring multiplication compatibility
• l1Weighted.instIsScalarTower: Scalar tower compatibility
• l1Weighted.instAlgebra: ℓ¹_ν is an ℝ-algebra
• l1Weighted.instNormedAlgebra: ℓ¹_ν is a normed ℝ-algebra
• l1Weighted.norm_pow_le: ‖a^n‖ ≤ ‖a‖^n

Dependencies

• ScaledReal.lean: Provides the scaled fiber type ScaledReal ν n
• CauchyProduct.lean: Provides algebraic properties (ring axioms)

References

• Section 7.4 of the radii polynomial textbook
• Definition 7.4.1: Banach algebra axioms
• Theorem 7.4.4: Submultiplicativity proof
• Corollary 7.4.5: ℓ¹_ν is a commutative Banach algebra

Part 1: Weighted ℓᵖ Space (General p)

lpWeighted ν p is the Banach space of sequences with finite weighted ℓᵖ norm. Defined as lp (ScaledReal ν) p, inheriting completeness from Mathlib.

The norm is: ‖a‖_{p,ν} = (Σₙ |aₙ|^p · ν^{pn})^{1/p}

@[reducible, inline]

abbrev lpWeighted (ν : PosReal) (p : ENNReal) : AddSubgroup (PreLp (ScaledReal ν))

The weighted ℓᵖ_ν space, realized as lp with scaled fibers.

Key insight: By using ScaledReal ν n (which has norm |x| · νⁿ) as the fiber at index n, the standard lp machinery gives us the weighted norm automatically.

Equations

• lpWeighted ν p = lp (ScaledReal ν) p

@[reducible, inline]

abbrev l1Weighted (ν : PosReal) : AddSubgroup (PreLp (ScaledReal ν))

Specialization to weighted ℓ¹.

This is the main space of interest for the Banach algebra structure. See Section 7.4: ℓ¹_ν = { a : ℕ → ℝ | ‖a‖₁,ν := Σₙ |aₙ| νⁿ < ∞ }

Equations

• l1Weighted ν = lpWeighted ν 1

Inherited Topological Structure

instance lpWeighted.instUniformSpace {ν : PosReal} {p : ENNReal} [Fact (1 ≤ p)] : UniformSpace ↥(lpWeighted ν p)

Equations

• lpWeighted.instUniformSpace = id inferInstance

instance lpWeighted.instCompleteSpace {ν : PosReal} {p : ENNReal} [Fact (1 ≤ p)] : CompleteSpace ↥(lpWeighted ν p)

ℓᵖ_ν is complete (a Banach space) for p ≥ 1.

This is inherited from Mathlib's completeness of lp.

Sequence Extraction

def lpWeighted.toSeq {p : ENNReal} {ν : PosReal} (a : ↥(lpWeighted ν p)) : ℕ → ℝ

Extract the underlying ℝ-valued sequence from a weighted ℓᵖ element.

This "forgets" the weighted norm structure and gives a plain function ℕ → ℝ.

Equations

• lpWeighted.toSeq a n = ↑(↑a n)

theorem lpWeighted.ext {ν : PosReal} {p : ENNReal} {a b : ↥(lpWeighted ν p)} (h : ∀ (n : ℕ), toSeq a n = toSeq b n) : a = b

Extensionality: two weighted sequences are equal iff their underlying real sequences are equal.

Membership and Construction

def lpWeighted.Mem (ν : PosReal) (p : ENNReal) (a : ℕ → ℝ) : Prop

Membership predicate: a sequence has finite weighted ℓᵖ norm.

Equations

• lpWeighted.Mem ν p a = Memℓp (fun (n : ℕ) => ScaledReal.ofReal (a n)) p

def lpWeighted.mk {ν : PosReal} {p : ENNReal} (a : ℕ → ℝ) (ha : Mem ν p a) : ↥(lpWeighted ν p)

Construct a weighted ℓᵖ element from a sequence with finite weighted norm.

Equations

• lpWeighted.mk a ha = ⟨fun (n : ℕ) => ScaledReal.ofReal (a n), ha⟩

Simp Lemmas for Sequence Operations

@[simp]

theorem lpWeighted.toSeq_apply {ν : PosReal} {p : ENNReal} (a : ↥(lpWeighted ν p)) (n : ℕ) : toSeq a n = ↑a n

@[simp]

theorem lpWeighted.mk_apply {ν : PosReal} {p : ENNReal} (a : ℕ → ℝ) (ha : Mem ν p a) (n : ℕ) : toSeq (mk a ha) n = a n

@[simp]

theorem lpWeighted.zero_toSeq {ν : PosReal} {p : ENNReal} (n : ℕ) : toSeq 0 n = 0

@[simp]

theorem lpWeighted.neg_toSeq {ν : PosReal} {p : ENNReal} (a : ↥(lpWeighted ν p)) (n : ℕ) : toSeq (-a) n = -toSeq a n

@[simp]

theorem lpWeighted.add_toSeq {ν : PosReal} {p : ENNReal} (a b : ↥(lpWeighted ν p)) (n : ℕ) : toSeq (a + b) n = toSeq a n + toSeq b n

@[simp]

theorem lpWeighted.sub_toSeq {ν : PosReal} {p : ENNReal} (a b : ↥(lpWeighted ν p)) (n : ℕ) : toSeq (a - b) n = toSeq a n - toSeq b n

@[simp]

theorem lpWeighted.smul_toSeq {ν : PosReal} {p : ENNReal} (c : ℝ) (a : ↥(lpWeighted ν p)) (n : ℕ) : toSeq (c • a) n = c * toSeq a n

Norm Characterization

theorem lpWeighted.norm_eq_tsum_rpow {ν : PosReal} {p : ENNReal} (hp : 0 < p.toReal) (a : ↥(lpWeighted ν p)) : ‖a‖ = (∑' (n : ℕ), (|toSeq a n| * ↑ν ^ n) ^ p.toReal) ^ (1 / p.toReal)

The norm for lpWeighted expressed as a weighted sum.

theorem lpWeighted.mem_iff_summable {ν : PosReal} {p : ENNReal} (hp : 0 < p.toReal) (a : ℕ → ℝ) (hp' : p ≠ ⊤) : Mem ν p a ↔ Summable fun (n : ℕ) => (|a n| * ↑ν ^ n) ^ p.toReal

Membership in ℓᵖ_ν ↔ weighted p-th power sum is summable.

Part 2: Weighted ℓ¹ Specialization

This section provides the API specific to l1Weighted ν, the weighted ℓ¹ space. The key simplification is that the norm becomes a simple weighted sum (no p-th powers).

instance l1Weighted.instFactLeENNRealOfNat : Fact (1 ≤ 1)

@[reducible, inline]

abbrev l1Weighted.toSeq {ν : PosReal} (a : ↥(l1Weighted ν)) : ℕ → ℝ

Alias for lpWeighted.toSeq in the ℓ¹ setting.

Equations

• l1Weighted.toSeq a = lpWeighted.toSeq a

theorem l1Weighted.norm_eq_tsum {ν : PosReal} (a : ↥(l1Weighted ν)) : ‖a‖ = ∑' (n : ℕ), |toSeq a n| * ↑ν ^ n

The ℓ¹_ν norm is a simple weighted sum: ‖a‖ = Σₙ |aₙ| νⁿ

theorem l1Weighted.mem_iff {ν : PosReal} (a : ℕ → ℝ) : lpWeighted.Mem ν 1 a ↔ Summable fun (n : ℕ) => |a n| * ↑ν ^ n

Membership in ℓ¹_ν ↔ weighted sum is summable.

Standard Basis Vectors

The single element single n x represents the sequence that is x at position n and 0 elsewhere. These are the standard basis vectors of ℓ¹_ν scaled by x.

def l1Weighted.single {ν : PosReal} (n : ℕ) (x : ℝ) : ↥(l1Weighted ν)

The single element in ℓ¹_ν: value x at position n, zero elsewhere.

This is the standard basis vector eₙ scaled by x. See Theorem 7.3.8.

Equations

• l1Weighted.single n x = lpWeighted.mk (fun (k : ℕ) => if k = n then x else 0) ⋯

@[simp]

theorem l1Weighted.single_toSeq_self {ν : PosReal} (n : ℕ) (x : ℝ) : toSeq (single n x) n = x

@[simp]

theorem l1Weighted.single_toSeq_ne {ν : PosReal} (n k : ℕ) (x : ℝ) (h : k ≠ n) : toSeq (single n x) k = 0

theorem l1Weighted.norm_single {ν : PosReal} (n : ℕ) (x : ℝ) : ‖single n x‖ = |x| * ↑ν ^ n

Norm of single element: ‖δₙ(x)‖ = |x| · νⁿ. See Theorem 7.3.8.

Finite-Dimensional Weighted Norms

These definitions support the finite-dimensional truncation used in Example 7.7. See Exercise 2.7.2 for the theory of finite-dimensional weighted norms.

def l1Weighted.finl1WeightedNorm {N : ℕ} (ν : NNReal) (x : Fin (N + 1) → ℝ) : ℝ

Finite weighted ℓ¹ norm: ‖x‖₁,ν = Σₙ |xₙ| νⁿ

Equations

• l1Weighted.finl1WeightedNorm ν x = ∑ n : Fin (N + 1), |x n| * ↑ν ^ ↑n

def l1Weighted.matrixColNorm {N : ℕ} (ν : PosReal) (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (j : Fin (N + 1)) : ℝ

Column norm for matrix: (1/νʲ) Σᵢ |Aᵢⱼ| νⁱ.

This appears in the weighted operator norm formula. See equation (7.9).

Equations

• l1Weighted.matrixColNorm ν A j = 1 / ↑ν ^ ↑j * ∑ i : Fin (N + 1), |A i j| * ↑ν ^ ↑i

def l1Weighted.finWeightedMatrixNorm {N : ℕ} (ν : PosReal) (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : ℝ

Induced matrix norm: ‖A‖_{ν,N} = max_j (1/νʲ) Σᵢ |Aᵢⱼ| νⁱ.

This is the operator norm on finite-dimensional weighted ℓ¹. See Exercise 2.7.2.

Equations

• l1Weighted.finWeightedMatrixNorm ν A = Finset.univ.sup' ⋯ fun (j : Fin (N + 1)) => l1Weighted.matrixColNorm ν A j

theorem l1Weighted.antidiagonal_weight {ν : PosReal} (n k l : ℕ) (h : k + l = n) : ↑ν ^ k * ↑ν ^ l = ↑ν ^ n

Key weight factorization: νᵏ · νˡ = νⁿ when k + l = n.

This is the crucial property enabling submultiplicativity (Theorem 7.4.4). The proof of norm_mul_le relies on this to factor νⁿ across antidiagonal pairs.

Finite Weighted Matrix Norm Properties

theorem l1Weighted.matrixColNorm_nonneg {ν : PosReal} {N : ℕ} (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (j : Fin (N + 1)) : 0 ≤ matrixColNorm ν A j

theorem l1Weighted.finWeightedMatrixNorm_nonneg {ν : PosReal} {N : ℕ} (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : 0 ≤ finWeightedMatrixNorm ν A

theorem l1Weighted.matrixColNorm_one {ν : PosReal} {N : ℕ} (j : Fin (N + 1)) : matrixColNorm ν 1 j = 1

theorem l1Weighted.finWeightedMatrixNorm_one {ν : PosReal} {N : ℕ} : finWeightedMatrixNorm ν 1 = 1

theorem l1Weighted.matrixColNorm_eq {ν : PosReal} {N : ℕ} (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (j : Fin (N + 1)) : matrixColNorm ν A j = (∑ i : Fin (N + 1), |A i j| * ↑ν ^ ↑i) / ↑ν ^ ↑j

Part 3: Banach Algebra Structure

This section establishes that ℓ¹_ν is a commutative Banach algebra (Corollary 7.4.5).

What is a Banach Algebra? (Definition 7.4.1)

A Banach algebra is a Banach space X with multiplication ·: X × X → X satisfying:

1. Associativity (7.11): x · (y · z) = (x · y) · z
2. Distributivity (7.12): (x + y) · z = x · z + y · z and x · (y + z) = x · y + x · z
3. Scalar compatibility (7.13): α(x · y) = (αx) · y = x · (αy)
4. Submultiplicativity (7.14): ‖x · y‖ ≤ ‖x‖ · ‖y‖

The algebra is commutative if x · y = y · x for all x, y.

Correspondence: Textbook ↔ Lean

Textbook	Equation	Lean Instance/Lemma
Banach space		CompleteSpace, NormedAddCommGroup
Associativity	(7.11)	instRing.mul_assoc
Left distributivity	(7.12)	instRing.left_distrib
Right distributivity	(7.12)	instRing.right_distrib
Scalar compatibility	(7.13)	instIsScalarTower, instSMulCommClass
Submultiplicativity	(7.14)	instNormedRing.norm_mul_le
Commutativity		instCommRing.mul_comm
Unit element		instRing.one_mul, instRing.mul_one
‖1‖ = 1		instNormOneClass
ℝ-algebra structure		instAlgebra, instNormedAlgebra

Why This Architecture?

Axioms (1)-(3) are pure algebra — they don't involve norms. These are proven in CauchyProduct.lean by connecting to PowerSeries R, where Mathlib has already established the ring structure.

Axiom (4) is analysis — it requires norm estimates. This is proven here using Mertens' theorem and weight factorization.

Structure of This Section

1. Membership closure (mem): Proves a, b ∈ ℓ¹_ν ⟹ a ⋆ b ∈ ℓ¹_ν
2. Multiplication (mul): Defines the ring multiplication
3. Submultiplicativity (norm_mul_le): The key analytic result (7.14)
4. Ring axioms: Thin wrappers lifting CauchyProduct lemmas (7.11-7.13)
5. Identity element (one): The Kronecker delta sequence
6. Typeclass instances: Ring, CommRing, NormedRing, NormOneClass
7. Algebra structure: SMulCommClass, IsScalarTower, Algebra, NormedAlgebra

Closure Under Multiplication

This is the first analytic result: the Cauchy product of two ℓ¹_ν sequences is again in ℓ¹_ν. The proof uses Mertens' theorem and weight factorization.

theorem l1Weighted.mem {ν : PosReal} {a b : ℕ → ℝ} (ha : lpWeighted.Mem ν 1 a) (hb : lpWeighted.Mem ν 1 b) : lpWeighted.Mem ν 1 (a ⋆ b)

Cauchy product preserves membership in ℓ¹_ν.

Proof sketch (Theorem 7.4.4):

1. Apply Mertens' theorem to reorder the double sum
2. Use weight factorization νⁿ = νᵏ · νˡ for k + l = n
3. Bound by ‖a‖ · ‖b‖

Multiplication Definition

def l1Weighted.mul {ν : PosReal} (a b : ↥(l1Weighted ν)) : ↥(l1Weighted ν)

Multiplication via Cauchy product.

This defines the Banach algebra multiplication on ℓ¹_ν. The @[simp] attribute ensures that mul a b unfolds in simp calls.

Equations

• l1Weighted.mul a b = lpWeighted.mk (lpWeighted.toSeq a ⋆ lpWeighted.toSeq b) ⋯

Submultiplicativity (Key Analytic Property)

This is axiom (4) of Definition 7.4.1, the defining property of a Banach algebra.

theorem l1Weighted.norm_mul_le {ν : PosReal} (a b : ↥(l1Weighted ν)) : ‖mul a b‖ ≤ ‖a‖ * ‖b‖

Submultiplicativity (Theorem 7.4.4, Equation 7.17): ‖a ⋆ b‖₁,ν ≤ ‖a‖₁,ν · ‖b‖₁,ν

This makes ℓ¹_ν a Banach algebra. The proof uses:

1. Mertens' theorem to exchange sum order
2. Weight factorization: νⁿ = νᵏ · νˡ for k + l = n

Ring Axioms (Lifted from CauchyProduct)

These lemmas are thin wrappers that lift the algebraic properties from CauchyProduct to l1Weighted. Each follows the same pattern:

1. Apply lpWeighted.ext to reduce to pointwise equality
2. Unfold mul to expose the Cauchy product
3. Apply the corresponding CauchyProduct lemma via congrFun

This architecture avoids re-proving ring axioms and ensures consistency with the PowerSeries multiplication structure.

theorem l1Weighted.mul_comm {ν : PosReal} (a b : ↥(l1Weighted ν)) : mul a b = mul b a

theorem l1Weighted.mul_assoc {ν : PosReal} (a b c : ↥(l1Weighted ν)) : mul (mul a b) c = mul a (mul b c)

theorem l1Weighted.left_distrib {ν : PosReal} (a b c : ↥(l1Weighted ν)) : mul a (b + c) = mul a b + mul a c

theorem l1Weighted.right_distrib {ν : PosReal} (a b c : ↥(l1Weighted ν)) : mul (a + b) c = mul a c + mul b c

theorem l1Weighted.zero_mul {ν : PosReal} (a : ↥(l1Weighted ν)) : mul 0 a = 0

theorem l1Weighted.mul_zero {ν : PosReal} (a : ↥(l1Weighted ν)) : mul a 0 = 0

Identity Element

The multiplicative identity is CauchyProduct.one: the Kronecker delta sequence with e₀ = 1 and eₙ = 0 for n ≥ 1. See Theorem 7.4.6.

theorem l1Weighted.one_mem (ν : PosReal) : lpWeighted.Mem ν 1 CauchyProduct.one

def l1Weighted.one (ν : PosReal) : ↥(l1Weighted ν)

The multiplicative identity element of ℓ¹_ν (Kronecker delta).

Equations

• l1Weighted.one ν = lpWeighted.mk CauchyProduct.one ⋯

@[simp]

theorem l1Weighted.one_toSeq_zero {ν : PosReal} : lpWeighted.toSeq (one ν) 0 = 1

@[simp]

theorem l1Weighted.one_toSeq_succ {ν : PosReal} (n : ℕ) : lpWeighted.toSeq (one ν) (n + 1) = 0

@[simp]

theorem l1Weighted.one_toSeq {ν : PosReal} : lpWeighted.toSeq (one ν) = CauchyProduct.one

theorem l1Weighted.mul_one {ν : PosReal} (a : ↥(l1Weighted ν)) : mul a (one ν) = a

theorem l1Weighted.one_mul {ν : PosReal} (a : ↥(l1Weighted ν)) : mul (one ν) a = a

theorem l1Weighted.norm_one (ν : PosReal) : ‖one ν‖ = 1

Typeclass Instances

These instances register ℓ¹_ν as a commutative Banach algebra with Lean's typeclass system, enabling generic lemmas and tactics like ring.

instance l1Weighted.instRing {ν : PosReal} : Ring ↥(l1Weighted ν)

Equations

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

instance l1Weighted.instCommRing {ν : PosReal} : CommRing ↥(l1Weighted ν)

Equations

• l1Weighted.instCommRing = { toRing := l1Weighted.instRing, mul_comm := ⋯ }

instance l1Weighted.instNormedRing {ν : PosReal} : NormedRing ↥(l1Weighted ν)

Equations

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

instance l1Weighted.instNormOneClass {ν : PosReal} : NormOneClass ↥(l1Weighted ν)

Algebra Structure (Scalar-Ring Compatibility)

These instances establish that scalar multiplication (by ℝ) is compatible with ring multiplication, making ℓ¹_ν an ℝ-algebra. This enables:

• smul_mul_assoc: (c • a) * b = c • (a * b)
• smul_comm: c • (a * b) = a * (c • b)

These are used in FrechetCauchyProduct.lean for the derivative formula.

instance l1Weighted.instSMulCommClass {ν : PosReal} : SMulCommClass ℝ ↥(l1Weighted ν) ↥(l1Weighted ν)

Scalar multiplication commutes with ring multiplication.

Says: c • (a * b) = a * (c • b) for scalars c ∈ ℝ. Uses CauchyProduct.mul_smul from the algebra layer.

instance l1Weighted.instIsScalarTower {ν : PosReal} : IsScalarTower ℝ ↥(l1Weighted ν) ↥(l1Weighted ν)

Scalar multiplication is associative with ring multiplication.

Says: (c • a) * b = c • (a * b) for scalars c ∈ ℝ. Uses CauchyProduct.smul_mul from the algebra layer.

Full Algebra Structure

These instances complete the Banach algebra structure by registering ℓ¹_ν as an ℝ-algebra. The Algebra ℝ instance bundles the ring homomorphism algebraMap that embeds ℝ into ℓ¹_ν via r ↦ r • 1 = (r, 0, 0, ...).

instance l1Weighted.instAlgebra {ν : PosReal} : Algebra ℝ ↥(l1Weighted ν)

ℓ¹_ν is an ℝ-algebra.

The algebraMap : ℝ →+* l1Weighted ν sends r ↦ r • 1 = (r, 0, 0, ...). This is synthesized from SMulCommClass and IsScalarTower via Algebra.ofModule.

Equations

• l1Weighted.instAlgebra = Algebra.ofModule ⋯ ⋯

@[simp]

theorem l1Weighted.algebraMap_apply {ν : PosReal} (r : ℝ) : (algebraMap ℝ ↥(l1Weighted ν)) r = r • 1

theorem l1Weighted.algebraMap_toSeq {ν : PosReal} (r : ℝ) (n : ℕ) : lpWeighted.toSeq ((algebraMap ℝ ↥(l1Weighted ν)) r) n = r * CauchyProduct.one n

The algebraMap sends r to the scaled identity: r · 𝟙 = (r, 0, 0, ...).

theorem l1Weighted.norm_algebraMap {ν : PosReal} (r : ℝ) : ‖(algebraMap ℝ ↥(l1Weighted ν)) r‖ = ‖r‖

The norm of algebraMap r equals |r|.

instance l1Weighted.instNormedAlgebra {ν : PosReal} : NormedAlgebra ℝ ↥(l1Weighted ν)

ℓ¹_ν is a normed ℝ-algebra.

Requires ‖c • a‖ ≤ ‖c‖ * ‖a‖, which holds with equality by norm_smul.

Equations

• l1Weighted.instNormedAlgebra = { toAlgebra := l1Weighted.instAlgebra, norm_smul_le := ⋯ }

Power Bounds

Note: Mathlib provides norm_pow_le for NormedRing + NormOneClass, but we include it explicitly for completeness and documentation.

theorem l1Weighted.norm_pow_le {ν : PosReal} (a : ↥(l1Weighted ν)) (n : ℕ) : ‖a ^ n‖ ≤ ‖a‖ ^ n

Norm bound for powers: ‖a^n‖ ≤ ‖a‖^n.

Follows from submultiplicativity by induction.