Convolution on ℓ^p(ℤ)

DefinitionConvolution of sequences on the integers#✓fully proved

Convolution of two complex sequences on ℤ, as a series. The series is 0 when it does not converge; for f ∈ ℓ¹ and g ∈ ℓ^p it always converges (see summable_intConv_term).

noncomputable def intConv (f g : ℤ → ℂ) (n : ℤ) : ℂ :=
  ∑' m, f m * g (n - m)

Used by 11

Used byConvolution is additive in the \(\ell^1\) argument · Convolution is additive in the \(\ell^p\) argument · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution · Associativity of \(\ell^1\) convolution · Commutativity of \(\ell^1\) convolution · Unit sequence is a left identity for convolution · Convolution of coordinate vectors · Convolution is homogeneous in the \(\ell^1\) argument · Convolution is homogeneous in the \(\ell^p\) argument · Convolution with zero on the left · Convolution with zero on the right

TheoremThe \(\ell^1\) norm as a sum of coordinate norms#✓fully proved

The ℓ¹ norm is the sum of the coordinate norms.

theorem tsum_norm_l1 (f : ℓ¹(ℤ, ℂ)) : ∑' m, ‖(f : ℤ → ℂ) m‖ = ‖f‖

Used by 2

Used byAssociativity of \(\ell^1\) convolution · Young's inequality with one \(\ell^1\) factor

TheoremSummability of convolution terms for \(\ell^1\) and \(\ell^p\) sequences#✓fully proved

The terms of a convolution of an ℓ¹ sequence with an ℓ^p sequence are summable.

theorem summable_intConv_term {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) (n : ℤ) :
    Summable fun m => (f : ℤ → ℂ) m * g (n - m)

Uses 1 · Used by 2

Proof usesCoordinate norms of an \(\ell^1\) family are summable

Used byConvolution is additive in the \(\ell^1\) argument · Convolution is additive in the \(\ell^p\) argument

TheoremTranslation preserves \(\ell^p\) membership#✓fully proved

Translating an ℓ^p sequence on ℤ preserves ℓ^p membership.

theorem memℓp_shift {p : ℝ≥0∞} [Fact (1 ≤ p)] {g : ℤ → ℂ} (hg : Memℓp g p)
    (m : ℤ) : Memℓp (fun n => g (n - m)) p

Used by 1

Used byTranslation of an \(\ell^p\) sequence on the integers

DefinitionTranslation of an \(\ell^p\) sequence on the integers#✓fully proved

Translation of an ℓ^p sequence on ℤ by m.

noncomputable def shiftLp {p : ℝ≥0∞} [Fact (1 ≤ p)] (m : ℤ)
    (g : ℓ^p(ℤ, ℂ)) : ℓ^p(ℤ, ℂ) :=
  ⟨fun n => g (n - m), memℓp_shift g.2 m⟩

Uses 1 · Used by 6

Statement usesTranslation preserves \(\ell^p\) membership

Used byConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution · Young's inequality with one \(\ell^1\) factor · Translation is an isometry of \(\ell^p(\mathbb{Z})\) · Pointwise formula for translation of \(\ell^p\) sequences · Summability of the Banach-space series for \(\ell^1\) convolution

TheoremPointwise formula for translation of \(\ell^p\) sequences#✓fully proved

Pointwise action of a translation.

theorem shiftLp_apply {p : ℝ≥0∞} [Fact (1 ≤ p)] (m : ℤ) (g : ℓ^p(ℤ, ℂ))
    (n : ℤ) : shiftLp m g n = g (n - m)

Uses 1 · Used by 1

Statement usesTranslation of an \(\ell^p\) sequence on the integers

Used byPointwise formula for \(\ell^1\)–\(\ell^p\) convolution

TheoremTranslation is an isometry of \(\ell^p(\mathbb{Z})\)#✓fully proved

Translation is an isometry of ℓ^p(ℤ, ℂ).

theorem norm_shiftLp {p : ℝ≥0∞} [Fact (1 ≤ p)] (m : ℤ)
    (g : ℓ^p(ℤ, ℂ)) : ‖shiftLp m g‖ = ‖g‖

Uses 1 · Used by 2

Statement usesTranslation of an \(\ell^p\) sequence on the integers

Used byYoung's inequality with one \(\ell^1\) factor · Summability of the Banach-space series for \(\ell^1\) convolution

TheoremSummability of the Banach-space series for \(\ell^1\) convolution#✓fully proved

The terms of the Banach-space series defining l1Conv are summable.

theorem summable_l1Conv_term {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) :
    Summable fun m => (f : ℤ → ℂ) m • shiftLp m g

Uses 3 · Used by 1

Statement usesTranslation of an \(\ell^p\) sequence on the integers

