Banach–Nečas–Babuška theorem

AbbreviationInf-sup condition#✓fully proved

The inf–sup condition: there is β > 0 such that β * ‖x‖ ≤ ‖B x‖ for every x. The right-hand side is the dual norm of the functional B x, i.e. sup_{‖y‖ ≤ 1} |B x y| (see norm_apply_eq_iSup).

abbrev IsInfSup (B : E →L[ℝ] F →L[ℝ] ℝ) : Prop :=
  ∃ β : ℝ, 0 < β ∧ ∀ x : E, β * ‖x‖ ≤ ‖B x‖

Used by 11

Used byBanach–Nečas–Babuška theorem · Banach–Nečas–Babuška equivalence acts as the bilinear form · Unique solvability of the inf-sup variational problem · Inf-sup condition in supremum form · Norm of the Banach–Nečas–Babuška isomorphism applied to a vector · Inf-sup condition makes the associated operator antilipschitz · Banach–Nečas–Babuška isomorphism · Banach–Nečas–Babuška isomorphism is characterized by the form · Inf-sup condition makes the associated operator's range closed · Inf-sup condition makes the associated operator injective · Inf-sup and nondegeneracy make the associated operator surjective

AbbreviationNondegeneracy in the second variable#✓fully proved

The only y annihilated by every B x is y = 0.

abbrev IsNondegenerate (B : E →L[ℝ] F →L[ℝ] ℝ) : Prop :=
  ∀ y : F, (∀ x : E, B x y = 0) → y = 0

Used by 10

Used byBanach–Nečas–Babuška theorem · Banach–Nečas–Babuška equivalence acts as the bilinear form · Stability bound for the inf-sup variational problem · Unique solvability of the inf-sup variational problem · Norm of the Banach–Nečas–Babuška isomorphism applied to a vector · Pointwise inverse bound for the Banach–Nečas–Babuška isomorphism · Operator-norm bound for the inverse Banach–Nečas–Babuška isomorphism · Banach–Nečas–Babuška isomorphism · Banach–Nečas–Babuška isomorphism is characterized by the form · Inf-sup and nondegeneracy make the associated operator surjective

TheoremDual norm as a supremum over the unit ball#✓fully proved

The dual norm is the supremum over the closed unit ball.

