Characterisation of H⁻¹(Ω)

Evans §5.9.1, Theorem 1.

H⁻¹(Ω) is the topological dual of H₀¹(Ω); in the graph encoding it is the type H01 Ω →L[ℝ] ℝ. The characterisation theorem says every f ∈ H⁻¹(Ω) is represented by an (n+1)-tuple (f₀, f₁, …, fₙ) of L²(Ω) functions through the pairing

⟨f, v⟩ = ∫_Ω (f₀ v - ∑ᵢ fᵢ ∂ᵢv),

and that ‖f‖_{H⁻¹} is the infimum of the tuple norms (∫_Ω ∑ᵢ |fᵢ|²)^{1/2} over all such representations, attained at the Riesz representative.

In the graph encoding a tuple of L² functions is an element F of the ambient space H1amb Ω = PiLp 2 (fun _ : Fin (d+1) => L2D Ω), and its PiLp norm is the tuple norm (∑ᵢ ‖Fᵢ‖²_{L²})^{1/2} = (∫_Ω ∑ᵢ |fᵢ|²)^{1/2}. The sign convention is the gradient flip F ↦ (F₀, -F₁, …, -Fₙ), a norm-preserving involution gradFlip, under which the representation property becomes f v = ⟪gradFlip F, v⟫ in H1amb Ω. The proof is then the Riesz representation theorem on the Hilbert space H₀¹(Ω):

• existence with ‖F‖ = ‖f‖: flip the Riesz representative of f;
• minimality: any representing tuple G gives f as ⟪gradFlip G, ·⟫ restricted to H₀¹, so ‖f‖ ≤ ‖gradFlip G‖ = ‖G‖ by Cauchy-Schwarz.

The L² ⊆ H⁻¹ embedding l2Functional (Evans §5.9.1, Theorem 1(iii)) is the instance with the tuple (f, 0, …, 0).

Gradient flip

noncomputable def EllipticPdes.gradFlip {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.H1amb Ω) : Sobolev.H1amb Ω

The sign convention adopted here: flip the gradient coordinates, keeping the function coordinate. A norm-preserving involution of the ambient space.

Equations

• EllipticPdes.gradFlip F = WithLp.toLp 2 (Fin.cons (F.ofLp 0) fun (i : Fin d) => -F.ofLp i.succ)

@[simp]

theorem EllipticPdes.gradFlip_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.H1amb Ω) : (gradFlip F).ofLp 0 = F.ofLp 0

Simp lemma: the gradient flip fixes the function coordinate, (gradFlip F) 0 = F 0.

@[simp]

theorem EllipticPdes.gradFlip_succ {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.H1amb Ω) (i : Fin d) : (gradFlip F).ofLp i.succ = -F.ofLp i.succ

Simp lemma: (gradFlip F) i.succ = -(F i.succ).

theorem EllipticPdes.gradFlip_gradFlip {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.H1amb Ω) : gradFlip (gradFlip F) = F

The gradient flip is an involution.

theorem EllipticPdes.norm_gradFlip {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.H1amb Ω) : ‖gradFlip F‖ = ‖F‖

The gradient flip preserves the ambient (tuple) norm.

theorem EllipticPdes.inner_gradFlip_left {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F V : Sobolev.H1amb Ω) : inner ℝ (gradFlip F) V = inner ℝ (F.ofLp 0) (V.ofLp 0) - ∑ i : Fin d, inner ℝ (F.ofLp i.succ) (V.ofLp i.succ)

Pairing a flipped tuple against an ambient vector is exactly the signed sum of our sign convention: function term minus gradient terms.

Representations of functionals by L² tuples