Proof usesTranslation is an isometry of \(\ell^p(\mathbb{Z})\) · Coordinate norms of an \(\ell^1\) family are summable

Used byPointwise formula for \(\ell^1\)–\(\ell^p\) convolution

DefinitionConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence#✓fully proved

Convolution of an ℓ¹ sequence with an ℓ^p sequence, as an element of ℓ^p(ℤ, ℂ): the Banach-space sum ∑' m, f m • shift m g.

noncomputable def l1Conv {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) : ℓ^p(ℤ, ℂ) :=
  ∑' m : ℤ, (f : ℤ → ℂ) m • shiftLp m g

Uses 1 · Used by 17

Statement usesTranslation of an \(\ell^p\) sequence on the integers

Used byConvolution is additive in the \(\ell^1\) argument · Convolution is additive in the \(\ell^p\) argument · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution · Associativity of \(\ell^1\) convolution · Convolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map · Pointwise action of the bundled convolution action · Convolution by a fixed \(\ell^1\) sequence as a bounded operator · Pointwise action of the convolution operator · Commutativity of \(\ell^1\) convolution · Unit sequence is a left identity for convolution · Unit sequence is a right identity for \(\ell^1\) convolution · Convolution of coordinate vectors · Convolution is homogeneous in the \(\ell^1\) argument · Convolution is homogeneous in the \(\ell^p\) argument · Convolution with zero on the left · Convolution with zero on the right · Young's inequality with one \(\ell^1\) factor

TheoremPointwise formula for \(\ell^1\)–\(\ell^p\) convolution#✓fully proved

Pointwise formula for convolution.

theorem l1Conv_apply {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) (n : ℤ) :
    l1Conv f g n = intConv (f : ℤ → ℂ) (g : ℤ → ℂ) n

Uses 5 · Used by 10

Statement usesConvolution of sequences on the integers · Convolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesTranslation of an \(\ell^p\) sequence on the integers · Pointwise formula for translation of \(\ell^p\) sequences · Summability of the Banach-space series for \(\ell^1\) convolution

Used byConvolution is additive in the \(\ell^1\) argument · Convolution is additive in the \(\ell^p\) argument · Associativity of \(\ell^1\) convolution · Commutativity of \(\ell^1\) convolution · Unit sequence is a left identity for convolution · Convolution of coordinate vectors · Convolution is homogeneous in the \(\ell^1\) argument · Convolution is homogeneous in the \(\ell^p\) argument · Convolution with zero on the left · Convolution with zero on the right

TheoremYoung's inequality with one \(\ell^1\) factor#✓fully proved

Young's inequality for convolution with one ℓ¹ factor.

theorem norm_l1Conv_le {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) :
    ‖l1Conv f g‖ ≤ ‖f‖ * ‖g‖

Uses 5 · Used by 2

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesTranslation is an isometry of \(\ell^p(\mathbb{Z})\) · Translation of an \(\ell^p\) sequence on the integers · The \(\ell^1\) norm as a sum of coordinate norms · Coordinate norms of an \(\ell^1\) family are summable

Used byConvolution by a fixed \(\ell^1\) sequence as a bounded operator · Operator norm of convolution by \(f\) is at most \(\|f\|_1\)

TheoremConvolution is additive in the \(\ell^1\) argument#✓fully proved

Convolution is additive in the ℓ¹ argument.

theorem l1Conv_add_left {p : ℝ≥0∞} [Fact (1 ≤ p)] (f₁ f₂ : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) :
    l1Conv (f₁ + f₂) g = l1Conv f₁ g + l1Conv f₂ g

Uses 4 · Used by 1

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution · Summability of convolution terms for \(\ell^1\) and \(\ell^p\) sequences

Used byConvolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map

TheoremConvolution is additive in the \(\ell^p\) argument#✓fully proved

Convolution is additive in the ℓ^p argument.

theorem l1Conv_add_right {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g₁ g₂ : ℓ^p(ℤ, ℂ)) :
    l1Conv f (g₁ + g₂) = l1Conv f g₁ + l1Conv f g₂

Uses 4 · Used by 1

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution · Summability of convolution terms for \(\ell^1\) and \(\ell^p\) sequences

Used byConvolution by a fixed \(\ell^1\) sequence as a bounded operator

TheoremConvolution is homogeneous in the \(\ell^1\) argument#✓fully proved

Convolution commutes with scalar multiplication in the ℓ¹ argument.

theorem l1Conv_smul_left {p : ℝ≥0∞} [Fact (1 ≤ p)] (c : ℂ) (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) :
    l1Conv (c • f) g = c • l1Conv f g

Uses 3 · Used by 1

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution

Used byConvolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map

