MATHLIBANNEX / CANONICAL DECLARATION CARD

Local almost-everywhere constancy from the weak equation

MathlibAnnex.WeakDivergenceZero.nonempty_localAEConstantAt

theorem

Turns constant mollifications into one almost-everywhere constant by choosing a common convergence point.

Statement

Let be a finite-dimensional real normed vector space with its Borel structure and an additive Haar measure . Let be open and locally integrable on . Assume for every vector field for which a compact set satisfies Here . For every , there are an open set and a real number with

Assumptions

The domain need not be connected, bounded, or of finite measure. There is no global integrability, Lipschitz, or continuity assumption on . No positive-dimension hypothesis is imposed. A point is supplied, so the conclusion is local; if is empty, there is no such point to consider.

Conclusion

The conclusion provides an open neighborhood of the prescribed point , with , and a real constant such that almost everywhere on . It does not assert at the originally supplied point, which might be exceptional.

The construction below uses the inner ball , the compact carrier , and the intermediate ball . All inclusions and compactness assertions follow from the chosen ball data and finite dimensionality. The same localized function and the same kernel sequence are used throughout.

Proof route

Localize to a compact ball. The weak equation makes every derivative of each smooth mollification zero on the inner ball, hence each mollification is constant there. Almost-everywhere convergence at one fixed good point forces these constants to converge. Uniqueness of limits then identifies the value at almost every other point.

Proof steps

  1. Choose a compact localization. The local-ball existence lemma, applied to openness at , permits choosing with . Put

    The inner ball is open, contains , and lies in . The closed ball is compact and measurable. Local integrability on gives integrability on , so is globally integrable and therefore locally integrable on . In particular on , also almost everywhere for .

  2. Use one shrinking sequence of kernels. Choose normalized smooth bumps centered at zero with inner radius and outer radius . In particular,

    These functions are smooth by the compact-kernel convolution theorem. The radii satisfy and . The normalized-bump convergence theorem for locally integrable functions therefore gives

    The hypotheses are precisely local integrability of , shrinking outer radii, and a uniform bound on the ratio of outer to inner radius.

  3. Make every mollification constant on the inner ball. Apply the vanishing-directional-derivative theorem to this open , this local ball data, the given local integrability, and the weak equation. It gives

    Thus is the zero linear functional. The ball is convex, hence preconnected, and is differentiable there. Thus the constancy theorem for each local mollification applies; its proof uses zero-derivative constancy on the open preconnected ball and supplies a real number such that

    This is pointwise constancy of each smooth mollification, not yet a statement about the limit .

  4. Choose a single point at which the whole sequence converges. The nonempty open ball has positive Haar measure. Restrict the almost-everywhere convergence in Step 2 to and intersect it with almost-everywhere membership in the measurable set . The inner-ball convergence-point lemma therefore supplies one at which the entire sequence converges. Set . Then

    This fixed good point is the reason the constants converge. We neither assume that converges nor choose a different exceptional-set witness for each .

  5. Pass to almost every other point and undo localization. For almost every with respect to , Step 2 gives and . Step 3 gives for every . Step 4 and uniqueness of real limits therefore imply

    Since on , this gives almost everywhere for . Taking supplies all the promised local data.

Main citations

Lean source signature (exact)

theorem WeakDivergenceZero.nonempty_localAEConstantAt
    {U : Set E} {u : E → ℝ} (hweak : WeakDivergenceZero μ U u)
    (hU : IsOpen U) (hu : LocallyIntegrableOn u U μ)
    {x : E} (hx : x ∈ U) : Nonempty (LocalAEConstantAt μ U u x)
In the source Mathematical meaning
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [μ.IsAddHaarMeasure] The finite-dimensional real normed space , with Borel measurable structure and additive Haar measure . Dimension zero is allowed.
(hweak : WeakDivergenceZero μ U u) The scalar weak equation for every vector field with a compact carrier contained in ; .
(hU : IsOpen U) (hu : LocallyIntegrableOn u U μ) The set is open and is locally integrable on . Whole-space integrability or Lipschitz continuity of is not assumed.
{x : E} (hx : x ∈ U) The requested point , which itself may be exceptional for an a.e. equality.
Nonempty (LocalAEConstantAt μ U u x) The conclusion is existence of a local record, with the six fields decoded below; it does not choose an arbitrary previously specified neighbourhood.
neighborhood The selected neighbourhood of ; this and the next five rows read the separately cited local record.
isOpen_neighborhood is open in the ambient topology.
mem_neighborhood The specified point satisfies .
neighborhood_subset .
In the source Mathematical meaning
constant One value for this neighbourhood.
ae_eq for -almost every . The same occur in these six fields.
Exact surrounding binder context (separate excerpts)

Exact source lines 7–12:

noncomputable section
open Set MeasureTheory TopologicalSpace
namespace MathlibAnnex
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
variable {μ : Measure E} [μ.IsAddHaarMeasure]

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

Exact content identity

Declaration: MathlibAnnex.WeakDivergenceZero.nonempty_localAEConstantAt

Accepted content SHA-256: a26a423bf64eda9884ab3d44deb8c12d8ab30eed12d3051d2626690322b0d158

Accepted source guide SHA-256: 87bd8f1e12997df114ea605364f4db3312b70b2166163623f6dc20359a69e14a

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