Frames in Hilbert spaces

DefinitionFinite frame#✓fully proved

Let \(E\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). A finite family \((f_i)_{i \in \iota}\) in \(E\) is a frame with frame bounds \(A, B \in \mathbb{R}\) if \(A > 0\), \(B > 0\) and, for every \(x \in E\), \(A \|x\|^2 \le \sum_{i \in \iota} |\langle f_i, x \rangle|^2 \le B \|x\|^2\).

def IsFrame (f : ι → E) (A B : ℝ) : Prop :=
  0 < A ∧ 0 < B ∧ ∀ x : E,
    A * ‖x‖ ^ 2 ≤ ∑ i, ‖⟪f i, x⟫_𝕜‖ ^ 2 ∧ ∑ i, ‖⟪f i, x⟫_𝕜‖ ^ 2 ≤ B * ‖x‖ ^ 2

Used by 16

Used byCanonical dual frame · The inverse frame operator is a right inverse · Frame operator of the canonical dual frame · Tight frames have scalar frame operator · Inverse frame operator · The inverse frame operator is a left inverse · Frame reconstruction formula · The canonical dual frame is a frame · The inverse frame operator is self-adjoint · The frame operator of a frame is invertible · The frame operator is bounded below · Lower frame inequality · The frame operator has norm at most the upper frame bound · The lower frame bound is positive · The upper frame bound is positive · Upper frame inequality

TheoremThe lower frame bound is positive#✓fully proved

Let \(E\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). If a finite family \((f_i)_{i \in \iota}\) in \(E\) is a frame with frame bounds \(A\) and \(B\), then \(A > 0\).

theorem IsFrame.pos_left {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) : 0 < A

Uses 1 · Used by 2

Statement usesFinite frame

Used byThe canonical dual frame is a frame · The frame operator of a frame is invertible

TheoremThe upper frame bound is positive#✓fully proved

If a finite family \((f_i)_{i \in \iota}\) in an inner product space \(E\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)) is a frame with frame bounds \(A\) and \(B\), then \(0 < B\).

theorem IsFrame.pos_right {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) : 0 < B

Uses 1 · Used by 2

Statement usesFinite frame

Used byThe canonical dual frame is a frame · The frame operator has norm at most the upper frame bound

TheoremLower frame inequality#✓fully proved

Let \(E\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((f_i)_{i \in \iota}\) be a finite frame in \(E\) with frame bounds \(A\) and \(B\). Then \(A \|x\|^2 \le \sum_{i \in \iota} |\langle f_i, x \rangle|^2\) for every \(x \in E\).

theorem IsFrame.lower {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) (x : E) :
    A * ‖x‖ ^ 2 ≤ ∑ i, ‖⟪f i, x⟫_𝕜‖ ^ 2

Uses 1 · Used by 3

Statement usesFinite frame

Used byTight frames have scalar frame operator · The canonical dual frame is a frame · The frame operator is bounded below

TheoremUpper frame inequality#✓fully proved

If a finite family \((f_i)_{i \in \iota}\) in an inner product space \(E\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)) is a frame with frame bounds \(A\) and \(B\), then \(\sum_{i} |\langle f_i, x \rangle|^2 \le B \|x\|^2\) for every \(x \in E\).

theorem IsFrame.upper {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) (x : E) :
    ∑ i, ‖⟪f i, x⟫_𝕜‖ ^ 2 ≤ B * ‖x‖ ^ 2

Uses 1 · Used by 3

Statement usesFinite frame

Used byTight frames have scalar frame operator · The canonical dual frame is a frame · The frame operator has norm at most the upper frame bound

DefinitionFrame operator#✓fully proved

For a finite family \((f_i)_{i \in \iota}\) in an inner product space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), the frame operator is the bounded linear operator \(S \colon E \to E\) given by \(S x = \sum_{i \in \iota} \langle f_i, x \rangle f_i\), the sum of the rank-one operators \(x \mapsto \langle f_i, x \rangle f_i\). The inner product is conjugate-linear in its first argument.

noncomputable def frameOperator (f : ι → E) : E →L[𝕜] E :=
  ∑ i, rankOne 𝕜 (f i) (f i)

Used by 17

Used byFrame operator formula · The inverse frame operator is a right inverse · Frame operator of the canonical dual frame · Tight frames have scalar frame operator · Inverse frame operator · The inverse frame operator is a left inverse · Frame reconstruction formula · Inner product against the frame operator · Quadratic form of the frame operator · The canonical dual frame is a frame · The frame operator is self-adjoint · The inverse frame operator is self-adjoint · The frame operator of a frame is invertible · The frame operator is bounded below · The frame operator has norm at most the upper frame bound · Real part of the frame quadratic form · Cauchy–Schwarz bound for the frame operator

TheoremFrame operator formula#✓fully proved

