MathlibAnnex.WeakDivergenceZero.exists_eqOn
theorem
Removes the exceptional set using continuity and positivity of open sets.
Statement
Let be a finite-dimensional real normed vector space with its Borel structure and an additive Haar measure . Let be open and preconnected. Let be locally integrable and continuous on , and suppose for every vector field for which a compact set satisfies Here . Then there is such that
Assumptions
Preconnectedness means that has no partition into two disjoint nonempty relatively open subsets; the empty set is allowed. In addition to openness, this condition, local integrability on , and the weak equation, continuity is required only on . The ambient space may have dimension zero. No global regularity, boundedness, or normalization of Haar measure is required.
Conclusion
The same constant obtained by the almost-everywhere theorem works pointwise on . There is no assertion about values outside .
Pointwise equality and almost-everywhere equality are different conclusions. The upgrade here uses both continuity and the positive measure of every nonempty open subset; the weak equation alone does not justify changing values on an exceptional set into pointwise information.
Proof route
First obtain a common constant almost everywhere. If a point had a different value, continuity would create a nonempty open neighborhood of different values, contradicting almost-everywhere equality.
Proof steps
Fix the almost-everywhere constant. Apply the global almost-everywhere constancy theorem to openness, preconnectedness, local integrability, and the weak equation. It gives a real with
This step does not use continuity.
Exclude any exceptional point. The open-set continuity lemma applies to and the constant function with this same : both are continuous on the open set , they agree almost everywhere there, and every nonempty open set has positive measure. Its contradiction argument is as follows. Suppose and . Set . Continuity on the open set provides an open neighborhood of , contained in , such that for all . Then
The almost-everywhere equality restricted to says there almost everywhere. But is nonempty and open, so and it contains a point satisfying that equality, a contradiction. Thus no such exists and on . If is empty, the pointwise conclusion is vacuous.
Main citations
- Exact
declaration and its source —
MathlibAnnex.WeakDivergenceZero.exists_eqOn - The
same weak hypotheses give an a.e. constant —
MathlibAnnex.WeakDivergenceZero.exists_aeConstantOn - Equality
everywhere from a.e. equality on an open set —
MeasureTheory.Measure.eqOn_open_of_ae_eq
Lean source signature (exact)
theorem WeakDivergenceZero.exists_eqOn
{U : Set E} {u : E → ℝ} (hweak : WeakDivergenceZero μ U u)
(hU : IsOpen U) (hUc : IsPreconnected U) (hu : LocallyIntegrableOn u U μ)
(hcont : ContinuousOn u U) : ∃ c : ℝ, Set.EqOn u (fun _ => c) U| 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. |
(hUc : IsPreconnected U) |
The domain is preconnected and may be empty. |
| In the source | Mathematical meaning |
|---|---|
(hcont : ContinuousOn u U) |
The extra assumption is ordinary continuity of on , not a.e. continuity or global continuity. |
∃ c : ℝ, Set.EqOn u (fun _ => c) U |
There exists one real
with
for every
.
fun _ => c is the constant function and
EqOn quantifies pointwise on
. |
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_eqOn
Accepted content SHA-256: c3b9910b26ffee458232ba0247b83cbe8decac623616d870480cff8481d8c2e6
Accepted source guide SHA-256: f8158618bd8f1f8986c7790011350a07218014fb772889a6977df8bc59261760
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73