TheoremConvolution is homogeneous in the \(\ell^p\) argument#✓fully proved

Convolution commutes with scalar multiplication in the ℓ^p argument.

theorem l1Conv_smul_right {p : ℝ≥0∞} [Fact (1 ≤ p)] (c : ℂ) (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) :
    l1Conv f (c • g) = c • l1Conv f g

Uses 3 · Used by 1

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution

Used byConvolution by a fixed \(\ell^1\) sequence as a bounded operator

TheoremConvolution with zero on the left#✓fully proved

Convolution with 0 on the left is 0.

theorem l1Conv_zero_left {p : ℝ≥0∞} [Fact (1 ≤ p)] (g : ℓ^p(ℤ, ℂ)) :
    l1Conv (p := p) 0 g = 0

Uses 3

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution

TheoremConvolution with zero on the right#✓fully proved

Convolution with 0 on the right is 0.

theorem l1Conv_zero_right {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ)) :
    l1Conv (p := p) f 0 = 0

Uses 3

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution

DefinitionConvolution by a fixed \(\ell^1\) sequence as a bounded operator#✓fully proved

For fixed f ∈ ℓ¹, convolution by f as a bounded operator on ℓ^p.

noncomputable def l1ConvCLMOf {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ)) :
    ℓ^p(ℤ, ℂ) →L[ℂ] ℓ^p(ℤ, ℂ) :=
  ({ toFun := l1Conv f
     map_add' := fun g₁ g₂ => l1Conv_add_right f g₁ g₂
     map_smul' := fun c g => l1Conv_smul_right c f g } :
    ℓ^p(ℤ, ℂ) →ₗ[ℂ] ℓ^p(ℤ, ℂ)).mkContinuous ‖f‖ (fun g => norm_l1Conv_le f g)

Uses 4 · Used by 3

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence · Convolution is additive in the \(\ell^p\) argument · Convolution is homogeneous in the \(\ell^p\) argument · Young's inequality with one \(\ell^1\) factor

Used byConvolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map · Pointwise action of the convolution operator · Operator norm of convolution by \(f\) is at most \(\|f\|_1\)

TheoremPointwise action of the convolution operator#✓fully proved

Pointwise action of the convolution operator.

theorem l1ConvCLMOf_apply {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) : l1ConvCLMOf f g = l1Conv f g

Uses 2

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence · Convolution by a fixed \(\ell^1\) sequence as a bounded operator

TheoremOperator norm of convolution by \(f\) is at most \(\|f\|_1\)#✓fully proved

The operator norm of convolution by f is at most ‖f‖.

theorem norm_l1ConvCLMOf_le {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ)) :
    ‖l1ConvCLMOf (p := p) f‖ ≤ ‖f‖

Uses 2 · Used by 2

Statement usesConvolution by a fixed \(\ell^1\) sequence as a bounded operator

Proof usesYoung's inequality with one \(\ell^1\) factor

Used byConvolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map · Convolution action has operator norm at most 1

DefinitionConvolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map#✓fully proved

The convolution action as a bounded linear map ℓ¹(ℤ, ℂ) →L[ℂ] (ℓ^p(ℤ, ℂ) →L[ℂ] ℓ^p(ℤ, ℂ)).

MathlibExt.Analysis.FunctionalAnalysis.IntConvolution.l1ConvCLM · 15 lines

noncomputable def l1ConvCLM {p : ℝ≥0∞} [Fact (1 ≤ p)] :
    ℓ¹(ℤ, ℂ) →L[ℂ] (ℓ^p(ℤ, ℂ) →L[ℂ] ℓ^p(ℤ, ℂ)) :=
  ({ toFun := l1ConvCLMOf
     map_add' := fun f₁ f₂ => by
        apply ContinuousLinearMap.ext
        intro g
        simp only [l1ConvCLMOf_apply, add_apply]
        exact l1Conv_add_left f₁ f₂ g
     map_smul' := fun c f => by
        apply ContinuousLinearMap.ext
        intro g
        simp only [l1ConvCLMOf_apply, smul_apply]
        exact l1Conv_smul_left c f g } :
    ℓ¹(ℤ, ℂ) →ₗ[ℂ] (ℓ^p(ℤ, ℂ) →L[ℂ] ℓ^p(ℤ, ℂ))).mkContinuous 1
    (fun f => by rw [one_mul]; exact norm_l1ConvCLMOf_le f)

Uses 5 · Used by 2

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence · Convolution by a fixed \(\ell^1\) sequence as a bounded operator · Convolution is additive in the \(\ell^1\) argument · Convolution is homogeneous in the \(\ell^1\) argument · Operator norm of convolution by \(f\) is at most \(\|f\|_1\)

