Céa's lemma

DefinitionRestriction of a bilinear form to a subspace#✓fully proved

Restriction of a bounded bilinear form to a submodule.

noncomputable def restrictBilin (B : V →L[ℝ] V →L[ℝ] ℝ) (W : Submodule ℝ V) :
    W →L[ℝ] W →L[ℝ] ℝ where
  toFun x := (B x).comp W.subtypeL
  map_add' x y := by
    ext z
    simp [map_add]
  map_smul' c x := by
    ext z
    simp [map_smul]
  cont := by
    fun_prop

Used by 4

Used byGalerkin solution · Galerkin solution is the unique solution of the Galerkin equations · Galerkin solution satisfies the Galerkin equations · Coercivity passes to restrictions to subspaces

TheoremCoercivity passes to restrictions to subspaces#✓fully proved

Coercivity is inherited by restriction to a submodule.

theorem isCoercive_restrictBilin {B : V →L[ℝ] V →L[ℝ] ℝ} {W : Submodule ℝ V}
    (hB : IsCoercive B) : IsCoercive (restrictBilin B W)

Uses 1 · Used by 3

Statement usesRestriction of a bilinear form to a subspace

Used byGalerkin solution · Galerkin solution is the unique solution of the Galerkin equations · Galerkin solution satisfies the Galerkin equations

DefinitionSolution of a coercive variational problem#✓fully proved

The solution of the variational problem B u w = L w for all w, obtained from the Lax–Milgram equivalence and the Riesz representation.

noncomputable def variationalSolution {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E] {B : E →L[ℝ] E →L[ℝ] ℝ}
    (hB : IsCoercive B) (L : E →L[ℝ] ℝ) : E :=
  hB.continuousLinearEquivOfBilin.symm ((InnerProductSpace.toDual ℝ E).symm L)

Used by 9

Used byExistence of a variational solution · Galerkin orthogonality · Galerkin solution · Galerkin solution satisfies the Galerkin equations · Céa's lemma · Céa's lemma · Stability bound for the variational solution · Variational solution is the unique solution · Variational solution satisfies the variational equation

TheoremVariational solution satisfies the variational equation#✓fully proved

The variational solution satisfies the variational equation.

theorem variationalSolution_spec {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E] {B : E →L[ℝ] E →L[ℝ] ℝ}
    (hB : IsCoercive B) (L : E →L[ℝ] ℝ) (w : E) :
    B (variationalSolution hB L) w = L w

Uses 1 · Used by 5

Statement usesSolution of a coercive variational problem

Used byExistence of a variational solution · Galerkin orthogonality · Galerkin solution satisfies the Galerkin equations · Stability bound for the variational solution · Variational solution is the unique solution

TheoremUniqueness for coercive variational problems#✓fully proved

Uniqueness for the variational problem: two vectors satisfying the same variational equation agree, by coercivity.

theorem eq_of_forall_bilin {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] {B : E →L[ℝ] E →L[ℝ] ℝ}
    (hB : IsCoercive B) {L : E →L[ℝ] ℝ} {x y : E}
    (hx : ∀ w, B x w = L w) (hy : ∀ w, B y w = L w) : x = y

Used by 2

Used byGalerkin solution is the unique solution of the Galerkin equations · Variational solution is the unique solution

TheoremVariational solution is the unique solution#✓fully proved

The variational solution is the unique solution of the variational equation.

theorem variationalSolution_eq_of_forall {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E] {B : E →L[ℝ] E →L[ℝ] ℝ}
    (hB : IsCoercive B) {L : E →L[ℝ] ℝ} {x : E}
    (hx : ∀ w, B x w = L w) : x = variationalSolution hB L

Uses 3

Statement usesSolution of a coercive variational problem

Proof usesUniqueness for coercive variational problems · Variational solution satisfies the variational equation

TheoremExistence of a variational solution#✓fully proved

Existence for the variational problem, in bare existential form.

theorem exists_variationalSolution {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E] {B : E →L[ℝ] E →L[ℝ] ℝ}
    (hB : IsCoercive B) (L : E →L[ℝ] ℝ) : ∃ u, ∀ w, B u w = L w

Uses 2

Proof usesSolution of a coercive variational problem · Variational solution satisfies the variational equation

DefinitionGalerkin solution#✓fully proved

The Galerkin solution in W: the solution of the variational problem for the restricted form and the restricted functional.

noncomputable def galerkinSolution {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) (L : V →L[ℝ] ℝ) : W :=
  @variationalSolution W _ _ hW.completeSpace_coe _
    (isCoercive_restrictBilin hB) (L.comp W.subtypeL)

Uses 3 · Used by 7

Statement usesCoercivity passes to restrictions to subspaces · Restriction of a bilinear form to a subspace · Solution of a coercive variational problem

Used byExistence of a Galerkin solution · Galerkin orthogonality · Galerkin solution is the unique solution of the Galerkin equations · Galerkin solution satisfies the Galerkin equations · Stability bound for the Galerkin solution · Céa's lemma · Céa's lemma

