Exact source: MathlibAnnex/Analysis/Distribution/WeakGradient/Basic.lean
Pinned GitHub source · Raw UTF-8 source
Back to Vanishing weak gradient tested by divergence · Back to Local almost-everywhere constancy from the weak equation · Back to Zero weak gradient gives zero derivatives of local mollifications
1import MathlibAnnex.Analysis.Distribution.Divergence2import MathlibAnnex.MeasureTheory.Function.AEConstant3import Mathlib.MeasureTheory.Integral.Bochner.Basic45noncomputable section6open Set MeasureTheory7namespace MathlibAnnex8variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]9 [MeasurableSpace E]1011/-- Vanishing weak gradient, tested by compact C¹ vector fields on a12finite-dimensional real normed space. The finite-dimensional instance is part13of the public declaration type. Local integrability remains a separate14required hypothesis of the rigidity theorem; this integral equation alone is15not a substitute for local integrability. -/16def WeakDivergenceZero [FiniteDimensional ℝ E]17 (μ : Measure E) (U : Set E) (u : E → ℝ) : Prop :=18 ∀ W : CompactC1VectorField E, W.carrier ⊆ U →19 ∫ y in U, u y * divergence W y ∂μ = 02021end MathlibAnnex