Uniqueness of the weak gradient on an open set

Two weak gradients of one function differ by a function orthogonal to every test function, and on an open set the fundamental lemma of the calculus of variations kills it. Mathlib has the lemma as IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero.

Uniqueness is what lets separate structures be assembled into one family. Higher interior regularity is proved order by order, so a solution with derivatives of every order arrives as one family per order, with nothing relating them; uniqueness identifies the entries they share, and a single family closed under differentiation follows.

Main declarations

• EllipticPdes.Embedding.hasWeakGradOn_unique_ae: two weak gradients of one function agree almost everywhere on an open set.

theorem EllipticPdes.Embedding.hasWeakGradOn_unique_ae {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} (hBo : IsOpen B) (hBm : MeasurableSet B) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g g' : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hg : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) B MeasureTheory.volume) (hg' : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g' k) B MeasureTheory.volume) (h : HasWeakGradOn B u g) (h' : HasWeakGradOn B u g') (k : Fin d) : g k =ᵐ[MeasureTheory.volume.restrict B] g' k

Uniqueness of the weak gradient on an open set. Two weak gradients of the same function agree almost everywhere, given integrability on the set, which is what the fundamental lemma of the calculus of variations asks of the difference.

Integrability rather than local integrability is asked for because the only sets this is applied to are balls, where an L² class supplies it, and because the splitting of the test integral needs it anyway.