For a finite family \((f_i)_{i \in \iota}\) in an inner product space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), the frame operator \(S\) of the family satisfies \(S x = \sum_{i \in \iota} \langle f_i, x \rangle f_i\) for every \(x \in E\), where the inner product is conjugate-linear in its first argument.

theorem frameOperator_apply (f : ι → E) (x : E) :
    frameOperator (𝕜 := 𝕜) f x = ∑ i, ⟪f i, x⟫_𝕜 • f i

Uses 1 · Used by 3

Statement usesFrame operator

Used byFrame operator of the canonical dual frame · Frame reconstruction formula · Inner product against the frame operator

TheoremInner product against the frame operator#✓fully proved

Let \(E\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with inner product conjugate-linear in the first argument, and let \(S\) be the frame operator of a finite family \((f_i)_{i \in \iota}\) in \(E\). Then \(\langle S x, y \rangle = \sum_{i \in \iota} \overline{\langle f_i, x \rangle} \, \langle f_i, y \rangle\) for all \(x, y \in E\).

theorem inner_frameOperator_apply (f : ι → E) (x y : E) :
    ⟪frameOperator (𝕜 := 𝕜) f x, y⟫_𝕜
      = ∑ i, (starRingEnd 𝕜) ⟪f i, x⟫_𝕜 * ⟪f i, y⟫_𝕜

Uses 2 · Used by 2

Statement usesFrame operator

Proof usesFrame operator formula

Used byQuadratic form of the frame operator · Cauchy–Schwarz bound for the frame operator

TheoremQuadratic form of the frame operator#✓fully proved

Let \(S\) be the frame operator of a finite family \((f_i)_{i \in \iota}\) in an inner product space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). For every \(x \in E\), \(\langle S x, x \rangle = \sum_{i \in \iota} |\langle f_i, x \rangle|^2\); the right side is a real number, viewed as an element of \(\mathbb{K}\).

theorem inner_frameOperator_apply_self (f : ι → E) (x : E) :
    ⟪frameOperator (𝕜 := 𝕜) f x, x⟫_𝕜
      = ((∑ i, ‖⟪f i, x⟫_𝕜‖ ^ 2 : ℝ) : 𝕜)

Uses 2 · Used by 2

Statement usesFrame operator

Proof usesInner product against the frame operator

Used byTight frames have scalar frame operator · Real part of the frame quadratic form

TheoremReal part of the frame quadratic form#✓fully proved

Let \((f_i)_{i \in \iota}\) be a finite family in an inner product space \(E\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)), with frame operator \(S\). For every \(x \in E\), \(\operatorname{Re} \langle S x, x \rangle = \sum_{i} |\langle f_i, x \rangle|^2\).

theorem re_inner_frameOperator_apply_self (f : ι → E) (x : E) :
    RCLike.re ⟪frameOperator (𝕜 := 𝕜) f x, x⟫_𝕜 = ∑ i, ‖⟪f i, x⟫_𝕜‖ ^ 2

Uses 2 · Used by 2

Statement usesFrame operator

Proof usesQuadratic form of the frame operator

Used byThe canonical dual frame is a frame · The frame operator is bounded below

TheoremCauchy–Schwarz bound for the frame operator#✓fully proved

Let \((f_i)_{i \in \iota}\) be a finite family in an inner product space \(E\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)), with frame operator \(S\). For all \(x, y \in E\),

\[ |\langle S x, y \rangle|^2 \le \Big(\sum_{i} |\langle f_i, x \rangle|^2\Big) \Big(\sum_{i} |\langle f_i, y \rangle|^2\Big). \]

theorem sq_norm_inner_frameOperator_apply_le (f : ι → E) (x y : E) :
    ‖⟪frameOperator (𝕜 := 𝕜) f x, y⟫_𝕜‖ ^ 2
      ≤ (∑ i, ‖⟪f i, x⟫_𝕜‖ ^ 2) * (∑ i, ‖⟪f i, y⟫_𝕜‖ ^ 2)

Uses 2 · Used by 2

Statement usesFrame operator

Proof usesInner product against the frame operator

Used byThe canonical dual frame is a frame · The frame operator has norm at most the upper frame bound

TheoremThe frame operator is self-adjoint#✓fully proved

Let \(E\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). For every finite family \((f_i)_{i \in \iota}\) in \(E\), not necessarily a frame, the frame operator of \((f_i)_{i \in \iota}\) is self-adjoint.

theorem isSelfAdjoint_frameOperator (f : ι → E) :
    IsSelfAdjoint (frameOperator (𝕜 := 𝕜) f)

Uses 1 · Used by 3

Statement usesFrame operator

Used byTight frames have scalar frame operator · The inverse frame operator is self-adjoint · The frame operator of a frame is invertible

