Riesz bases

DefinitionRiesz basis of a Hilbert space#✓fully proved

A family f : ι → E is a Riesz basis (with respect to the Hilbert basis b) if it is the image of b under a bounded invertible operator.

def IsRieszBasis (b : HilbertBasis ι 𝕜 E) (f : ι → E) : Prop :=
  ∃ T : E ≃L[𝕜] E, ∀ i, T (b i) = f i

Used by 4

Used byRiesz bases have dense span · Biorthogonal dual of a Riesz basis · Paley–Wiener stability theorem · Riesz bases are linearly independent

TheoremRiesz bases are linearly independent#✓fully proved

A Riesz basis is linearly independent.

theorem IsRieszBasis.linearIndependent {b : HilbertBasis ι 𝕜 E} {f : ι → E}
    (h : IsRieszBasis b f) : LinearIndependent 𝕜 f

Uses 1

Statement usesRiesz basis of a Hilbert space

TheoremRiesz bases have dense span#✓fully proved

A Riesz basis has dense span.

theorem IsRieszBasis.dense_span {b : HilbertBasis ι 𝕜 E} {f : ι → E}
    (h : IsRieszBasis b f) : (Submodule.span 𝕜 (Set.range f)).topologicalClosure = ⊤

Uses 1

Statement usesRiesz basis of a Hilbert space

TheoremBiorthogonal dual of a Riesz basis#✓fully proved

A Riesz basis admits a biorthogonal dual family with a reconstruction formula: there is g : ι → E with ⟪f i, g j⟫ = if i = j then 1 else 0 and x = ∑' i, ⟪g i, x⟫ • f i for every x. The dual is g j = (T⁻¹)† (b j) for the operator T witnessing that f is a Riesz basis.

theorem IsRieszBasis.exists_dual {b : HilbertBasis ι 𝕜 E} {f : ι → E}
    [DecidableEq ι] (h : IsRieszBasis b f) :
    ∃ g : ι → E, (∀ i j, ⟪f i, g j⟫_𝕜 = if i = j then 1 else 0) ∧
      ∀ x, HasSum (fun i => ⟪g i, x⟫_𝕜 • f i) x

Uses 1

Statement usesRiesz basis of a Hilbert space

DefinitionNorm sequence of a square-summable family#✓fully proved

The sequence of norms of a square-summable family, as an element of ℓ²(ι, ℝ).

noncomputable def normSeq (d : ι → E) (hd : Summable fun i => ‖d i‖ ^ 2) :
    ℓ²(ι, ℝ) :=
  ⟨fun i => ‖d i‖, by
    show Memℓp (fun i => ‖d i‖) (2 : ℝ≥0∞)
    rw [memℓp_gen_iff (by simp : (0 : ℝ) < (2 : ℝ≥0∞).toReal)]
    have hni : ∀ i, |(‖d i‖ : ℝ)| = ‖d i‖ :=
      fun i => abs_of_nonneg (norm_nonneg _)
    simpa only [Real.norm_eq_abs, hni, ENNReal.toReal_ofNat, Real.rpow_two] using hd⟩

Used by 2

Used byNorm bound for a synthesis series · Absolute summability of a synthesis series

DefinitionNorm sequence of an \(\ell^2\) coefficient sequence#✓fully proved

The sequence of norms of an ℓ² coefficient sequence, as an element of ℓ²(ι, ℝ).

noncomputable def normSeqLp (c : ℓ²(ι, 𝕜)) : ℓ²(ι, ℝ) :=
  ⟨fun i => ‖c i‖, (lp.memℓp c).norm⟩

Used by 3

Used by\(\ell^2\) norm of the norm sequence · Norm bound for a synthesis series · Absolute summability of a synthesis series

Theorem\(\ell^2\) norm of the norm sequence#✓fully proved

The ℓ² norm of the norms of a coefficient sequence is the norm of the sequence.

theorem norm_normSeqLp (c : ℓ²(ι, 𝕜)) : ‖normSeqLp c‖ = ‖c‖

Uses 1 · Used by 1

Statement usesNorm sequence of an \(\ell^2\) coefficient sequence

Used byNorm bound for a synthesis series

TheoremAbsolute summability of a synthesis series#✓fully proved

The norms of the terms of a synthesis series are summable when the coefficient sequence is in ℓ² and the synthesized family is square-summable: this is Cauchy–Schwarz for ℓ², via lp.tsum_mul_le_mul_norm applied to the two real ℓ² sequences of norms.

theorem summable_norm_synthesis (d : ι → E)
    (hd : Summable fun i => ‖d i‖ ^ 2) (c : ℓ²(ι, 𝕜)) :
    Summable fun i => ‖c i • d i‖

Uses 2 · Used by 2

Proof usesNorm sequence of a square-summable family · Norm sequence of an \(\ell^2\) coefficient sequence

