Tikhonov regularization

DefinitionTikhonov functional#✓fully proved

The Tikhonov (ridge) functional J(x) = ‖A x - b‖ ^ 2 + Λ * ‖x‖ ^ 2.

noncomputable def tikhonovFunctional (A : H →L[𝕜] K) (b : K) (Λ : ℝ) (x : H) : ℝ :=
  ‖A x - b‖ ^ 2 + Λ * ‖x‖ ^ 2

Used by 4

Used byTikhonov minimizers solve the normal equations · Existence and uniqueness of the Tikhonov minimizer · Solutions of the normal equations minimize the Tikhonov functional · Quadratic identity for the Tikhonov functional at a normal-equation solution

DefinitionNormal operator of the Tikhonov problem#✓fully proved

The normal operator A† ∘L A + Λ • 1 of the Tikhonov problem.

noncomputable def tikhonovOperator (A : H →L[𝕜] K) (Λ : ℝ) : H →L[𝕜] H :=
  A† ∘L A + (Λ : 𝕜) • (1 : H →L[𝕜] H)

Used by 16

Used byTikhonov normal operator is bijective · Tikhonov minimizers solve the normal equations · Solvability of the Tikhonov normal equations · Existence and uniqueness of the Tikhonov minimizer · Tikhonov normal operator has closed range · Solutions of the normal equations minimize the Tikhonov functional · Tikhonov normal operator is self-adjoint · Tikhonov normal operator is invertible · Tikhonov normal operator has trivial kernel · Stability bound for Tikhonov regularized solutions · Tikhonov normal operator is surjective · Real part of the Tikhonov normal operator's quadratic form · Tikhonov solutions tend to zero as the parameter grows · Quadratic identity for the Tikhonov functional at a normal-equation solution · Inner product of the Tikhonov normal operator with its argument · Tikhonov normal operator is bounded below by the regularization parameter

TheoremInner product of the Tikhonov normal operator with its argument#✓fully proved

The inner product of the normal operator applied to x with x itself.

theorem tikhonovOperator_inner_self (A : H →L[𝕜] K) (Λ : ℝ) (x : H) :
    ⟪tikhonovOperator A Λ x, x⟫_𝕜 = ((‖A x‖ ^ 2 + Λ * ‖x‖ ^ 2 : ℝ) : 𝕜)

Uses 1 · Used by 1

Statement usesNormal operator of the Tikhonov problem

Used byReal part of the Tikhonov normal operator's quadratic form

TheoremReal part of the Tikhonov normal operator's quadratic form#✓fully proved

The real part of the inner product of the normal operator applied to x with x itself.

theorem re_inner_tikhonovOperator_self (A : H →L[𝕜] K) (Λ : ℝ) (x : H) :
    RCLike.re ⟪tikhonovOperator A Λ x, x⟫_𝕜 = ‖A x‖ ^ 2 + Λ * ‖x‖ ^ 2

Uses 2 · Used by 2

Statement usesNormal operator of the Tikhonov problem

Proof usesInner product of the Tikhonov normal operator with its argument

Used byStability bound for Tikhonov regularized solutions · Tikhonov normal operator is bounded below by the regularization parameter

TheoremTikhonov normal operator is self-adjoint#✓fully proved

The normal operator is self-adjoint, for every real Λ.

theorem isSelfAdjoint_tikhonovOperator (A : H →L[𝕜] K) (Λ : ℝ) :
    IsSelfAdjoint (tikhonovOperator A Λ)

Uses 1 · Used by 1

Statement usesNormal operator of the Tikhonov problem

Used byTikhonov normal operator is surjective

TheoremTikhonov normal operator is bounded below by the regularization parameter#✓fully proved

The normal operator is bounded below by Λ, for every real Λ.

theorem tikhonovOperator_le_norm (A : H →L[𝕜] K) (Λ : ℝ) (x : H) :
    Λ * ‖x‖ ≤ ‖tikhonovOperator A Λ x‖

Uses 2 · Used by 2