TheoremThe frame operator is bounded below#✓fully proved

Let \(E\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((f_i)_{i \in \iota}\) be a finite frame in \(E\) with frame bounds \(A\) and \(B\) and frame operator \(S\). Then \(A \|x\| \le \|S x\|\) for every \(x \in E\).

theorem le_norm_frameOperator_apply {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B)
    (x : E) : A * ‖x‖ ≤ ‖frameOperator (𝕜 := 𝕜) f x‖

Uses 4 · Used by 1

Statement usesFinite frame · Frame operator

Proof usesLower frame inequality · Real part of the frame quadratic form

Used byThe frame operator of a frame is invertible

TheoremThe frame operator of a frame is invertible#✓fully proved

Let \(E\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((f_i)_{i \in \iota}\) be a finite frame in \(E\) with frame bounds \(A\) and \(B\). Then its frame operator \(S\) is a unit in the algebra of bounded linear operators on \(E\), that is, \(S\) has a bounded linear two-sided inverse.

The operator \(S\) is bounded below and self-adjoint, so it is injective with closed range whose orthogonal complement is trivial.

theorem isUnit_frameOperator {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) :
    IsUnit (frameOperator (𝕜 := 𝕜) f)

Uses 5 · Used by 3

Statement usesFinite frame · Frame operator

Proof usesThe lower frame bound is positive · The frame operator is self-adjoint · The frame operator is bounded below

Used byThe inverse frame operator is a right inverse · Inverse frame operator · The inverse frame operator is a left inverse

TheoremThe frame operator has norm at most the upper frame bound#✓fully proved

Let \(E\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((f_i)_{i \in \iota}\) be a finite frame in \(E\) with frame bounds \(A\) and \(B\) and frame operator \(S\). Then the operator norm of \(S\) satisfies \(\|S\| \le B\).

theorem norm_frameOperator_le {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) :
    ‖frameOperator (𝕜 := 𝕜) f‖ ≤ B

Uses 5

Statement usesFinite frame · Frame operator

Proof usesThe upper frame bound is positive · Upper frame inequality · Cauchy–Schwarz bound for the frame operator

DefinitionInverse frame operator#✓fully proved

Let \((f_i)_{i \in \iota}\), with \(\iota\) finite, be a frame with bounds \(A\) and \(B\) in a Hilbert space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). Its frame operator \(S\) is invertible in the algebra of bounded linear operators on \(E\), and the inverse frame operator \(S^{-1}\) is its inverse there.

noncomputable def frameOperatorInv {f : ι → E} {A B : ℝ}
    (hf : IsFrame (𝕜 := 𝕜) f A B) : E →L[𝕜] E :=
  ↑(IsUnit.unit (isUnit_frameOperator hf))⁻¹

Uses 3 · Used by 7

Statement usesFinite frame · Frame operator · The frame operator of a frame is invertible

Used byCanonical dual frame · The inverse frame operator is a right inverse · Frame operator of the canonical dual frame · The inverse frame operator is a left inverse · Frame reconstruction formula · The canonical dual frame is a frame · The inverse frame operator is self-adjoint

TheoremThe inverse frame operator is a right inverse#✓fully proved

Let \((f_i)_{i \in \iota}\), with \(\iota\) finite, be a frame with bounds \(A\) and \(B\) in a Hilbert space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with frame operator \(S\) and inverse frame operator \(S^{-1}\). Then \(S \circ S^{-1}\) is the identity operator on \(E\).

theorem frameOperator_comp_frameOperatorInv {f : ι → E} {A B : ℝ}
    (hf : IsFrame (𝕜 := 𝕜) f A B) :
    frameOperator (𝕜 := 𝕜) f ∘L frameOperatorInv hf = 1

Uses 4 · Used by 4

Statement usesFinite frame · Frame operator · Inverse frame operator

Proof usesThe frame operator of a frame is invertible

Used byFrame operator of the canonical dual frame · Frame reconstruction formula · The canonical dual frame is a frame · The inverse frame operator is self-adjoint

TheoremThe inverse frame operator is a left inverse#✓fully proved

Let \((f_i)_{i \in \iota}\), with \(\iota\) finite, be a frame with bounds \(A\) and \(B\) in a Hilbert space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with frame operator \(S\) and inverse frame operator \(S^{-1}\). Then \(S^{-1} \circ S\) is the identity operator on \(E\).

theorem frameOperatorInv_comp_frameOperator {f : ι → E} {A B : ℝ}
    (hf : IsFrame (𝕜 := 𝕜) f A B) :
    frameOperatorInv hf ∘L frameOperator (𝕜 := 𝕜) f = 1

Uses 4 · Used by 1

Statement usesFinite frame · Frame operator · Inverse frame operator

Proof usesThe frame operator of a frame is invertible

Used byThe canonical dual frame is a frame

TheoremThe inverse frame operator is self-adjoint#✓fully proved

Let \(E\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((f_i)_{i \in \iota}\) be a finite frame in \(E\) with frame bounds \(A\) and \(B\). Then the inverse \(S^{-1}\) of its frame operator \(S\) is self-adjoint.

theorem isSelfAdjoint_frameOperatorInv {f : ι → E} {A B : ℝ}
    (hf : IsFrame (𝕜 := 𝕜) f A B) : IsSelfAdjoint (frameOperatorInv hf)

Uses 5 · Used by 1

Statement usesFinite frame · Inverse frame operator

Proof usesFrame operator · The inverse frame operator is a right inverse · The frame operator is self-adjoint

Used byFrame operator of the canonical dual frame

TheoremFrame reconstruction formula#✓fully proved

Let \((f_i)_{i \in \iota}\), with \(\iota\) finite, be a frame with bounds \(A\) and \(B\) in a Hilbert space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), and let \(S^{-1}\) be the inverse of its frame operator. Then every \(x \in E\) satisfies \(x = \sum_{i \in \iota} \langle f_i, S^{-1} x \rangle f_i\).

theorem frame_reconstruction {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B)
    (x : E) :
    ∑ i, ⟪f i, frameOperatorInv hf x⟫_𝕜 • f i = x

Uses 5

Statement usesFinite frame · Inverse frame operator

Proof usesFrame operator · Frame operator formula · The inverse frame operator is a right inverse

DefinitionCanonical dual frame#✓fully proved

Let \((f_i)_{i \in \iota}\), with \(\iota\) finite, be a frame with bounds \(A\) and \(B\) in a Hilbert space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), and let \(S^{-1}\) be the inverse of its frame operator. The canonical dual frame is the family \((S^{-1} f_i)_{i \in \iota}\).

noncomputable def dualFrame {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B)
    (i : ι) : E :=
  frameOperatorInv hf (f i)

Uses 2 · Used by 2

Statement usesFinite frame · Inverse frame operator

Used byFrame operator of the canonical dual frame · The canonical dual frame is a frame

TheoremFrame operator of the canonical dual frame#✓fully proved

Let \((f_i)_{i \in \iota}\), with \(\iota\) finite, be a frame with bounds \(A\) and \(B\) in a Hilbert space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), and let \(S^{-1}\) be the inverse of its frame operator. Then the frame operator of the canonical dual frame \((S^{-1} f_i)_{i \in \iota}\) is \(S^{-1}\).

