Rolewicz backward shifts

TheoremPowers of the forward shift preserve norms#✓fully proved

Powers of the forward shift preserve norms.

theorem norm_forwardShiftCLM_pow_apply (n : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    ‖(LpShiftOperator.shiftCLM ^ n) x‖ = ‖x‖

Uses 2 · Used by 3

Statement usesThe unilateral shift operator

Proof usesThe unilateral shift preserves norms

Used byRolewicz's theorem · Distance from the periodic approximant to the truncation · Norm of a term of the periodic approximant

TheoremPowers of the backward shift do not increase norms#✓fully proved

Powers of the backward shift do not increase norms.

theorem norm_backwardShiftCLM_pow_apply_le (n : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    ‖(LpShiftOperator.backwardCLM ^ n) x‖ ≤ ‖x‖

Uses 2 · Used by 1

Statement usesBackward shift

Proof usesThe backward shift linear map does not increase norms

Used byRolewicz's theorem

TheoremPowers of a scalar multiple of the backward shift#✓fully proved

Powers of a scalar multiple of the backward shift, applied pointwise.

theorem smul_backwardShiftCLM_pow_apply (μ : 𝕜) (n : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    (((μ • LpShiftOperator.backwardCLM) ^ n) x) = μ ^ n • (LpShiftOperator.backwardCLM ^ n) x

Uses 1 · Used by 3

Statement usesBackward shift

Used byRolewicz's theorem · Powers of a scaled backward shift as operators · Coordinates of powers of a scaled backward shift

TheoremFinitely supported vectors are dense in \(\ell^2(\mathbb{N})\)#✓fully proved

The span of the single-coordinate vectors is dense in ℓ²(ℕ, 𝕜): every vector is the sum of its canonical series.

theorem dense_span_single :
    Dense (↑(Submodule.span 𝕜
      (Set.range fun i => (lp.single 2 i (1 : 𝕜) : ℓ²(ℕ, 𝕜)))) : Set (ℓ²(ℕ, 𝕜)))

Used by 1

Used byRolewicz's theorem

TheoremVectors in the span of coordinate vectors have finite support#✓fully proved

Every vector in the span of the single-coordinate vectors is eventually zero: it has finite support.

theorem exists_forall_eq_zero_of_mem_span_single {x : ℓ²(ℕ, 𝕜)}
    (hx : x ∈ Submodule.span 𝕜 (Set.range fun i => lp.single 2 i (1 : 𝕜))) :
    ∃ N, ∀ i, N ≤ i → (x : ℕ → 𝕜) i = 0

Used by 1

Used byRolewicz's theorem

TheoremRolewicz's theorem#✓fully proved

The scalar multiple μ • B of the backward shift on ℓ²(ℕ, 𝕜) is hypercyclic if and only if ‖μ‖ > 1.

theorem isHypercyclic_smul_backwardShiftCLM_iff (μ : 𝕜) :
    IsHypercyclic ((μ • LpShiftOperator.backwardCLM : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))) ↔ 1 < ‖μ‖

Uses 12

Statement usesHypercyclic operator · Backward shift

Proof usesHypercyclicity criterion · Finitely supported vectors are dense in \(\ell^2(\mathbb{N})\) · Vectors in the span of coordinate vectors have finite support · Powers of the backward shift do not increase norms · Powers of the forward shift preserve norms · Powers of a scalar multiple of the backward shift · The unilateral shift operator · A Hilbert space with a countable orthonormal basis is separable · Pointwise action of a power of the backward shift · Backward shift power is a left inverse of the shift power

TheoremCoordinates of powers of a scaled backward shift#✓fully proved

Coordinate form of a power of a scalar multiple of the backward shift.

theorem smul_backwardCLM_pow_apply_coord (μ : 𝕜) (n : ℕ) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    (((μ • backwardCLM) ^ n) x) i = μ ^ n * (x : ℕ → 𝕜) (i + n)

Uses 3 · Used by 1

Statement usesBackward shift

Proof usesPowers of a scalar multiple of the backward shift · Pointwise action of a power of the backward shift

Used byCoordinate recurrence for periodic points of \(\mu B\)

TheoremPowers of a scaled backward shift as operators#✓fully proved

A power of a scalar multiple of the backward shift, as an operator.

theorem smul_backwardCLM_pow (μ : 𝕜) (n : ℕ) :
    (μ • backwardCLM (𝕜 := 𝕜)) ^ n = μ ^ n • (backwardCLM (𝕜 := 𝕜) ^ n)

Uses 2 · Used by 1

Statement usesBackward shift

Proof usesPowers of a scalar multiple of the backward shift

Used byAction of the scaled backward shift power on approximant terms

TheoremZero is a periodic point of every operator#✓fully proved

0 is a periodic point of every period for every operator.

theorem isPeriodicPoint_zero (T : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)) (n : ℕ) :
    Function.IsPeriodicPt (⇑T) n 0

Used by 1

Used byPeriodic points of \(\mu B\) are dense iff \(|\mu| > 1\)

DefinitionPeriodic approximant of a truncated sequence#✓fully proved

The periodic extension of the truncation of y to its first N coordinates: the geometric series over forward shifts by blocks of length N, with coefficients (μ⁻¹ ^ N) ^ m.

noncomputable def periodicApprox (μ : 𝕜) (N : ℕ) (y : ℓ²(ℕ, 𝕜)) : ℓ²(ℕ, 𝕜) :=
  ∑' m : ℕ, (μ⁻¹ ^ N) ^ m • ((shiftCLM ^ N) ^ m) (lpTrunc 2 N y)

Uses 2 · Used by 3

Statement usesThe unilateral shift operator · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Used byDense periodic points of the Rolewicz operator for \(|\mu| > 1\) · Distance from the periodic approximant to the truncation · Periodic approximant is a periodic point

TheoremGeometric ratio of the periodic approximant is below 1#✓fully proved

The geometric ratio ‖μ⁻¹ ^ N‖ is < 1 when ‖μ‖ > 1 and N > 0.

theorem norm_inv_pow_lt_one {μ : 𝕜} (hμ : 1 < ‖μ‖) {N : ℕ} (hN : 0 < N) :
    ‖μ⁻¹ ^ N‖ < 1

Used by 2

Used byDistance from the periodic approximant to the truncation · Summability of the geometric bound for periodic approximants

TheoremSummability of the geometric bound for periodic approximants#✓fully proved

The geometric series bounding the periodic approximant terms is summable.

theorem summable_geom_trunc {μ : 𝕜} (hμ : 1 < ‖μ‖) {N : ℕ} (hN : 0 < N) (y : ℓ²(ℕ, 𝕜)) :
    Summable (fun m => ‖μ⁻¹ ^ N‖ ^ m * ‖lpTrunc 2 N y‖)

Uses 2 · Used by 2

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesGeometric ratio of the periodic approximant is below 1

Used bySummability of the shifted periodic approximant terms · Summability of the periodic approximant terms

TheoremNorm of a term of the periodic approximant#✓fully proved

The norm of a term of the periodic approximant.

theorem norm_periodicApprox_term (μ : 𝕜) (N m : ℕ) (y : ℓ²(ℕ, 𝕜)) :
    ‖(μ⁻¹ ^ N) ^ m • ((shiftCLM ^ N) ^ m) (lpTrunc 2 N y)‖ =
      ‖μ⁻¹ ^ N‖ ^ m * ‖lpTrunc 2 N y‖

Uses 3 · Used by 2

Statement usesThe unilateral shift operator · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesPowers of the forward shift preserve norms

Used bySummability of the shifted periodic approximant terms · Summability of the periodic approximant terms

TheoremSummability of the periodic approximant terms#✓fully proved

Summability of the terms of the periodic approximant.

theorem summable_periodicApprox_terms {μ : 𝕜} (hμ : 1 < ‖μ‖) {N : ℕ} (hN : 0 < N)
    (y : ℓ²(ℕ, 𝕜)) :
    Summable (fun m => (μ⁻¹ ^ N) ^ m • ((shiftCLM ^ N) ^ m) (lpTrunc 2 N y))

Uses 4 · Used by 2

Statement usesThe unilateral shift operator · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesNorm of a term of the periodic approximant · Summability of the geometric bound for periodic approximants

Used byDistance from the periodic approximant to the truncation · Periodic approximant is a periodic point

TheoremFirst term of the periodic approximant is the truncation#✓fully proved

The m = 0 term of the periodic approximant is the truncation.

theorem periodicApprox_term_zero (μ : 𝕜) (N : ℕ) (y : ℓ²(ℕ, 𝕜)) :
    (μ⁻¹ ^ N) ^ 0 • ((shiftCLM ^ N) ^ 0) (lpTrunc 2 N y) = lpTrunc 2 N y

Uses 2 · Used by 1

Statement usesThe unilateral shift operator · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Used byDistance from the periodic approximant to the truncation

TheoremBackward shift annihilates truncations after \(N\) steps#✓fully proved

Applying the backward shift N times to a truncation gives 0.

theorem backwardCLM_pow_trunc (N : ℕ) (y : ℓ²(ℕ, 𝕜)) :
    (backwardCLM ^ N) (lpTrunc 2 N y) = 0

Uses 4 · Used by 1

Statement usesBackward shift · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesPointwise action of a power of the backward shift · Pointwise action of \(\ell^p\) truncation

Used byAction of the scaled backward shift power on approximant terms

TheoremAction of the scaled backward shift power on approximant terms#✓fully proved

How (μ • B) ^ N acts on a term of the periodic approximant: the m = 0 term is killed, and every later term shifts down by one.

theorem periodicApprox_step {μ : 𝕜} (hμ : 1 < ‖μ‖) {N : ℕ}
    (y : ℓ²(ℕ, 𝕜)) (m : ℕ) : ((μ • backwardCLM) ^ N)
      ((μ⁻¹ ^ N) ^ m • ((shiftCLM ^ N) ^ m) (lpTrunc 2 N y)) =
    if m = 0 then 0 else (μ⁻¹ ^ N) ^ (m - 1) • ((shiftCLM ^ N) ^ (m - 1)) (lpTrunc 2 N y)

Uses 6 · Used by 1

Statement usesBackward shift · The unilateral shift operator · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesBackward shift annihilates truncations after \(N\) steps · Powers of a scaled backward shift as operators · Backward shift power is a left inverse of the shift power

Used byPeriodic approximant is a periodic point

TheoremSummability of the shifted periodic approximant terms#✓fully proved

Summability of the terms of the periodic approximant after applying (μ • B) ^ N.

theorem summable_periodicApprox_map {μ : 𝕜} (hμ : 1 < ‖μ‖) {N : ℕ} (hN : 0 < N)
    (y : ℓ²(ℕ, 𝕜)) : Summable (fun m => ((μ • backwardCLM) ^ N)
      ((μ⁻¹ ^ N) ^ m • ((shiftCLM ^ N) ^ m) (lpTrunc 2 N y)))

Uses 5 · Used by 1

Statement usesBackward shift · The unilateral shift operator · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesNorm of a term of the periodic approximant · Summability of the geometric bound for periodic approximants

Used byPeriodic approximant is a periodic point

TheoremPeriodic approximant is a periodic point#✓fully proved

The periodic approximant is periodic of period N when ‖μ‖ > 1.

theorem periodicApprox_isPeriodicPoint {μ : 𝕜} (hμ : 1 < ‖μ‖) {N : ℕ} (hN : 0 < N)
    (y : ℓ²(ℕ, 𝕜)) : Function.IsPeriodicPt (⇑(μ • backwardCLM)) N (periodicApprox μ N y)

Uses 7 · Used by 1

Statement usesPeriodic approximant of a truncated sequence · Backward shift

Proof usesAction of the scaled backward shift power on approximant terms · Summability of the shifted periodic approximant terms · Summability of the periodic approximant terms · The unilateral shift operator · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Used byDense periodic points of the Rolewicz operator for \(|\mu| > 1\)

TheoremDistance from the periodic approximant to the truncation#✓fully proved

The distance from the periodic approximant to the truncation is at most the geometric tail (r / (1 - r)) * ‖y‖, where r = ‖μ‖⁻¹ ^ N.

theorem norm_periodicApprox_sub_trunc {μ : 𝕜} (hμ : 1 < ‖μ‖) {N : ℕ} (hN : 0 < N)
    (y : ℓ²(ℕ, 𝕜)) :
    ‖periodicApprox μ N y - lpTrunc 2 N y‖ ≤
      (‖μ‖⁻¹ ^ N / (1 - ‖μ‖⁻¹ ^ N)) * ‖y‖

Uses 8 · Used by 1

Statement usesPeriodic approximant of a truncated sequence · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesPowers of the forward shift preserve norms · Geometric ratio of the periodic approximant is below 1 · First term of the periodic approximant is the truncation · Summability of the periodic approximant terms · The unilateral shift operator · Truncation is a contraction on \(\ell^p\)

Used byDense periodic points of the Rolewicz operator for \(|\mu| > 1\)

TheoremDense periodic points of the Rolewicz operator for \(|\mu| > 1\)#✓fully proved

The periodic points of μ • B are dense when ‖μ‖ > 1.

theorem dense_periodicPoints_of_one_lt_norm {μ : 𝕜} (hμ : 1 < ‖μ‖) :
    Dense (Function.periodicPts (⇑(μ • backwardCLM (𝕜 := 𝕜))))

Uses 6 · Used by 1

Statement usesBackward shift

Proof usesDistance from the periodic approximant to the truncation · Periodic approximant of a truncated sequence · Periodic approximant is a periodic point · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates · Truncations of an \(\ell^p\) vector converge to it

Used byPeriodic points of \(\mu B\) are dense iff \(|\mu| > 1\)

TheoremCoordinate recurrence for periodic points of \(\mu B\)#✓fully proved

If x is periodic for μ • B, its coordinates satisfy x k = μ ^ (n * m) * x (k + n * m) for all m.

theorem periodic_coord_iterate {μ : 𝕜} {n : ℕ} {x : ℓ²(ℕ, 𝕜)}
    (hx : Function.IsPeriodicPt (⇑(μ • backwardCLM)) n x) (k : ℕ) (m : ℕ) :
    (x : ℕ → 𝕜) k = μ ^ (n * m) * (x : ℕ → 𝕜) (k + n * m)

Uses 2 · Used by 1

Statement usesBackward shift

Proof usesCoordinates of powers of a scaled backward shift

Used byNo nonzero periodic points of \(\mu B\) when \(|\mu| \le 1\)

TheoremCoordinates of an \(\ell^2\) vector tend to zero#✓fully proved

The coordinates of an ℓ² vector tend to 0.

theorem tendsto_norm_coord (x : ℓ²(ℕ, 𝕜)) :
    Tendsto (fun j => ‖(x : ℕ → 𝕜) j‖) atTop (𝓝 0)

Used by 1

Used byNo nonzero periodic points of \(\mu B\) when \(|\mu| \le 1\)

TheoremNo nonzero periodic points of \(\mu B\) when \(|\mu| \le 1\)#✓fully proved

The only periodic point of μ • B is 0 when ‖μ‖ ≤ 1.

theorem eq_zero_of_isPeriodicPoint_of_norm_le_one {μ : 𝕜} (hμ : ‖μ‖ ≤ 1) {n : ℕ} (hn : 0 < n)
    {x : ℓ²(ℕ, 𝕜)} (hx : Function.IsPeriodicPt (⇑(μ • backwardCLM)) n x) : x = 0

Uses 3 · Used by 1

Statement usesBackward shift

Proof usesCoordinate recurrence for periodic points of \(\mu B\) · Coordinates of an \(\ell^2\) vector tend to zero

Used byPeriodic points of \(\mu B\) are dense iff \(|\mu| > 1\)

TheoremPeriodic points of \(\mu B\) are dense iff \(|\mu| > 1\)#✓fully proved

The periodic points of μ • B are dense if and only if ‖μ‖ > 1.

theorem dense_periodicPoints_iff (μ : 𝕜) :
    Dense (Function.periodicPts (⇑(μ • backwardCLM (𝕜 := 𝕜)))) ↔
      1 < ‖μ‖

Uses 4

Statement usesBackward shift

Proof usesDense periodic points of the Rolewicz operator for \(|\mu| > 1\) · No nonzero periodic points of \(\mu B\) when \(|\mu| \le 1\) · Zero is a periodic point of every operator

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.