TheoremGalerkin solution satisfies the Galerkin equations#✓fully proved

The Galerkin solution satisfies the Galerkin equations.

theorem galerkinSolution_spec {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) (L : V →L[ℝ] ℝ) (w : W) :
    B (galerkinSolution hB hW L : V) (w : V) = L (w : V)

Uses 5 · Used by 4

Statement usesGalerkin solution

Proof usesCoercivity passes to restrictions to subspaces · Restriction of a bilinear form to a subspace · Solution of a coercive variational problem · Variational solution satisfies the variational equation

Used byExistence of a Galerkin solution · Galerkin orthogonality · Galerkin solution is the unique solution of the Galerkin equations · Stability bound for the Galerkin solution

TheoremGalerkin solution is the unique solution of the Galerkin equations#✓fully proved

The Galerkin solution is the unique element of W satisfying the Galerkin equations.

theorem galerkinSolution_eq_of_forall {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) {L : V →L[ℝ] ℝ} {x : W}
    (hx : ∀ w : W, B (x : V) (w : V) = L (w : V)) : x = galerkinSolution hB hW L

Uses 5

Statement usesGalerkin solution

Proof usesUniqueness for coercive variational problems · Galerkin solution satisfies the Galerkin equations · Coercivity passes to restrictions to subspaces · Restriction of a bilinear form to a subspace

TheoremExistence of a Galerkin solution#✓fully proved

Existence for the Galerkin problem, in bare existential form.

theorem exists_galerkinSolution {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) (L : V →L[ℝ] ℝ) :
    ∃ uh ∈ W, ∀ w ∈ W, B uh w = L w

Uses 2

Proof usesGalerkin solution · Galerkin solution satisfies the Galerkin equations

TheoremGalerkin orthogonality#✓fully proved

Galerkin orthogonality: the error u - u_h is B-orthogonal to W.

theorem galerkin_orthogonality {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) (L : V →L[ℝ] ℝ) (w : W) :
    B (variationalSolution hB L - (galerkinSolution hB hW L : V)) (w : V) = 0

Uses 4 · Used by 1

Statement usesGalerkin solution · Solution of a coercive variational problem

Proof usesGalerkin solution satisfies the Galerkin equations · Variational solution satisfies the variational equation

Used byCéa's lemma

TheoremCéa's lemma#✓fully proved

Céa's lemma (pointwise form): the Galerkin error is bounded by (‖B‖ / α) times the distance from u to any element v of W.

theorem norm_sub_galerkinSolution_le {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) (L : V →L[ℝ] ℝ)
    {α : ℝ} (hα : 0 < α) (hco : ∀ v, α * ‖v‖ * ‖v‖ ≤ B v v) (v : V) (hv : v ∈ W) :
    ‖variationalSolution hB L - (galerkinSolution hB hW L : V)‖
      ≤ (‖B‖ / α) * ‖variationalSolution hB L - v‖

Uses 3 · Used by 1

Statement usesGalerkin solution · Solution of a coercive variational problem

Proof usesGalerkin orthogonality

Used byCéa's lemma

TheoremCéa's lemma#✓fully proved

Céa's lemma (infimum form): the Galerkin error is bounded by (‖B‖ / α) times the best-approximation error ⨅ v : W, ‖u - v‖.

theorem norm_sub_galerkinSolution_le_iInf {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) (L : V →L[ℝ] ℝ)
    {α : ℝ} (hα : 0 < α) (hco : ∀ v, α * ‖v‖ * ‖v‖ ≤ B v v) :
    ‖variationalSolution hB L - (galerkinSolution hB hW L : V)‖
      ≤ (‖B‖ / α) * ⨅ v : W, ‖variationalSolution hB L - (v : V)‖

Uses 3

Statement usesGalerkin solution · Solution of a coercive variational problem

Proof usesCéa's lemma

TheoremStability bound for the variational solution#✓fully proved

Stability of the variational solution: ‖u‖ ≤ ‖L‖ / α.

theorem norm_variationalSolution_le {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    (L : V →L[ℝ] ℝ) {α : ℝ} (hα : 0 < α) (hco : ∀ v, α * ‖v‖ * ‖v‖ ≤ B v v) :
    ‖variationalSolution hB L‖ ≤ ‖L‖ / α

Uses 2

Statement usesSolution of a coercive variational problem

Proof usesVariational solution satisfies the variational equation

TheoremStability bound for the Galerkin solution#✓fully proved

Stability of the Galerkin solution: ‖u_h‖ ≤ ‖L‖ / α.

theorem norm_galerkinSolution_le {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
    {W : Submodule ℝ V} (hW : IsComplete (W : Set V)) (L : V →L[ℝ] ℝ)
    {α : ℝ} (hα : 0 < α) (hco : ∀ v, α * ‖v‖ * ‖v‖ ≤ B v v) :
    ‖galerkinSolution hB hW L‖ ≤ ‖L‖ / α

Uses 2

Statement usesGalerkin solution

Proof usesGalerkin solution satisfies the Galerkin equations

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.