theorem frameOperator_dualFrame {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) :
    frameOperator (𝕜 := 𝕜) (dualFrame hf) = frameOperatorInv hf

Uses 7 · Used by 1

Statement usesFinite frame · Canonical dual frame · Frame operator · Inverse frame operator

Proof usesFrame operator formula · The inverse frame operator is a right inverse · The inverse frame operator is self-adjoint

Used byThe canonical dual frame is a frame

TheoremThe canonical dual frame is a frame#✓fully proved

Let \(E\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((f_i)_{i \in \iota}\) be a finite frame in \(E\) with frame bounds \(A\) and \(B\) and frame operator \(S\). Then the canonical dual frame \((S^{-1} f_i)_{i \in \iota}\) is a frame with lower frame bound \(1/B\) and upper frame bound \(1/A\).

theorem isFrame_dualFrame {f : ι → E} {A B : ℝ} (hf : IsFrame (𝕜 := 𝕜) f A B) :
    IsFrame (𝕜 := 𝕜) (dualFrame hf) (1 / B) (1 / A)

Uses 13

Statement usesFinite frame · Canonical dual frame

Proof usesLower frame inequality · The lower frame bound is positive · The upper frame bound is positive · Upper frame inequality · Frame operator · Inverse frame operator · The inverse frame operator is a left inverse · The inverse frame operator is a right inverse · Frame operator of the canonical dual frame · Real part of the frame quadratic form · Cauchy–Schwarz bound for the frame operator

TheoremTight frames have scalar frame operator#✓fully proved

Let \((f_i)_{i \in \iota}\), with \(\iota\) finite, be a frame in a Hilbert space \(E\) over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) whose lower and upper frame bounds are both equal to \(A\). Then its frame operator is \(S = A \cdot I\), where \(I\) is the identity operator on \(E\).

theorem frameOperator_eq_smul_one_of_isTightFrame {f : ι → E} {A : ℝ}
    (hf : IsFrame (𝕜 := 𝕜) f A A) :
    frameOperator (𝕜 := 𝕜) f = (A : 𝕜) • (1 : E →L[𝕜] E)

Uses 6

Statement usesFinite frame · Frame operator

Proof usesLower frame inequality · Upper frame inequality · Quadratic form of the frame operator · The frame operator is self-adjoint

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.