MATHLIBANNEX / CANONICAL DECLARATION CARD

Global almost-everywhere constancy on a preconnected domain

MathlibAnnex.WeakDivergenceZero.exists_aeConstantOn

theorem

Combines local weak-gradient rigidity with topological and countable gluing.

Statement

Let be a finite-dimensional real normed vector space with its Borel structure and an additive Haar measure . Let be open and preconnected, and let be locally integrable on . Suppose for every vector field for which a compact set satisfies Here . Then there exists such that

Assumptions

Preconnectedness means that cannot be partitioned into two disjoint nonempty relatively open subsets. It permits ; nonemptiness is not required. The dimension of may be zero. The assumptions are local integrability on and the weak test equation, together with openness and preconnectedness. There is no bounded-domain, positive-dimension, global , Lipschitz, or continuity hypothesis.

Conclusion

There is one constant on the whole domain in the restricted almost-everywhere sense. Continuity would be an additional assumption for pointwise equality. The empty domain admits any constant, for example zero.

Finite-dimensional normed spaces are second countable, so every subset is Lindelöf. Additive Haar measure is positive on nonempty open sets. These two consequences of the ambient hypotheses supply the topological gluing theorem’s hypotheses; they are not additional restrictions on .

Proof route

Obtain local almost-everywhere data from the weak equation, then apply the preconnected version of the general gluing theorem. That version handles the empty domain separately.

Proof steps

  1. Produce local data. At every , the local weak-gradient constancy theorem applies to the given hypotheses: the same open , local integrability, and weak equation. It supplies an open and with

    No connectedness assumption is needed for this local step.

  2. Check and apply the global hypotheses. The measure is positive on nonempty open sets by its Haar property. Second countability of supplies the Lindelöf property of . If is empty, and works. If is nonempty, preconnectedness together with nonemptiness makes it connected. The connected local-to-global gluing theorem now applies to the data in Step 1 and gives

    Within that theorem, positive open overlaps identify constants, connectedness propagates a fixed constant, and a countable subcover permits measure-theoretic gluing. The preconnected gluing theorem used in the exact proof combines these two cases; it uses nonemptiness of the codomain, here supplied by .

Main citations

Lean source signature (exact)

theorem WeakDivergenceZero.exists_aeConstantOn
    {U : Set E} {u : E → ℝ} (hweak : WeakDivergenceZero μ U u)
    (hU : IsOpen U) (hUc : IsPreconnected U) (hu : LocallyIntegrableOn u U μ) :
    ∃ c : ℝ, AEConstantOn μ u U c
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.
In the source Mathematical meaning
(hUc : IsPreconnected U) The set admits no partition into two disjoint nonempty relatively open subsets. It may be empty.
∃ c : ℝ, AEConstantOn μ u U c There is one real such that almost everywhere for . This is the restricted a.e. conclusion, not pointwise equality.
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.exists_aeConstantOn

Accepted content SHA-256: da4869ee31e90d1ecb36f261ae536a47cf7c036ad939cf2fc7aa54baea534bf0

Accepted source guide SHA-256: b5fd40e9b66a265ee25a744293adb0245db63c0bfbc898bb4a3f6ea9f8a628ae

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