Statement usesNormal operator of the Tikhonov problem

Proof usesReal part of the Tikhonov normal operator's quadratic form

Used byTikhonov normal operator has closed range · Tikhonov normal operator has trivial kernel

TheoremTikhonov normal operator has trivial kernel#✓fully proved

The normal operator has trivial kernel when Λ > 0.

theorem ker_tikhonovOperator_eq_bot (A : H →L[𝕜] K) (Λ : ℝ) (hΛ : 0 < Λ) :
    (tikhonovOperator A Λ : H →ₗ[𝕜] H).ker = ⊥

Uses 2 · Used by 2

Statement usesNormal operator of the Tikhonov problem

Proof usesTikhonov normal operator is bounded below by the regularization parameter

Used byTikhonov normal operator is bijective · Tikhonov normal operator is surjective

TheoremTikhonov normal operator has closed range#✓fully proved

The normal operator has closed range when Λ > 0, since it is bounded below.

theorem isClosed_range_tikhonovOperator (A : H →L[𝕜] K) (Λ : ℝ) (hΛ : 0 < Λ) :
    IsClosed (Set.range (tikhonovOperator A Λ))

Uses 2 · Used by 1

Statement usesNormal operator of the Tikhonov problem

Proof usesTikhonov normal operator is bounded below by the regularization parameter

Used byTikhonov normal operator is surjective

TheoremTikhonov normal operator is surjective#✓fully proved

The normal operator is surjective when Λ > 0: its range is closed and its orthogonal complement is its kernel, which is trivial since the operator is self-adjoint.

theorem range_tikhonovOperator_eq_top (A : H →L[𝕜] K) (Λ : ℝ) (hΛ : 0 < Λ) :
    (tikhonovOperator A Λ : H →ₗ[𝕜] H).range = ⊤

Uses 4 · Used by 1

Statement usesNormal operator of the Tikhonov problem

Proof usesTikhonov normal operator has closed range · Tikhonov normal operator is self-adjoint · Tikhonov normal operator has trivial kernel

Used byTikhonov normal operator is bijective

TheoremTikhonov normal operator is bijective#✓fully proved

The normal operator is bijective when Λ > 0.

theorem bijective_tikhonovOperator (A : H →L[𝕜] K) (Λ : ℝ) (hΛ : 0 < Λ) :
    Function.Bijective (tikhonovOperator A Λ)

Uses 3 · Used by 2

Statement usesNormal operator of the Tikhonov problem

Proof usesTikhonov normal operator has trivial kernel · Tikhonov normal operator is surjective

Used bySolvability of the Tikhonov normal equations · Tikhonov normal operator is invertible

TheoremTikhonov normal operator is invertible#✓fully proved

The normal operator is a unit when Λ > 0.

theorem isUnit_tikhonovOperator (A : H →L[𝕜] K) (Λ : ℝ) (hΛ : 0 < Λ) :
    IsUnit (tikhonovOperator A Λ)

Uses 2

Statement usesNormal operator of the Tikhonov problem

Proof usesTikhonov normal operator is bijective

TheoremSolvability of the Tikhonov normal equations#✓fully proved

The normal equations are solvable when Λ > 0.

theorem exists_tikhonov_normal_equations (A : H →L[𝕜] K) (b : K) (Λ : ℝ)
    (hΛ : 0 < Λ) : ∃ x, tikhonovOperator A Λ x = (A†) b

Uses 2 · Used by 1

Statement usesNormal operator of the Tikhonov problem

Proof usesTikhonov normal operator is bijective

Used byExistence and uniqueness of the Tikhonov minimizer

TheoremQuadratic identity for the Tikhonov functional at a normal-equation solution#✓fully proved

The quadratic identity for the Tikhonov functional around a solution of the normal equations: the cross term vanishes by the normal equations.

theorem tikhonovFunctional_add_of_normal_equations (A : H →L[𝕜] K) (b : K) (Λ : ℝ)
    {x₀ : H} (h₀ : tikhonovOperator A Λ x₀ = (A†) b) (x : H) :
    tikhonovFunctional A b Λ x
      = tikhonovFunctional A b Λ x₀ + ‖A (x - x₀)‖ ^ 2 + Λ * ‖x - x₀‖ ^ 2

