Documentation

TauCeti.Analysis.InnerProductSpace.Lions

Lions' representation theorem #

Lax–Milgram solves B u v = ℓ v when the bilinear form B is defined and coercive on a single Hilbert space. Lions' representation theorem is the version in which the solution and the test vectors live in different spaces: the solution u is sought in a Hilbert space H, while the test vectors φ range over a vector space Φ, which need carry no topology, that is mapped into H by j. The form E φ u must be continuous in u for each fixed φ, and coercive on the diagonal, c p(φ)² ≤ E φ (j φ), for a function p : Φ → ℝ dominating ‖j φ‖ (in applications, a norm on Φ). Then every functional ℓ on Φ bounded by p is represented: there is u ∈ H with E φ u = ℓ φ for every φ.

Unlike Lax–Milgram, the theorem gives no uniqueness, and it needs neither continuity of E in φ nor completeness of the test space. This is what makes it applicable to evolution equations. For u' + A(t) u = f with u(0) = u₀ in a Gelfand triple V ↪ H ↪ V*, one takes L²(0, T; V) for the Hilbert space and the C¹ functions φ : ℝ → V with φ(T) = 0 for the test space, with E φ u = ∫ (A(t) u φ - ⟪u, φ'⟫): integrating by parts, E φ φ = ½ ‖φ(0)‖² + ∫ A(t) φ φ is coercive for p φ = (‖φ‖²_{L²(V)} + ‖φ(0)‖²)^{1/2}, which also bounds the right-hand side ℓ φ = ∫ f φ + ⟪u₀, φ(0)⟫ (TauCeti.exists_memLp_forall_setIntegral_eq_add_inner).

The proof #

By the Fréchet–Riesz theorem, E φ u = ⟪T φ, u⟫ for a linear map T : Φ → H. Coercivity and Cauchy–Schwarz give c p(φ)² ≤ ⟪T φ, j φ⟫ ≤ ‖T φ‖ p(φ), so c p(φ) ≤ ‖T φ‖, and therefore |ℓ φ| ≤ (M / c) ‖T φ‖. In particular ℓ vanishes on the kernel of T, so T φ ↦ ℓ φ is a well-defined functional on the range of T, of norm at most M / c. Its Hahn–Banach extension to H is represented, again by Fréchet–Riesz, by the vector u sought.

Main declarations #

References #

theorem LinearMap.exists_forall_apply_eq_and_norm_le_of_coercive {Φ : Type u_1} {H : Type u_2} [AddCommGroup Φ] [Module ℝ Φ] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (E : Φ →ₗ[ℝ] StrongDual ℝ H) (j : Φ → H) (p : Φ → ℝ) (ℓ : Φ →ₗ[ℝ] ℝ) {c M : ℝ} (hc : 0 < c) (hM : 0 ≤ M) (hE : ∀ (φ : Φ), c * p φ ^ 2 ≤ (E φ) (j φ)) (hj : ∀ (φ : Φ), ‖j φ‖ ≤ p φ) (hℓ : ∀ (φ : Φ), |ℓ φ| ≤ M * p φ) :
∃ (u : H), (∀ (φ : Φ), (E φ) u = ℓ φ) ∧ ‖u‖ ≤ M / c

Lions' representation theorem. Let H be a real Hilbert space, Φ a real vector space with a map j : Φ → H and a function p : Φ → ℝ dominating it, ‖j φ‖ ≤ p φ, and let E assign to each φ ∈ Φ a continuous linear functional on H that is coercive on the diagonal, c p(φ)² ≤ E φ (j φ) with c > 0. Then every linear functional ℓ on Φ with |ℓ φ| ≤ M p(φ) is represented by some u ∈ H, in the sense that E φ u = ℓ φ for every φ ∈ Φ, and u can be chosen with ‖u‖ ≤ M / c.

No continuity of E in φ, completeness of Φ or uniqueness of u is claimed; the test space Φ carries no topology at all.