Composition operators on ℓ²

DefinitionUniformly bounded fibers of a map on the naturals#✓fully proved

The fibers of ψ are finite and uniformly bounded by M: every value is taken at most M times. This is the boundedness hypothesis for the composition operator.

def HasBoundedFibers (ψ : ℕ → ℕ) (M : ℕ) : Prop :=
  ∀ m, (ψ ⁻¹' {m}).Finite ∧ (ψ ⁻¹' {m}).ncard ≤ M

Used by 26

Used byAdjoint of a composition operator is the fiber-sum operator · Bounded composition operator on \(\ell^2\) · Pointwise action of the bounded composition operator · Composition of composition operators · Composition operator of a pointwise identity symbol · Composition operator of the identity is the identity · Composition operator as a linear map · Pointwise action of the composition linear map · Supremum of the fiber counts of a map · Fiber supremum as a supremum of cardinalities · Fiber supremum is nonnegative · Bounded fibers are preserved under composition · Halving map has fibers of size at most two · Permutations have fibers of size one · Injective maps have fibers of size at most one · Composition operator is injective iff its symbol is surjective · Precomposition preserves square-summability · Operator norm of a composition operator · Vectorwise norm bound for the composition operator · Operator-norm bound for the composition operator · Norm of the composition operator on a basis vector · Norm bound for the composition linear map · Squared-norm bound for the composition linear map · Composition operators on \(\ell^2\) are never compact · Composition operator is surjective iff its symbol is injective · Squared-norm sum bound for a precomposed sequence

DefinitionFiber cardinality of a map#✓fully proved

The number of preimages of m under ψ, defined for a finite fiber.

