Vanishing weak gradient tested by divergence

MathlibAnnex.WeakDivergenceZero

def

Expresses a weak equation through compactly supported continuously differentiable vector fields.

Statement

Let be a finite-dimensional real normed vector space equipped with a measurable structure, let be any measure on , let , and let . For a vector field , write for its real Fréchet derivative and . The weak equation considered here is for every vector field supplied with a compact carrier containing its nonzero set. The integral is with respect to .

Definition

Using , the complete condition is The source packages and together as a compact test field. Without integrability hypotheses, the integral has the total Bochner-integral convention; no distribution-theoretic regularity is silently added.

Assumptions

The predicate itself assumes no openness of , compatibility between the topology and measurable structure, Haar property of , or local integrability of . These are separate hypotheses in its analytic uses. The zero-dimensional case is included.

Conclusion

The result of the definition is a proposition about , , and . It asks for the displayed equality for every admissible pair , rather than for a derivative of . In the later Haar setting, with open and locally integrable on , the compact support and continuous bounded divergence make these test integrals ordinary integrable pairings.

Notes

A carrier is a chosen compact containing ; it need not equal that set or its closure. Since is Hausdorff, is closed and also contains . If , the field is zero on the open neighborhood , hence and . This neighborhood argument, not merely at one point, confines the divergence to .

def WeakDivergenceZero [FiniteDimensional ℝ E]
    (μ : Measure E) (U : Set E) (u : E → ℝ) : Prop :=
  ∀ W : CompactC1VectorField E, W.carrier ⊆ U →
    ∫ y in U, u y * divergence W y ∂μ = 0

noncomputable section
open Set MeasureTheory
namespace MathlibAnnex
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E]

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project