Used byPointwise action of the bundled convolution action · Convolution action has operator norm at most 1

TheoremPointwise action of the bundled convolution action#✓fully proved

Pointwise action of the convolution action.

theorem l1ConvCLM_apply {p : ℝ≥0∞} [Fact (1 ≤ p)] (f : ℓ¹(ℤ, ℂ))
    (g : ℓ^p(ℤ, ℂ)) : l1ConvCLM f g = l1Conv f g

Uses 2

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence · Convolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map

TheoremConvolution action has operator norm at most 1#✓fully proved

The convolution action has operator norm at most 1.

theorem norm_l1ConvCLM_le {p : ℝ≥0∞} [Fact (1 ≤ p)] : ‖l1ConvCLM (p := p)‖ ≤ 1

Uses 2

Statement usesConvolution action of \(\ell^1\) on \(\ell^p\) as a bounded bilinear map

Proof usesOperator norm of convolution by \(f\) is at most \(\|f\|_1\)

TheoremCommutativity of \(\ell^1\) convolution#✓fully proved

Convolution of ℓ¹ sequences is commutative.

theorem l1Conv_comm (f g : ℓ¹(ℤ, ℂ)) : l1Conv f g = l1Conv g f

Uses 3 · Used by 1

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution

Used byUnit sequence is a right identity for \(\ell^1\) convolution

TheoremAssociativity of \(\ell^1\) convolution#✓fully proved

Convolution of ℓ¹ sequences is associative.

theorem l1Conv_assoc (f g h : ℓ¹(ℤ, ℂ)) : l1Conv (l1Conv f g) h = l1Conv f (l1Conv g h)

Uses 5

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution · The \(\ell^1\) norm as a sum of coordinate norms · Coordinate norms of an \(\ell^1\) family are summable

DefinitionUnit sequence in \(\ell^1(\mathbb{Z})\)#✓fully proved

The unit sequence δ at 0 in ℓ¹(ℤ, ℂ).

noncomputable def l1Delta : ℓ¹(ℤ, ℂ) := lp.single (E := fun _ : ℤ => ℂ) 1 0 1

Used by 4

Used byUnit sequence is a left identity for convolution · Unit sequence is a right identity for \(\ell^1\) convolution · Pointwise values of the unit sequence · Norm of the unit sequence is 1

TheoremPointwise values of the unit sequence#✓fully proved

Pointwise values of the unit sequence.

theorem l1Delta_apply (n : ℤ) : l1Delta n = if n = 0 then 1 else 0

Uses 1 · Used by 1

Statement usesUnit sequence in \(\ell^1(\mathbb{Z})\)

Used byUnit sequence is a left identity for convolution

TheoremNorm of the unit sequence is 1#✓fully proved

The norm of the unit sequence is 1.

theorem norm_l1Delta : ‖l1Delta‖ = 1

Uses 1

Statement usesUnit sequence in \(\ell^1(\mathbb{Z})\)

TheoremUnit sequence is a left identity for convolution#✓fully proved

The unit sequence is a left unit for convolution.

theorem l1Conv_delta_left {p : ℝ≥0∞} [Fact (1 ≤ p)] (g : ℓ^p(ℤ, ℂ)) :
    l1Conv l1Delta g = g

Uses 5 · Used by 1

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence · Unit sequence in \(\ell^1(\mathbb{Z})\)

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution · Pointwise values of the unit sequence

Used byUnit sequence is a right identity for \(\ell^1\) convolution

TheoremUnit sequence is a right identity for \(\ell^1\) convolution#✓fully proved

The unit sequence is a right unit for convolution on ℓ¹.

theorem l1Conv_delta_right (f : ℓ¹(ℤ, ℂ)) : l1Conv f l1Delta = f

Uses 4

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence · Unit sequence in \(\ell^1(\mathbb{Z})\)

Proof usesCommutativity of \(\ell^1\) convolution · Unit sequence is a left identity for convolution

TheoremConvolution of coordinate vectors#✓fully proved

Convolution of two coordinate vectors: positions add, coefficients multiply.

theorem l1Conv_single_single {p : ℝ≥0∞} [Fact (1 ≤ p)] (i j : ℤ) (a b : ℂ) :
    l1Conv (lp.single (E := fun _ : ℤ => ℂ) 1 i a)
        (lp.single (E := fun _ : ℤ => ℂ) p j b)
      = lp.single (E := fun _ : ℤ => ℂ) p (i + j) (a * b)

Uses 3

Statement usesConvolution of an \(\ell^1\) sequence with an \(\ell^p\) sequence

Proof usesConvolution of sequences on the integers · Pointwise formula for \(\ell^1\)–\(\ell^p\) convolution

31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.