noncomputable def fiberCard (ψ : ℕ → ℕ) (m : ℕ) (hfin : (ψ ⁻¹' {m}).Finite) : ℕ :=
  hfin.toFinset.card

Used by 6

Used byFiber count agrees with set cardinality · Supremum of the fiber counts of a map · Fiber supremum as a supremum of cardinalities · Operator norm of a composition operator · Norm of the composition operator on a basis vector · Composition operators on \(\ell^2\) are never compact

TheoremFiber count agrees with set cardinality#✓fully proved

On its finite domain, the fiber count agrees with the standard natural cardinality.

@[simp] theorem fiberCard_eq_ncard (ψ : ℕ → ℕ) (m : ℕ) (hfin : (ψ ⁻¹' {m}).Finite) :
    fiberCard ψ m hfin = (ψ ⁻¹' {m}).ncard

Uses 1 · Used by 4

Statement usesFiber cardinality of a map

Used byFiber supremum as a supremum of cardinalities · Operator norm of a composition operator · Norm of the composition operator on a basis vector · Composition operators on \(\ell^2\) are never compact

DefinitionSupremum of the fiber counts of a map#✓fully proved

The real supremum of the fiber counts of ψ, defined for uniformly bounded finite fibers. The bound in hψ ensures that the real-valued family is bounded above.

noncomputable def fiberSup (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) : ℝ :=
  ⨆ m, (fiberCard ψ m (hψ m).1 : ℝ)

Uses 2 · Used by 9

Statement usesUniformly bounded fibers of a map on the naturals · Fiber cardinality of a map

Used byBounded composition operator on \(\ell^2\) · Fiber supremum as a supremum of cardinalities · Fiber supremum is nonnegative · Operator norm of a composition operator · Vectorwise norm bound for the composition operator · Operator-norm bound for the composition operator · Norm bound for the composition linear map · Squared-norm bound for the composition linear map · Squared-norm sum bound for a precomposed sequence

TheoremFiber supremum as a supremum of cardinalities#✓fully proved

On its bounded finite domain, the fiber supremum agrees with the supremum of natural cardinalities. Its value is independent of the chosen bound and evidence.

theorem fiberSup_eq_iSup (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    fiberSup ψ hψ = ⨆ m, ((ψ ⁻¹' {m}).ncard : ℝ)

Uses 4 · Used by 3

Statement usesUniformly bounded fibers of a map on the naturals · Supremum of the fiber counts of a map

Proof usesFiber cardinality of a map · Fiber count agrees with set cardinality

Used byFiber supremum is nonnegative · Operator norm of a composition operator · Squared-norm sum bound for a precomposed sequence

DefinitionPrecomposition of a sequence with a map#✓fully proved

The composition function: precompose a sequence with ψ.

def compFun (ψ : ℕ → ℕ) (x : ℕ → 𝕜) (n : ℕ) : 𝕜 := x (ψ n)

Used by 2

Used byComposition operator as a linear map · Precomposition preserves square-summability

TheoremPrecomposition preserves square-summability#✓fully proved

The composed sequence of an ℓ² sequence is in ℓ², under the bounded fibers hypothesis.

theorem memℓp_compFun (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (x : ℓ²(ℕ, 𝕜)) : Memℓp (compFun ψ (x : ℕ → 𝕜)) 2

Uses 2 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Precomposition of a sequence with a map

Used byComposition operator as a linear map

TheoremSquared-norm sum bound for a precomposed sequence#✓fully proved

The squared-norm sum of the composed sequence is at most fiberSup ψ hψ times the squared-norm sum of the original sequence.

theorem tsum_compFun_norm_sq_le (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (x : ℓ²(ℕ, 𝕜)) :
    ∑' n, ‖(x : ℕ → 𝕜) (ψ n)‖ ^ (2 : ℝ)
      ≤ fiberSup ψ hψ * ∑' m, ‖(x : ℕ → 𝕜) m‖ ^ (2 : ℝ)

Uses 3 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Supremum of the fiber counts of a map

Proof usesFiber supremum as a supremum of cardinalities

Used bySquared-norm bound for the composition linear map

DefinitionComposition operator as a linear map#✓fully proved

The composition operator as a linear map.

noncomputable def compLinMap (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun x := ⟨compFun ψ (x : ℕ → 𝕜), memℓp_compFun ψ hψ x⟩
  map_add' x y := by
    apply lp.ext
    funext i
    simp only [compFun, lp.coeFn_add, Pi.add_apply]
  map_smul' c x := by
    apply lp.ext
    funext i
    simp only [compFun, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, RingHom.id_apply]

Uses 3 · Used by 5

Statement usesUniformly bounded fibers of a map on the naturals · Precomposition of a sequence with a map · Precomposition preserves square-summability

Used byBounded composition operator on \(\ell^2\) · Pointwise action of the composition linear map · Operator-norm bound for the composition operator · Norm bound for the composition linear map · Squared-norm bound for the composition linear map

TheoremPointwise action of the composition linear map#✓fully proved

Pointwise action of the composition linear map.

theorem compLinMap_apply (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (x : ℓ²(ℕ, 𝕜)) (i : ℕ) : compLinMap ψ hψ x i = (x : ℕ → 𝕜) (ψ i)

Uses 2 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Composition operator as a linear map

Used bySquared-norm bound for the composition linear map

TheoremSquared-norm bound for the composition linear map#✓fully proved

The squared norm of C_ψ x is at most fiberSup ψ hψ * ‖x‖².

theorem norm_sq_compLinMap_apply_le (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (x : ℓ²(ℕ, 𝕜)) :
    ‖compLinMap ψ hψ x‖ ^ (2 : ℝ) ≤ fiberSup ψ hψ * ‖x‖ ^ (2 : ℝ)

Uses 5 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Composition operator as a linear map · Supremum of the fiber counts of a map

Proof usesPointwise action of the composition linear map · Squared-norm sum bound for a precomposed sequence

Used byNorm bound for the composition linear map

TheoremFiber supremum is nonnegative#✓fully proved

fiberSup ψ hψ is nonnegative.

theorem fiberSup_nonneg (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    0 ≤ fiberSup ψ hψ

Uses 3 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Supremum of the fiber counts of a map

Proof usesFiber supremum as a supremum of cardinalities

Used byNorm bound for the composition linear map

TheoremNorm bound for the composition linear map#✓fully proved

The composition operator is bounded by √(fiberSup ψ hψ).

theorem norm_compLinMap_apply_le (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (x : ℓ²(ℕ, 𝕜)) :
    ‖compLinMap ψ hψ x‖ ≤ Real.sqrt (fiberSup ψ hψ) * ‖x‖

Uses 5 · Used by 3

Statement usesUniformly bounded fibers of a map on the naturals · Composition operator as a linear map · Supremum of the fiber counts of a map

Proof usesFiber supremum is nonnegative · Squared-norm bound for the composition linear map

Used byBounded composition operator on \(\ell^2\) · Vectorwise norm bound for the composition operator · Operator-norm bound for the composition operator

DefinitionBounded composition operator on \(\ell^2\)#✓fully proved

The composition operator as a bounded operator on ℓ²(ℕ, 𝕜).

noncomputable def compCLM (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  (compLinMap ψ hψ).mkContinuous (Real.sqrt (fiberSup ψ hψ))
    (norm_compLinMap_apply_le ψ hψ)

Uses 4 · Used by 14

Statement usesUniformly bounded fibers of a map on the naturals · Composition operator as a linear map · Supremum of the fiber counts of a map · Norm bound for the composition linear map

Used byAdjoint of a composition operator is the fiber-sum operator · Adjoint of a composition operator with a permutation symbol · Pointwise action of the bounded composition operator · Composition of composition operators · Composition operator of a pointwise identity symbol · Composition operator of the identity is the identity · Permutation composition operators are unitary · Composition operator is injective iff its symbol is surjective · Operator norm of a composition operator · Vectorwise norm bound for the composition operator · Operator-norm bound for the composition operator · Norm of the composition operator on a basis vector · Composition operators on \(\ell^2\) are never compact · Composition operator is surjective iff its symbol is injective

TheoremPointwise action of the bounded composition operator#✓fully proved

Pointwise action of the composition operator.

theorem compCLM_apply (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (x : ℓ²(ℕ, 𝕜)) (i : ℕ) : compCLM (𝕜 := 𝕜) ψ hψ x i = (x : ℕ → 𝕜) (ψ i)

Uses 2 · Used by 5

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Used byAdjoint of a composition operator is the fiber-sum operator · Adjoint of a composition operator with a permutation symbol · Composition operator is injective iff its symbol is surjective · Norm of the composition operator on a basis vector · Composition operator is surjective iff its symbol is injective

TheoremVectorwise norm bound for the composition operator#✓fully proved

The composition operator is bounded by √(fiberSup ψ hψ) on every vector.

theorem norm_compCLM_apply_le (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (x : ℓ²(ℕ, 𝕜)) :
    ‖compCLM (𝕜 := 𝕜) ψ hψ x‖ ≤ Real.sqrt (fiberSup ψ hψ) * ‖x‖

Uses 4

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\) · Supremum of the fiber counts of a map

Proof usesNorm bound for the composition linear map

TheoremOperator-norm bound for the composition operator#✓fully proved

The operator norm of C_ψ is at most √(fiberSup ψ hψ).

theorem norm_compCLM_le (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    ‖compCLM (𝕜 := 𝕜) ψ hψ‖ ≤ Real.sqrt (fiberSup ψ hψ)

Uses 5 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\) · Supremum of the fiber counts of a map

Proof usesComposition operator as a linear map · Norm bound for the composition linear map

Used byOperator norm of a composition operator

TheoremNorm of the composition operator on a basis vector#✓fully proved

The norm of C_ψ applied to a standard basis vector is the square root of the corresponding fiber count.

theorem norm_compCLM_single (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) (m : ℕ) :
    ‖compCLM (𝕜 := 𝕜) ψ hψ (lp.single 2 m (1 : 𝕜))‖ =
      Real.sqrt (fiberCard ψ m (hψ m).1 : ℝ)

Uses 5 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\) · Fiber cardinality of a map

Proof usesPointwise action of the bounded composition operator · Fiber count agrees with set cardinality

Used byOperator norm of a composition operator

TheoremOperator norm of a composition operator#✓fully proved

The operator norm of the composition operator: ‖C_ψ‖ = √(fiberSup ψ hψ), the square root of the largest fiber count.

theorem norm_compCLM (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    ‖compCLM (𝕜 := 𝕜) ψ hψ‖ = Real.sqrt (fiberSup ψ hψ)

Uses 8

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\) · Supremum of the fiber counts of a map

Proof usesFiber cardinality of a map · Fiber count agrees with set cardinality · Fiber supremum as a supremum of cardinalities · Operator-norm bound for the composition operator · Norm of the composition operator on a basis vector

TheoremAdjoint of a composition operator is the fiber-sum operator#✓fully proved

The adjoint of the composition operator is the fiber-sum operator: ((C_ψ)† y) m is the sum of y over the fiber of m.

theorem adjoint_compCLM_apply (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (y : ℓ²(ℕ, 𝕜)) (m : ℕ) :
    (((compCLM (𝕜 := 𝕜) ψ hψ)†) y) m
      = ∑ n ∈ Set.Finite.toFinset (hψ m).1, (y : ℕ → 𝕜) n

Uses 3 · Used by 2

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Proof usesPointwise action of the bounded composition operator

Used byAdjoint of a composition operator with a permutation symbol · Composition operator is surjective iff its symbol is injective

TheoremBounded fibers are preserved under composition#✓fully proved

Fiber bounds compose: the fibers of ψ ∘ φ are bounded by the product of the bounds.

theorem hasBoundedFibers_comp {φ ψ : ℕ → ℕ} {Mφ Mψ : ℕ}
    (hφ : HasBoundedFibers φ Mφ) (hψ : HasBoundedFibers ψ Mψ) :
    HasBoundedFibers (ψ ∘ φ) (Mψ * Mφ)

Uses 1 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals

Used byPermutation composition operators are unitary

TheoremComposition of composition operators#✓fully proved

Composition of composition operators is composition of symbols in the reversed order: C_φ ∘L C_ψ = C_{ψ ∘ φ}.

theorem compCLM_comp {φ ψ : ℕ → ℕ} {Mφ Mψ : ℕ}
    (hφ : HasBoundedFibers φ Mφ) (hψ : HasBoundedFibers ψ Mψ)
    (h : HasBoundedFibers (ψ ∘ φ) (Mψ * Mφ)) :
    compCLM (𝕜 := 𝕜) φ hφ ∘L compCLM (𝕜 := 𝕜) ψ hψ = compCLM (𝕜 := 𝕜) (ψ ∘ φ) h

Uses 2 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Used byPermutation composition operators are unitary

TheoremComposition operator of a pointwise identity symbol#✓fully proved

If ψ is pointwise the identity, C_ψ is the identity operator.

theorem compCLM_eq_of_forall {ψ : ℕ → ℕ} {M : ℕ} (hψ : HasBoundedFibers ψ M)
    (h : ∀ n, ψ n = n) : compCLM (𝕜 := 𝕜) ψ hψ = 1

Uses 2 · Used by 2

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Used byComposition operator of the identity is the identity · Permutation composition operators are unitary

TheoremComposition operator of the identity is the identity#✓fully proved

C_id is the identity operator.

theorem compCLM_id {M : ℕ} (h : HasBoundedFibers id M) : compCLM (𝕜 := 𝕜) id h = 1

Uses 3

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Proof usesComposition operator of a pointwise identity symbol

TheoremInjective maps have fibers of size at most one#✓fully proved

An injective symbol has fibers of size at most one.

theorem hasBoundedFibers_of_injective {ψ : ℕ → ℕ} (hψ : Function.Injective ψ) :
    HasBoundedFibers ψ 1

Uses 1 · Used by 1

Statement usesUniformly bounded fibers of a map on the naturals

Used byPermutations have fibers of size one

TheoremPermutations have fibers of size one#✓fully proved

A permutation symbol has fibers of size one.

theorem hasBoundedFibers_equiv (e : ℕ ≃ ℕ) : HasBoundedFibers e 1

Uses 2 · Used by 2

Statement usesUniformly bounded fibers of a map on the naturals

Proof usesInjective maps have fibers of size at most one

Used byAdjoint of a composition operator with a permutation symbol · Permutation composition operators are unitary

TheoremAdjoint of a composition operator with a permutation symbol#✓fully proved

The adjoint of the composition operator for a permutation symbol is the composition operator of the inverse permutation.

theorem adjoint_compCLM_of_equiv (e : ℕ ≃ ℕ) :
    (compCLM (𝕜 := 𝕜) e (hasBoundedFibers_equiv e))†
      = compCLM (𝕜 := 𝕜) e.symm (hasBoundedFibers_equiv e.symm)

Uses 4 · Used by 1

Statement usesBounded composition operator on \(\ell^2\) · Permutations have fibers of size one

Proof usesAdjoint of a composition operator is the fiber-sum operator · Pointwise action of the bounded composition operator

Used byPermutation composition operators are unitary

TheoremPermutation composition operators are unitary#✓fully proved

A permutation symbol gives a unitary composition operator.

theorem compCLM_mem_unitary (e : ℕ ≃ ℕ) :
    compCLM (𝕜 := 𝕜) e (hasBoundedFibers_equiv e)
      ∈ unitary (ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))

Uses 6

Statement usesBounded composition operator on \(\ell^2\) · Permutations have fibers of size one

Proof usesAdjoint of a composition operator with a permutation symbol · Composition of composition operators · Composition operator of a pointwise identity symbol · Bounded fibers are preserved under composition

TheoremComposition operator is injective iff its symbol is surjective#✓fully proved

C_ψ is injective iff ψ is surjective: a missing value gives a basis vector in the kernel, and a surjective symbol lets every coordinate be read off from the image.

theorem injective_compCLM_iff (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    Function.Injective (compCLM (𝕜 := 𝕜) ψ hψ) ↔ Function.Surjective ψ

Uses 3

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Proof usesPointwise action of the bounded composition operator

TheoremComposition operator is surjective iff its symbol is injective#✓fully proved

C_ψ is surjective iff ψ is injective: if ψ a = ψ b with a ≠ b, the a-th and b-th coordinates of every vector in the range agree, so e_a is not in the range; if ψ is injective, the preimage of y is obtained by applying the adjoint and reading off the fiber sums.

theorem surjective_compCLM_iff (ψ : ℕ → ℕ) {M : ℕ} (hψ : HasBoundedFibers ψ M) :
    Function.Surjective (compCLM (𝕜 := 𝕜) ψ hψ) ↔ Function.Injective ψ

Uses 4

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Proof usesAdjoint of a composition operator is the fiber-sum operator · Pointwise action of the bounded composition operator

TheoremHalving map has fibers of size at most two#✓fully proved

Halving pairs: the map n ↦ n / 2 has fibers of size at most two.

theorem hasBoundedFibers_div_two : HasBoundedFibers (fun n => n / 2) 2

Uses 1

Statement usesUniformly bounded fibers of a map on the naturals

TheoremComposition operators on \(\ell^2\) are never compact#✓fully proved

A composition operator on ℓ²(ℕ, 𝕜) is never compact: the images of the basis vectors indexed by the (necessarily infinite) range of ψ are pairwise orthogonal and bounded below in norm, so they have no Cauchy subsequence.

theorem not_isCompactOperator_compCLM (ψ : ℕ → ℕ) {M : ℕ}
    (hψ : HasBoundedFibers ψ M) :
    ¬ IsCompactOperator (compCLM (𝕜 := 𝕜) ψ hψ)

Uses 4

Statement usesUniformly bounded fibers of a map on the naturals · Bounded composition operator on \(\ell^2\)

Proof usesFiber cardinality of a map · Fiber count agrees with set cardinality

32 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.