Strang's lemma

TheoremStrang's first lemma#✓fully proved

Strang's first lemma (pointwise form): if u solves the exact variational problem B u w = ℓ w and uh solves the perturbed problem Bh uh w = ℓh w on the discrete space V (embedded by the linear isometry J), and Bh is coercive with constant α, then for every competitor vh : V the error ‖u - J uh‖ is bounded by the best-approximation error of u at vh plus the consistency errors. Here Bh - B.bilinearComp J J measures the bilinear-form crime and ℓh - ℓ.comp J measures the functional crime.

theorem strang_first_lemma
    {B : E →L[ℝ] E →L[ℝ] ℝ} {Bh : V →L[ℝ] V →L[ℝ] ℝ}
    {ℓ : E →L[ℝ] ℝ} {ℓh : V →L[ℝ] ℝ} {J : V →ₗᵢ[ℝ] E}
    {α : ℝ} (hα : 0 < α) (hco : ∀ v, α * ‖v‖ * ‖v‖ ≤ Bh v v)
    {u : E} {uh : V} (hu : ∀ w, B u w = ℓ w) (huh : ∀ w, Bh uh w = ℓh w)
    (vh : V) :
    ‖u - J uh‖ ≤ (1 + (‖B‖ + ‖Bh - B.bilinearComp J.toContinuousLinearMap
        J.toContinuousLinearMap‖) / α) * ‖u - J vh‖
      + (‖ℓh - ℓ.comp J.toContinuousLinearMap‖
        + ‖Bh - B.bilinearComp J.toContinuousLinearMap
          J.toContinuousLinearMap‖ * ‖u‖) / α

Used by 1

Used byStrang's first lemma

TheoremStrang's first lemma#✓fully proved

Strang's first lemma (infimum form): the error is bounded by the best-approximation error ⨅ vh : V, ‖u - J vh‖ plus the consistency errors.

theorem strang_first_lemma_iInf
    {B : E →L[ℝ] E →L[ℝ] ℝ} {Bh : V →L[ℝ] V →L[ℝ] ℝ}
    {ℓ : E →L[ℝ] ℝ} {ℓh : V →L[ℝ] ℝ} {J : V →ₗᵢ[ℝ] E}
    {α : ℝ} (hα : 0 < α) (hco : ∀ v, α * ‖v‖ * ‖v‖ ≤ Bh v v)
    {u : E} {uh : V} (hu : ∀ w, B u w = ℓ w) (huh : ∀ w, Bh uh w = ℓh w) :
    ‖u - J uh‖ ≤ (1 + (‖B‖ + ‖Bh - B.bilinearComp J.toContinuousLinearMap
        J.toContinuousLinearMap‖) / α) * (⨅ vh : V, ‖u - J vh‖)
      + (‖ℓh - ℓ.comp J.toContinuousLinearMap‖
        + ‖Bh - B.bilinearComp J.toContinuousLinearMap
          J.toContinuousLinearMap‖ * ‖u‖) / α

Uses 1

Proof usesStrang's first lemma

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.