Uses 2 · Used by 2

Statement usesTikhonov functional · Normal operator of the Tikhonov problem

Used byTikhonov minimizers solve the normal equations · Solutions of the normal equations minimize the Tikhonov functional

TheoremSolutions of the normal equations minimize the Tikhonov functional#✓fully proved

A solution of the normal equations minimizes the Tikhonov functional.

theorem isMinOn_tikhonovFunctional_of_normal_equations (A : H →L[𝕜] K) (b : K) (Λ : ℝ)
    (hΛ : 0 ≤ Λ) {x₀ : H} (h₀ : tikhonovOperator A Λ x₀ = (A†) b) :
    IsMinOn (tikhonovFunctional A b Λ) univ x₀

Uses 3 · Used by 1

Statement usesTikhonov functional · Normal operator of the Tikhonov problem

Proof usesQuadratic identity for the Tikhonov functional at a normal-equation solution

Used byExistence and uniqueness of the Tikhonov minimizer

TheoremTikhonov minimizers solve the normal equations#✓fully proved

A minimizer of the Tikhonov functional equals a solution of the normal equations, when Λ > 0.

theorem eq_of_isMinOn_tikhonovFunctional (A : H →L[𝕜] K) (b : K) (Λ : ℝ)
    (hΛ : 0 < Λ) {x₀ x : H} (h₀ : tikhonovOperator A Λ x₀ = (A†) b)
    (hmin : IsMinOn (tikhonovFunctional A b Λ) univ x) : x = x₀

Uses 3 · Used by 1

Statement usesTikhonov functional · Normal operator of the Tikhonov problem

Proof usesQuadratic identity for the Tikhonov functional at a normal-equation solution

Used byExistence and uniqueness of the Tikhonov minimizer

TheoremExistence and uniqueness of the Tikhonov minimizer#✓fully proved

The Tikhonov functional has a unique minimizer when Λ > 0.

theorem existsUnique_tikhonov_minimizer (A : H →L[𝕜] K) (b : K) (Λ : ℝ)
    (hΛ : 0 < Λ) : ∃! x, ∀ y, tikhonovFunctional A b Λ x ≤ tikhonovFunctional A b Λ y

Uses 5

Statement usesTikhonov functional

Proof usesTikhonov minimizers solve the normal equations · Solvability of the Tikhonov normal equations · Solutions of the normal equations minimize the Tikhonov functional · Normal operator of the Tikhonov problem

TheoremStability bound for Tikhonov regularized solutions#✓fully proved

Stability bound for a solution of the normal equations.

theorem norm_le_of_tikhonov_normal_equations (A : H →L[𝕜] K) (b : K) (Λ : ℝ)
    (hΛ : 0 < Λ) {x : H} (h : tikhonovOperator A Λ x = (A†) b) :
    ‖x‖ ≤ ‖A‖ * ‖b‖ / Λ

Uses 2 · Used by 1

Statement usesNormal operator of the Tikhonov problem

Proof usesReal part of the Tikhonov normal operator's quadratic form

Used byTikhonov solutions tend to zero as the parameter grows

TheoremTikhonov solutions tend to zero as the parameter grows#✓fully proved

Solutions of the Tikhonov normal equations tend to 0 as Λ → ∞.

theorem tendsto_tikhonov_solution_zero (A : H →L[𝕜] K) (b : K) (Λ : ℕ → ℝ)
    (hΛ : ∀ n, 0 < Λ n) (hΛtop : Tendsto Λ atTop atTop) (x : ℕ → H)
    (hx : ∀ n, tikhonovOperator A (Λ n) (x n) = (A†) b) :
    Tendsto x atTop (𝓝 0)

Uses 2

Statement usesNormal operator of the Tikhonov problem

Proof usesStability bound for Tikhonov regularized solutions

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.