Hankel operators

DefinitionAnti-diagonal slice of a sequence#✓fully proved

The k-th anti-diagonal slice function: reverse the first k + 1 coordinates, kill the rest.

def hankelSliceFun (k : ℕ) (x : ℕ → 𝕜) (i : ℕ) : 𝕜 :=
  if i ≤ k then x (k - i) else 0

Used by 8

Used byPartial sums of the Hankel slice series are compact · Anti-diagonal slice of an ℓ² sequence lies in ℓ² · Matrix entries of the Hankel operator · Pointwise action of the anti-diagonal slice operator · Anti-diagonal slice is symmetric · Anti-diagonal slice as a linear map · Pointwise action of the anti-diagonal slice map · Anti-diagonal slice does not increase the sum of squared norms

TheoremAnti-diagonal slice of an ℓ² sequence lies in ℓ²#✓fully proved

The slice of an ℓ² sequence is in ℓ².

theorem hankel_memℓp_sliceFun {k : ℕ} {x : ℓ²(ℕ, 𝕜)} :
    Memℓp (hankelSliceFun k (x : ℕ → 𝕜)) 2

Uses 1 · Used by 1

Statement usesAnti-diagonal slice of a sequence

Used byAnti-diagonal slice as a linear map

DefinitionAnti-diagonal slice as a linear map#✓fully proved

The k-th anti-diagonal slice as a linear map.

noncomputable def hankelSliceLinMap (k : ℕ) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun x := ⟨hankelSliceFun k (x : ℕ → 𝕜), hankel_memℓp_sliceFun⟩
  map_add' x y := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_add, Pi.add_apply, hankelSliceFun_apply]
    split_ifs with hi <;> simp
  map_smul' c x := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, hankelSliceFun_apply,
      RingHom.id_apply]
    split_ifs with hi <;> simp

Uses 2 · Used by 3

Statement usesAnti-diagonal slice of a sequence · Anti-diagonal slice of an ℓ² sequence lies in ℓ²

Used byAnti-diagonal slice operator · Pointwise action of the anti-diagonal slice map · Anti-diagonal slice map does not increase norms

TheoremPointwise action of the anti-diagonal slice map#✓fully proved

Pointwise action of the slice linear map.

theorem hankelSliceLinMap_apply (k : ℕ) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    hankelSliceLinMap k x i = hankelSliceFun k (x : ℕ → 𝕜) i

Uses 2

Statement usesAnti-diagonal slice of a sequence · Anti-diagonal slice as a linear map

TheoremAnti-diagonal slice does not increase the sum of squared norms#✓fully proved

The (squared) norms of a sliced sequence sum to at most the squared norms of the original sequence: only the first k + 1 coordinates survive, in reverse order.

theorem hankel_tsum_normSq_slice_le {k : ℕ} (x : ℓ²(ℕ, 𝕜)) :
    ∑' i, ‖hankelSliceFun k (x : ℕ → 𝕜) i‖ ^ 2 ≤ ∑' i, ‖(x : ℕ → 𝕜) i‖ ^ 2

Uses 1 · Used by 1

Statement usesAnti-diagonal slice of a sequence

Used byAnti-diagonal slice map does not increase norms

TheoremAnti-diagonal slice map does not increase norms#✓fully proved

A slice does not increase norms.

