Aubin–Nitsche lemma

TheoremTranspose of a coercive bilinear form is coercive#✓fully proved

The transpose of a coercive bilinear form is coercive with the same constant, since B.flip u u = B u u.

theorem isCoercive_flip {B : H →L[ℝ] H →L[ℝ] ℝ} (hB : IsCoercive B) :
    IsCoercive B.flip

Used by 1

Used byExistence for the adjoint problem

TheoremExistence for the adjoint problem#✓fully proved

If B is coercive, then for every e : H there is z : H with B v z = ⟪J e, J v⟫_ℝ for all v : H.

theorem exists_adjointSolution [CompleteSpace H] [CompleteSpace L]
    {B : H →L[ℝ] H →L[ℝ] ℝ} {J : H →L[ℝ] L} (hB : IsCoercive B) (e : H) :
    ∃ z : H, ∀ v : H, B v z = ⟪J e, J v⟫_ℝ

Uses 1

Proof usesTranspose of a coercive bilinear form is coercive

TheoremAubin–Nitsche lemma, pointwise form#✓fully proved

If e satisfies Galerkin orthogonality against Vh and z solves the adjoint problem, then for every competitor zh ∈ Vh, ‖J e‖² ≤ ‖B‖ * ‖e‖ * ‖z - zh‖.

theorem aubinNitsche_pointwise {B : H →L[ℝ] H →L[ℝ] ℝ} {J : H →L[ℝ] L}
    {e z : H} {Vh : Submodule ℝ H} {zh : H} (hzh : zh ∈ Vh)
    (horth : ∀ wh ∈ Vh, B e wh = 0) (hadj : ∀ v : H, B v z = ⟪J e, J v⟫_ℝ) :
    ‖J e‖ ^ 2 ≤ ‖B‖ * ‖e‖ * ‖z - zh‖

Used by 2

Used byAubin–Nitsche lemma, infimum form · Aubin–Nitsche lemma, rate form

TheoremAubin–Nitsche lemma, infimum form#✓fully proved

With the same hypotheses, ‖J e‖² ≤ ‖B‖ * ‖e‖ * Metric.infDist z Vh.

theorem aubinNitsche_core {B : H →L[ℝ] H →L[ℝ] ℝ} {J : H →L[ℝ] L}
    {e z : H} {Vh : Submodule ℝ H}
    (horth : ∀ wh ∈ Vh, B e wh = 0) (hadj : ∀ v : H, B v z = ⟪J e, J v⟫_ℝ) :
    ‖J e‖ ^ 2 ≤ ‖B‖ * ‖e‖ * Metric.infDist z (Vh : Set H)

Uses 1

Proof usesAubin–Nitsche lemma, pointwise form

TheoremAdjoint stability#✓fully proved

If B is coercive with constant α and ‖J‖ ≤ Cemb, then the adjoint solution satisfies α * ‖z‖ ≤ Cemb * ‖J e‖.

theorem adjointSolution_norm_le {B : H →L[ℝ] H →L[ℝ] ℝ} {J : H →L[ℝ] L}
    {α Cemb : ℝ} (hco : ∀ v : H, α * ‖v‖ * ‖v‖ ≤ B v v)
    (hJ : ‖J‖ ≤ Cemb) {e z : H} (hadj : ∀ v : H, B v z = ⟪J e, J v⟫_ℝ) :
    α * ‖z‖ ≤ Cemb * ‖J e‖

Used by 1

Used byAubin–Nitsche lemma, rate form

TheoremAubin–Nitsche lemma, rate form#✓fully proved

If in addition the adjoint solution is approximable in Vh with ‖z - zh‖ ≤ Capp * h * ‖z‖ for some zh ∈ Vh, then the weak-norm error gains the factor h: α * ‖J e‖ ≤ ‖B‖ * Cemb * Capp * h * ‖e‖.

theorem aubinNitsche_rate {B : H →L[ℝ] H →L[ℝ] ℝ} {J : H →L[ℝ] L}
    {Vh : Submodule ℝ H} {α Cemb Capp h : ℝ} (hα : 0 < α)
    (hco : ∀ v : H, α * ‖v‖ * ‖v‖ ≤ B v v) (hJ : ‖J‖ ≤ Cemb)
    (hCemb : 0 ≤ Cemb) (hCapp : 0 ≤ Capp) (hh : 0 ≤ h)
    {e z : H} (horth : ∀ wh ∈ Vh, B e wh = 0)
    (hadj : ∀ v : H, B v z = ⟪J e, J v⟫_ℝ)
    (happrox : ∃ zh ∈ Vh, ‖z - zh‖ ≤ Capp * h * ‖z‖) :
    α * ‖J e‖ ≤ ‖B‖ * Cemb * Capp * h * ‖e‖

Uses 2

Proof usesAdjoint stability · Aubin–Nitsche lemma, pointwise form

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.