AcceptedTheorem · Statement with omitted proof

Equivalence of variational equations and energy minimization

A symmetric positive-definite variational problem is equivalent to minimizing its quadratic energy.

Larsson & Thomée ↗
Theorem A.2 · printed p. 229

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

A symmetric positive-definite variational problem is equivalent to minimizing its quadratic energy.

a(u,v)=L(v)\ \text{for all }v\quad\Longleftrightarrow\quad F(u)\le F(v)\ \text{for all }v,\quad F(v)=\tfrac12a(v,v)-L(v).

Assumptions & context

A real Hilbert-space setting, a symmetric positive-definite bilinear form, and a bounded linear functional.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem A.2 · printed p. 229

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem thm_A_2 (a : LinearMap.BilinForm ℝ V) (L : V →L[ℝ] ℝ)
    (ha_symm : IsSymmetricForm a) (ha_pos : IsPositiveDefiniteForm a) (u : V) :
    SatisfiesA11 a L u ↔ ∀ v : V, energyF a L u ≤ energyF a L v := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomeeA2

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]

/-- Symmetry of a bilinear form: `a(u,v) = a(v,u)` for all `u, v`. -/
def IsSymmetricForm (a : LinearMap.BilinForm ℝ V) : Prop :=
  ∀ u v : V, a u v = a v u

/-- Positive definiteness of a bilinear form: `a(v,v) > 0` for all `v ≠ 0`. -/
def IsPositiveDefiniteForm (a : LinearMap.BilinForm ℝ V) : Prop :=
  ∀ v : V, v ≠ 0 → 0 < a v v

/-- The variational problem (A.11): `a(u,v) = L(v)` for all `v ∈ V`. -/
def SatisfiesA11 (a : LinearMap.BilinForm ℝ V) (L : V →L[ℝ] ℝ) (u : V) : Prop :=
  ∀ v : V, a u v = L v

/-- The energy functional of (A.15): `F(v) = ½ a(v,v) - L(v)`. -/
def energyF (a : LinearMap.BilinForm ℝ V) (L : V →L[ℝ] ℝ) (v : V) : ℝ :=
  (1 / 2 : ℝ) * a v v - L v

/-- Theorem A.2 (Larsson–Thomée). If `a` is a symmetric, positive definite bilinear form and
`L` is a bounded linear form on the Hilbert space `V`, then `u ∈ V` satisfies (A.11) if and
only if `F(u) ≤ F(v)` for all `v ∈ V`, where `F(v) = ½ a(v,v) - L(v)` (A.15). -/
theorem thm_A_2 (a : LinearMap.BilinForm ℝ V) (L : V →L[ℝ] ℝ)
    (ha_symm : IsSymmetricForm a) (ha_pos : IsPositiveDefiniteForm a) (u : V) :
    SatisfiesA11 a L u ↔ ∀ v : V, energyF a L u ≤ energyF a L v := by
  sorry

end PDETextbook.LarssonThomeeA2

How to read the formalization

This is an equivalence for a proposed solution; the separate Lax–Milgram statement supplies existence under boundedness and coercivity.

← Back to all statements