Uniqueness of the whole-space weak derivative

HasWeakDeriv k g g' (EllipticPdes.Regularity.DiffQuotientBound) pins g' only through its integrals against smooth compactly supported test functions. Those integrals determine g' as an L² class, because the test classes are dense in L²(ℝᵈ) (MeasureTheory.Lp.dense_hasCompactSupport_contDiff), so two weak k-derivatives of the same class agree.

The identification steps of higher interior regularity (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2) produce a second derivative twice, once as a limit of difference quotients and once through the Leibniz rule, and need them to be the same class. This file supplies that step.

Main declarations

• annihilates_of_forall_testCls: an L² class orthogonal to every smooth compactly supported class is zero.
• HasWeakDeriv.unique: the weak k-derivative is unique as an L² class.

theorem EllipticPdes.Regularity.annihilates_of_forall_testCls {d : ℕ} {w : ↥(MeasureTheory.EucL2 d)} (hw : ∀ (ρ : EuclideanSpace ℝ (Fin d) → ℝ), ContDiff ℝ (↑⊤) ρ → HasCompactSupport ρ → ∫ (x : EuclideanSpace ℝ (Fin d)), ↑↑w x * ρ x = 0) : w = 0

Vanishing of an L² class orthogonal to every test class. The classes of smooth compactly supported functions are dense in L²(ℝᵈ), and y ↦ ⟪w, y⟫ is continuous, so a pairing that vanishes on that family vanishes everywhere, in particular against w itself.

theorem EllipticPdes.Regularity.HasWeakDeriv.unique {d : ℕ} {k : Fin d} {g w₁ w₂ : ↥(MeasureTheory.EucL2 d)} (h₁ : HasWeakDeriv k g w₁) (h₂ : HasWeakDeriv k g w₂) : w₁ = w₂

Uniqueness of the whole-space weak derivative. Two L² weak k-derivatives of the same class coincide: their difference is orthogonal to every smooth compactly supported test class, hence zero by annihilates_of_forall_testCls.