def EllipticPdes.IsHnegRepr {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (F : Sobolev.H1amb Ω) (f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) : Prop

The tuple F = (f₀, f₁, …, fₙ) of L²(Ω) functions represents the functional f ∈ H⁻¹(Ω) when ⟨f, v⟩ = ⟪f₀, v₀⟫ - ∑ᵢ ⟪fᵢ, ∂ᵢv⟫ for every v ∈ H₀¹(Ω), the inner-product form of the minus-sign convention adopted here.

Equations

• EllipticPdes.IsHnegRepr Ω F f = ∀ (v : ↥(EllipticPdes.Sobolev.H01 Ω)), f v = inner ℝ (F.ofLp 0) ((↑v).ofLp 0) - ∑ i : Fin d, inner ℝ (F.ofLp i.succ) ((↑v).ofLp i.succ)

theorem EllipticPdes.isHnegRepr_iff_inner {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.H1amb Ω) (f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) : IsHnegRepr Ω F f ↔ ∀ (v : ↥(Sobolev.H01 Ω)), f v = inner ℝ (gradFlip F) ↑v

A tuple represents f exactly when its gradient flip is an ambient Riesz vector for f on H₀¹.

theorem EllipticPdes.inner_L2_eq_integral {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (a b : Sobolev.L2D Ω) : inner ℝ a b = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑a x * ↑↑b x

The L² inner product on Ω as an integral, for restating representations in integral form.

theorem EllipticPdes.isHnegRepr_iff_integral {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F : Sobolev.H1amb Ω) (f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) : IsHnegRepr Ω F f ↔ ∀ (v : ↥(Sobolev.H01 Ω)), f v = (∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑(F.ofLp 0) x * ↑↑((↑v).ofLp 0) x) - ∑ i : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑(F.ofLp i.succ) x * ↑↑((↑v).ofLp i.succ) x

The representation property in integral form: ⟨f, v⟩ = ∫_Ω f₀ v - ∑ᵢ ∫_Ω fᵢ ∂ᵢv.

theorem EllipticPdes.exists_isHnegRepr_norm_eq {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) : ∃ (F : Sobolev.H1amb Ω), IsHnegRepr Ω F f ∧ ‖F‖ = ‖f‖

Existence of a norm-attaining representation. The gradient flip of the Riesz representative of f on the Hilbert space H₀¹(Ω) represents f with tuple norm exactly ‖f‖_{H⁻¹}.

theorem EllipticPdes.norm_le_of_isHnegRepr {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {F : Sobolev.H1amb Ω} {f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ} (hF : IsHnegRepr Ω F f) : ‖f‖ ≤ ‖F‖

Minimality. Every representing tuple dominates the dual norm: ‖f‖_{H⁻¹} ≤ (∫_Ω ∑ᵢ |fᵢ|²)^{1/2}, by Cauchy-Schwarz against the flipped tuple.

theorem EllipticPdes.hneg_norm_isLeast {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) : IsLeast {r : ℝ | ∃ (F : Sobolev.H1amb Ω), IsHnegRepr Ω F f ∧ ‖F‖ = r} ‖f‖

Dual norm as the least tuple norm. The set of norms of representing tuples has ‖f‖_{H⁻¹} as a member (the Riesz representative) and as a lower bound (minimality): the infimum is attained.

theorem EllipticPdes.hneg_norm_eq_sInf {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) : ‖f‖ = sInf {r : ℝ | ∃ (F : Sobolev.H1amb Ω), IsHnegRepr Ω F f ∧ ‖F‖ = r}

‖f‖_{H⁻¹} as the infimum of the tuple norms over all representations of f.

Terminal result of the library, the infimum form of hneg_norm_isLeast. Nothing else consumes it.

theorem EllipticPdes.hneg_characterization {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) : ∃ (F : Sobolev.H1amb Ω), (∀ (v : ↥(Sobolev.H01 Ω)), f v = (∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑(F.ofLp 0) x * ↑↑((↑v).ofLp 0) x) - ∑ i : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑(F.ofLp i.succ) x * ↑↑((↑v).ofLp i.succ) x) ∧ ‖F‖ = ‖f‖ ∧ ∀ (G : Sobolev.H1amb Ω), (∀ (v : ↥(Sobolev.H01 Ω)), f v = (∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑(G.ofLp 0) x * ↑↑((↑v).ofLp 0) x) - ∑ i : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑(G.ofLp i.succ) x * ↑↑((↑v).ofLp i.succ) x) → ‖F‖ ≤ ‖G‖

Characterisation of H⁻¹(Ω) (Evans §5.9.1, Theorem 1, in the sign convention adopted here). Every continuous linear functional f on H₀¹(Ω) is represented by a tuple F = (f₀, f₁, …, fₙ) of L²(Ω) functions through ⟨f, v⟩ = ∫_Ω f₀ v - ∑ᵢ ∫_Ω fᵢ ∂ᵢv, whose tuple norm (∫_Ω ∑ᵢ |fᵢ|²)^{1/2} = ‖F‖ equals ‖f‖_{H⁻¹} and is least among all representing tuples: the infimum is attained at the Riesz representative.

Terminal result of the library, stated in the manuscript. Nothing else consumes it.

L² ⊆ H⁻¹ embedding

theorem EllipticPdes.isHnegRepr_single_l2Functional {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (f : Sobolev.L2D Ω) : IsHnegRepr Ω (PiLp.single 2 0 f) (l2Functional Ω f)

The L² ⊆ H⁻¹ embedding (Evans §5.9.1, Theorem 1(iii)) is the representation by the tuple (f, 0, …, 0): a single L² function with no gradient terms.