theorem norm_hankelSliceLinMap_apply_le (k : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    ‖hankelSliceLinMap k x‖ ≤ ‖x‖

Uses 2 · Used by 2

Statement usesAnti-diagonal slice as a linear map

Proof usesAnti-diagonal slice does not increase the sum of squared norms

Used byAnti-diagonal slice operator · Anti-diagonal slice operator has norm at most one

DefinitionAnti-diagonal slice operator#✓fully proved

The k-th anti-diagonal slice as a bounded operator.

noncomputable def hankelSlice (k : ℕ) : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  (hankelSliceLinMap k).mkContinuous 1 (fun x => by
    rw [one_mul]
    exact norm_hankelSliceLinMap_apply_le k x)

Uses 2 · Used by 14

Statement usesAnti-diagonal slice as a linear map · Anti-diagonal slice map does not increase norms

Used byAdjoint of a Hankel operator · Anti-diagonal slice operator is self-adjoint · Hankel operator as the sum of its slices · Partial sums of the Hankel slice series are compact · Hankel operator with absolutely summable symbol · Matrix entries of the Hankel operator · Hankel operator with zero symbol is zero · Pointwise action of the anti-diagonal slice operator · Anti-diagonal slice is symmetric · Summability of weighted anti-diagonal slices · Hankel operator with absolutely summable symbol is compact · Hankel operator with real symbol is self-adjoint · Norm bound for the Hankel operator · Anti-diagonal slice operator has norm at most one

TheoremPointwise action of the anti-diagonal slice operator#✓fully proved

Pointwise action of the slice operator.

theorem hankelSlice_apply (k : ℕ) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    hankelSlice k x i = hankelSliceFun k (x : ℕ → 𝕜) i

Uses 2 · Used by 2

Statement usesAnti-diagonal slice operator · Anti-diagonal slice of a sequence

Used byPartial sums of the Hankel slice series are compact · Anti-diagonal slice is symmetric

TheoremAnti-diagonal slice operator has norm at most one#✓fully proved

The operator norm of a slice is at most 1.

theorem norm_hankelSlice_le (k : ℕ) : ‖hankelSlice (𝕜 := 𝕜) k‖ ≤ 1

Uses 2 · Used by 3

Statement usesAnti-diagonal slice operator

Proof usesAnti-diagonal slice map does not increase norms

Used byMatrix entries of the Hankel operator · Summability of weighted anti-diagonal slices · Norm bound for the Hankel operator

TheoremAnti-diagonal slice is symmetric#✓fully proved

A slice is symmetric for the inner product: the anti-diagonal symmetry is a finite-sum reflection.

theorem hankelSlice_inner_symm (k : ℕ) (x y : ℓ²(ℕ, 𝕜)) :
    ⟪hankelSlice k x, y⟫_𝕜 = ⟪x, hankelSlice k y⟫_𝕜

Uses 3 · Used by 1

Statement usesAnti-diagonal slice operator

Proof usesAnti-diagonal slice of a sequence · Pointwise action of the anti-diagonal slice operator

Used byAnti-diagonal slice operator is self-adjoint

TheoremAnti-diagonal slice operator is self-adjoint#✓fully proved

A slice is self-adjoint.

theorem adjoint_hankelSlice (k : ℕ) :
    (hankelSlice (𝕜 := 𝕜) k)† = hankelSlice (𝕜 := 𝕜) k

Uses 2 · Used by 1

Statement usesAnti-diagonal slice operator

Proof usesAnti-diagonal slice is symmetric

Used byAdjoint of a Hankel operator

TheoremSummability of weighted anti-diagonal slices#✓fully proved

The slice operators weighted by a are summable in operator norm when a is absolutely summable.

theorem hankel_summable_slices {a : ℕ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    Summable fun k => (a k) • hankelSlice (𝕜 := 𝕜) k

Uses 2 · Used by 1

Statement usesAnti-diagonal slice operator

Proof usesAnti-diagonal slice operator has norm at most one

Used byHankel operator as the sum of its slices

DefinitionHankel operator with absolutely summable symbol#✓fully proved

The Hankel operator with symbol a. Defined as the norm-convergent series ∑' k, a k • hankelSlice k over the anti-diagonal slices.

noncomputable def hankelOperator (a : ℕ → 𝕜) (_ha : Summable fun k => ‖a k‖) :
    ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  ∑' k, (a k) • hankelSlice (𝕜 := 𝕜) k

Uses 1 · Used by 7

Statement usesAnti-diagonal slice operator

Used byAdjoint of a Hankel operator · Hankel operator as the sum of its slices · Matrix entries of the Hankel operator · Hankel operator with zero symbol is zero · Hankel operator with absolutely summable symbol is compact · Hankel operator with real symbol is self-adjoint · Norm bound for the Hankel operator

TheoremHankel operator as the sum of its slices#✓fully proved

The Hankel operator is the sum of its slices.

theorem hankel_hasSum_slices {a : ℕ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    HasSum (fun k => (a k) • hankelSlice (𝕜 := 𝕜) k) (hankelOperator a ha)

Uses 3 · Used by 4

Statement usesHankel operator with absolutely summable symbol · Anti-diagonal slice operator

Proof usesSummability of weighted anti-diagonal slices

Used byAdjoint of a Hankel operator · Matrix entries of the Hankel operator · Hankel operator with absolutely summable symbol is compact · Norm bound for the Hankel operator

TheoremMatrix entries of the Hankel operator#✓fully proved

Pointwise action of the Hankel operator: (Hₐ x) i = ∑' j, a (i + j) * x j.

theorem hankelOperator_apply {a : ℕ → 𝕜} (ha : Summable fun k => ‖a k‖)
    (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    hankelOperator a ha x i = ∑' j, a (i + j) * x j

Uses 5

Statement usesHankel operator with absolutely summable symbol

Proof usesAnti-diagonal slice operator · Anti-diagonal slice of a sequence · Hankel operator as the sum of its slices · Anti-diagonal slice operator has norm at most one

TheoremHankel operator with zero symbol is zero#✓fully proved

The zero symbol gives the zero operator.

theorem hankelOperator_zero : hankelOperator (0 : ℕ → 𝕜) (by simp) = 0

Uses 2

Statement usesHankel operator with absolutely summable symbol

Proof usesAnti-diagonal slice operator

TheoremNorm bound for the Hankel operator#✓fully proved

Operator-norm bound: ‖Hₐ‖ ≤ ∑' k, ‖a k‖.

theorem norm_hankelOperator_le {a : ℕ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    ‖hankelOperator a ha‖ ≤ ∑' k, ‖a k‖

Uses 4

Statement usesHankel operator with absolutely summable symbol

Proof usesAnti-diagonal slice operator · Hankel operator as the sum of its slices · Anti-diagonal slice operator has norm at most one

TheoremAdjoint of a Hankel operator#✓fully proved

Adjoint of a Hankel operator: (Hₐ)† = H_{star a}, by passing the adjoint through the finite partial sums and taking the limit.

theorem adjoint_hankelOperator {a : ℕ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    (hankelOperator (𝕜 := 𝕜) a ha)† =
      hankelOperator (star a) (by simpa using ha)

Uses 4 · Used by 1

Statement usesHankel operator with absolutely summable symbol

Proof usesAnti-diagonal slice operator is self-adjoint · Anti-diagonal slice operator · Hankel operator as the sum of its slices

Used byHankel operator with real symbol is self-adjoint

TheoremHankel operator with real symbol is self-adjoint#✓fully proved

A Hankel operator with a real-valued (star-fixed) symbol is self-adjoint.

theorem isSelfAdjoint_hankelOperator_of_forall_star {a : ℕ → 𝕜}
    (ha : Summable fun k => ‖a k‖) (hstar : ∀ k, star (a k) = a k) :
    IsSelfAdjoint (hankelOperator a ha)

Uses 3

Statement usesHankel operator with absolutely summable symbol

Proof usesAdjoint of a Hankel operator · Anti-diagonal slice operator

TheoremPartial sums of the Hankel slice series are compact#✓fully proved

A finite partial sum of the slice series has finite-dimensional range, hence is a compact operator.

theorem hankel_isCompactOperator_partialSum {a : ℕ → 𝕜} (N : ℕ) :
    IsCompactOperator ((∑ k ∈ Finset.range N, (a k) • hankelSlice (𝕜 := 𝕜) k :
      ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)))

Uses 3 · Used by 1

Statement usesAnti-diagonal slice operator

Proof usesAnti-diagonal slice of a sequence · Pointwise action of the anti-diagonal slice operator

Used byHankel operator with absolutely summable symbol is compact

TheoremHankel operator with absolutely summable symbol is compact#✓fully proved

A Hankel operator with an absolutely summable symbol is compact: it is the norm limit of its finite partial sums, each of which has finite-dimensional range.

theorem isCompactOperator_hankelOperator {a : ℕ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    IsCompactOperator (hankelOperator a ha)

Uses 4

Statement usesHankel operator with absolutely summable symbol

Proof usesAnti-diagonal slice operator · Hankel operator as the sum of its slices · Partial sums of the Hankel slice series are compact

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.