Used byNorm bound for a synthesis series · Summability of a synthesis series

TheoremSummability of a synthesis series#✓fully proved

The terms of a synthesis series are summable when the coefficient sequence is in ℓ² and the synthesized family is square-summable.

theorem summable_synthesis (d : ι → E) (hd : Summable fun i => ‖d i‖ ^ 2)
    (c : ℓ²(ι, 𝕜)) : Summable fun i => c i • d i

Uses 1 · Used by 1

Proof usesAbsolute summability of a synthesis series

Used byLinear map underlying the synthesis operator

TheoremNorm bound for a synthesis series#✓fully proved

Norm bound for a synthesis series, by Cauchy–Schwarz for ℓ².

theorem norm_tsum_smul_le (d : ι → E) (hd : Summable fun i => ‖d i‖ ^ 2)
    (c : ℓ²(ι, 𝕜)) :
    ‖∑' i, c i • d i‖ ≤ Real.sqrt (∑' i, ‖d i‖ ^ 2) * ‖c‖

Uses 4 · Used by 2

Proof usesNorm sequence of a square-summable family · Norm sequence of an \(\ell^2\) coefficient sequence · \(\ell^2\) norm of the norm sequence · Absolute summability of a synthesis series

Used byOperator norm bound for the synthesis operator · Synthesis operator of a square-summable family

DefinitionLinear map underlying the synthesis operator#✓fully proved

The linear map underlying the synthesis operator.

noncomputable def synthesisLinearMap (d : ι → E)
    (hd : Summable fun i => ‖d i‖ ^ 2) :
    ℓ²(ι, 𝕜) →ₗ[𝕜] E where
  toFun c := ∑' i, c i • d i
  map_add' c c' := by
    rw [← Summable.tsum_add (summable_synthesis d hd c) (summable_synthesis d hd c')]
    refine tsum_congr fun i => ?_
    simp [add_smul]
  map_smul' a c := by
    simp only [RingHom.id_apply]
    rw [← (summable_synthesis d hd c).tsum_const_smul a]
    refine tsum_congr fun i => ?_
    simp [lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, mul_smul]

Uses 1 · Used by 1

Statement usesSummability of a synthesis series

Used bySynthesis operator of a square-summable family

DefinitionSynthesis operator of a square-summable family#✓fully proved

The synthesis operator: for a square-summable family d : ι → E, the bounded operator ℓ²(ι, 𝕜) →L[𝕜] E sending c to ∑' i, c i • d i.

noncomputable def synthesisCLM (d : ι → E) (hd : Summable fun i => ‖d i‖ ^ 2) :
    ℓ²(ι, 𝕜) →L[𝕜] E :=
  LinearMap.mkContinuous (synthesisLinearMap d hd) _
    fun c => norm_tsum_smul_le d hd c

Uses 2 · Used by 3

Statement usesNorm bound for a synthesis series · Linear map underlying the synthesis operator

Used byPaley–Wiener stability theorem · Operator norm bound for the synthesis operator · Synthesis operator on a basis vector

TheoremOperator norm bound for the synthesis operator#✓fully proved

The operator norm of the synthesis operator is at most √(∑' i, ‖d i‖ ^ 2).

theorem norm_synthesisCLM_le (d : ι → E) (hd : Summable fun i => ‖d i‖ ^ 2) :
    ‖synthesisCLM (𝕜 := 𝕜) d hd‖ ≤ Real.sqrt (∑' i, ‖d i‖ ^ 2)

Uses 2 · Used by 1

Statement usesSynthesis operator of a square-summable family

Proof usesNorm bound for a synthesis series

Used byPaley–Wiener stability theorem

TheoremSynthesis operator on a basis vector#✓fully proved

The synthesis operator at a basis vector picks out one term of the family.

theorem synthesisCLM_single (d : ι → E) (hd : Summable fun i => ‖d i‖ ^ 2)
    [DecidableEq ι] (i : ι) :
    synthesisCLM (𝕜 := 𝕜) d hd (lp.single 2 i (1 : 𝕜)) = d i

Uses 1 · Used by 1

Statement usesSynthesis operator of a square-summable family

Used byPaley–Wiener stability theorem

TheoremPaley–Wiener stability theorem#✓fully proved

If b is a Hilbert basis and ∑' i, ‖f i - b i‖ ^ 2 < 1, then f is a Riesz basis.

theorem isRieszBasis_of_tsum_norm_sq_lt_one (b : HilbertBasis ι 𝕜 E) (f : ι → E)
    (hd : Summable fun i => ‖f i - b i‖ ^ 2)
    (h : ∑' i, ‖f i - b i‖ ^ 2 < 1) : IsRieszBasis b f

Uses 4

Statement usesRiesz basis of a Hilbert space

Proof usesOperator norm bound for the synthesis operator · Synthesis operator of a square-summable family · Synthesis operator on a basis vector

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.