theorem norm_apply_eq_iSup (B : E →L[ℝ] F →L[ℝ] ℝ) (x : E) :
    ‖B x‖ = ⨆ y : {y : F // ‖y‖ ≤ 1}, ‖B x y‖

Used by 1

Used byInf-sup condition in supremum form

TheoremInf-sup condition in supremum form#✓fully proved

The inf–sup condition in classical supremum form.

theorem isInfSup_iff (B : E →L[ℝ] F →L[ℝ] ℝ) :
    IsInfSup B ↔ ∃ β : ℝ, 0 < β ∧
      ∀ x : E, β * ‖x‖ ≤ ⨆ y : {y : F // ‖y‖ ≤ 1}, ‖B x y‖

Uses 2

Statement usesInf-sup condition

Proof usesDual norm as a supremum over the unit ball

DefinitionOperator associated to a bounded bilinear form#✓fully proved

The operator E →L[ℝ] F associated to a bounded bilinear form B : E →L[ℝ] F →L[ℝ] ℝ, characterized by ⟪bilinearFormSharp B x, y⟫ = B x y. This is the two-space analogue of Mathlib's continuousLinearMapOfBilin (which is stated for E = F).

noncomputable def bilinearFormSharp (B : E →L[ℝ] F →L[ℝ] ℝ) : E →L[ℝ] F :=
  (InnerProductSpace.toDual ℝ F).symm.toContinuousLinearEquiv.toContinuousLinearMap.comp B

Used by 8

Used byStability bound for the inf-sup variational problem · Norm of the Banach–Nečas–Babuška isomorphism applied to a vector · Inf-sup condition makes the associated operator antilipschitz · Banach–Nečas–Babuška isomorphism · Banach–Nečas–Babuška isomorphism is characterized by the form · Inf-sup condition makes the associated operator's range closed · Inf-sup condition makes the associated operator injective · Inf-sup and nondegeneracy make the associated operator surjective

TheoremInf-sup condition makes the associated operator antilipschitz#✓fully proved

The inf–sup condition makes bilinearFormSharp B antilipschitz.

theorem sharp_antilipschitz {B : E →L[ℝ] F →L[ℝ] ℝ} (hB : IsInfSup B) :
    ∃ C : ℝ≥0, 0 < C ∧ AntilipschitzWith C (bilinearFormSharp B)

Uses 2 · Used by 2

Statement usesInf-sup condition · Operator associated to a bounded bilinear form

Used byInf-sup condition makes the associated operator's range closed · Inf-sup condition makes the associated operator injective

TheoremInf-sup condition makes the associated operator injective#✓fully proved

The inf–sup condition makes bilinearFormSharp B injective.

theorem sharp_ker_eq_bot {B : E →L[ℝ] F →L[ℝ] ℝ} (hB : IsInfSup B) :
    (bilinearFormSharp B).ker = ⊥

Uses 3 · Used by 1

Statement usesInf-sup condition · Operator associated to a bounded bilinear form

Proof usesInf-sup condition makes the associated operator antilipschitz

Used byBanach–Nečas–Babuška isomorphism

TheoremInf-sup condition makes the associated operator's range closed#✓fully proved

The inf–sup condition makes the range of bilinearFormSharp B closed.

theorem sharp_isClosed_range {B : E →L[ℝ] F →L[ℝ] ℝ} (hB : IsInfSup B) :
    IsClosed ((bilinearFormSharp B).range : Set F)

Uses 3 · Used by 1

Statement usesInf-sup condition · Operator associated to a bounded bilinear form

Proof usesInf-sup condition makes the associated operator antilipschitz

Used byInf-sup and nondegeneracy make the associated operator surjective

TheoremInf-sup and nondegeneracy make the associated operator surjective#✓fully proved

The inf–sup condition plus nondegeneracy make bilinearFormSharp B surjective: the orthogonal complement of its range is trivial, and a closed subspace of a Hilbert space with trivial orthogonal complement is everything.

theorem sharp_range_eq_top {B : E →L[ℝ] F →L[ℝ] ℝ} (hInf : IsInfSup B)
    (hNondeg : IsNondegenerate B) : (bilinearFormSharp B).range = ⊤

Uses 4 · Used by 1

Statement usesInf-sup condition · Nondegeneracy in the second variable · Operator associated to a bounded bilinear form

Proof usesInf-sup condition makes the associated operator's range closed

Used byBanach–Nečas–Babuška isomorphism

DefinitionBanach–Nečas–Babuška isomorphism#✓fully proved

The Banach–Nečas–Babuška isomorphism: the operator associated to a bilinear form satisfying the inf–sup condition and nondegeneracy is a continuous linear equivalence.

noncomputable def sharpEquiv {B : E →L[ℝ] F →L[ℝ] ℝ} (hInf : IsInfSup B)
    (hNondeg : IsNondegenerate B) : E ≃L[ℝ] F :=
  ContinuousLinearEquiv.ofBijective (bilinearFormSharp B)
    (sharp_ker_eq_bot hInf) (sharp_range_eq_top hInf hNondeg)

Uses 5 · Used by 6

Statement usesInf-sup condition · Nondegeneracy in the second variable · Operator associated to a bounded bilinear form · Inf-sup condition makes the associated operator injective · Inf-sup and nondegeneracy make the associated operator surjective

Used byBanach–Nečas–Babuška theorem · Stability bound for the inf-sup variational problem · Norm of the Banach–Nečas–Babuška isomorphism applied to a vector · Pointwise inverse bound for the Banach–Nečas–Babuška isomorphism · Operator-norm bound for the inverse Banach–Nečas–Babuška isomorphism · Banach–Nečas–Babuška isomorphism is characterized by the form

TheoremBanach–Nečas–Babuška isomorphism is characterized by the form#✓fully proved

The equivalence sharpEquiv is characterized by the bilinear form.

@[simp]
theorem sharpEquiv_apply {B : E →L[ℝ] F →L[ℝ] ℝ} (hInf : IsInfSup B)
    (hNondeg : IsNondegenerate B) (x : E) (y : F) :
    ⟪sharpEquiv hInf hNondeg x, y⟫_ℝ = B x y

Uses 4

Statement usesInf-sup condition · Nondegeneracy in the second variable · Banach–Nečas–Babuška isomorphism

Proof usesOperator associated to a bounded bilinear form

TheoremNorm of the Banach–Nečas–Babuška isomorphism applied to a vector#✓fully proved

The norm of sharpEquiv applied to x is the dual norm of B x.

theorem norm_sharpEquiv_apply {B : E →L[ℝ] F →L[ℝ] ℝ} (hInf : IsInfSup B)
    (hNondeg : IsNondegenerate B) (x : E) :
    ‖sharpEquiv hInf hNondeg x‖ = ‖B x‖

Uses 4 · Used by 1

Statement usesInf-sup condition · Nondegeneracy in the second variable · Banach–Nečas–Babuška isomorphism

Proof usesOperator associated to a bounded bilinear form

Used byPointwise inverse bound for the Banach–Nečas–Babuška isomorphism

TheoremPointwise inverse bound for the Banach–Nečas–Babuška isomorphism#✓fully proved

Pointwise inverse bound for sharpEquiv: the inverse operator is bounded by β⁻¹ when β is an inf–sup constant.

theorem norm_sharpEquiv_symm_apply_le {B : E →L[ℝ] F →L[ℝ] ℝ} {β : ℝ} (hβ : 0 < β)
    (hB : ∀ x : E, β * ‖x‖ ≤ ‖B x‖) (hNondeg : IsNondegenerate B) (y : F) :
    ‖(sharpEquiv ⟨β, hβ, hB⟩ hNondeg).symm y‖ ≤ β⁻¹ * ‖y‖

Uses 3 · Used by 2

Statement usesNondegeneracy in the second variable · Banach–Nečas–Babuška isomorphism

Proof usesNorm of the Banach–Nečas–Babuška isomorphism applied to a vector

Used byStability bound for the inf-sup variational problem · Operator-norm bound for the inverse Banach–Nečas–Babuška isomorphism

TheoremOperator-norm bound for the inverse Banach–Nečas–Babuška isomorphism#✓fully proved

Operator-norm bound for the inverse: ‖(sharpEquiv)⁻¹‖ ≤ β⁻¹.

theorem norm_sharpEquiv_symm_le {B : E →L[ℝ] F →L[ℝ] ℝ} {β : ℝ} (hβ : 0 < β)
    (hB : ∀ x : E, β * ‖x‖ ≤ ‖B x‖) (hNondeg : IsNondegenerate B) :
    ‖((sharpEquiv ⟨β, hβ, hB⟩ hNondeg).symm : F →L[ℝ] E)‖ ≤ β⁻¹

Uses 3

Statement usesNondegeneracy in the second variable · Banach–Nečas–Babuška isomorphism

Proof usesPointwise inverse bound for the Banach–Nečas–Babuška isomorphism

DefinitionBanach–Nečas–Babuška theorem#✓fully proved

The Banach–Nečas–Babuška theorem: a bilinear form satisfying the inf–sup condition and nondegeneracy is itself a continuous linear equivalence E ≃L[ℝ] (F →L[ℝ] ℝ).

noncomputable def continuousLinearEquivOfBilinearForm {B : E →L[ℝ] F →L[ℝ] ℝ}
    (hInf : IsInfSup B) (hNondeg : IsNondegenerate B) : E ≃L[ℝ] (F →L[ℝ] ℝ) :=
  (sharpEquiv hInf hNondeg).trans (InnerProductSpace.toDual ℝ F).toContinuousLinearEquiv

Uses 3 · Used by 2

Statement usesInf-sup condition · Nondegeneracy in the second variable · Banach–Nečas–Babuška isomorphism

Used byBanach–Nečas–Babuška equivalence acts as the bilinear form · Unique solvability of the inf-sup variational problem

TheoremBanach–Nečas–Babuška equivalence acts as the bilinear form#✓fully proved

The equivalence continuousLinearEquivOfBilinearForm acts as B.

@[simp]
theorem continuousLinearEquivOfBilinearForm_apply {B : E →L[ℝ] F →L[ℝ] ℝ}
    (hInf : IsInfSup B) (hNondeg : IsNondegenerate B) (x : E) :
    continuousLinearEquivOfBilinearForm hInf hNondeg x = B x

Uses 3 · Used by 1

Statement usesInf-sup condition · Nondegeneracy in the second variable · Banach–Nečas–Babuška theorem

Used byUnique solvability of the inf-sup variational problem

TheoremUnique solvability of the inf-sup variational problem#✓fully proved

The variational problem B x y = φ y for all y has a unique solution.

theorem exists_unique_apply_eq {B : E →L[ℝ] F →L[ℝ] ℝ} (hInf : IsInfSup B)
    (hNondeg : IsNondegenerate B) (φ : F →L[ℝ] ℝ) :
    ∃! x : E, ∀ y : F, B x y = φ y

Uses 4

Statement usesInf-sup condition · Nondegeneracy in the second variable

Proof usesBanach–Nečas–Babuška theorem · Banach–Nečas–Babuška equivalence acts as the bilinear form

TheoremStability bound for the inf-sup variational problem#✓fully proved

The variational problem has a solution with the stability bound ‖x‖ ≤ β⁻¹ * ‖φ‖.

theorem exists_apply_eq_and_norm_le {B : E →L[ℝ] F →L[ℝ] ℝ} {β : ℝ} (hβ : 0 < β)
    (hB : ∀ x : E, β * ‖x‖ ≤ ‖B x‖) (hNondeg : IsNondegenerate B)
    (φ : F →L[ℝ] ℝ) :
    ∃ x : E, (∀ y : F, B x y = φ y) ∧ ‖x‖ ≤ β⁻¹ * ‖φ‖

Uses 4

Statement usesNondegeneracy in the second variable

Proof usesOperator associated to a bounded bilinear form · Pointwise inverse bound for the Banach–Nečas–Babuška isomorphism · Banach–Nečas–Babuška isomorphism

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.