Exact source: MathlibAnnex/Analysis/Distribution/WeakGradient.lean
Pinned GitHub source · Raw UTF-8 source
Back to Almost-everywhere constancy of the sign on a preconnected target · Back to Global almost-everywhere constancy on a preconnected domain · Back to A continuous function with zero weak gradient is constant
1import MathlibAnnex.Analysis.Distribution.WeakGradient.Local23/-! Weak-gradient-zero rigidity on a finite-dimensional real normed space.4No choice of coordinates, positive dimension, bounded domain, or global5integrability assumption occurs in the conclusion. The parent RET2 source6was independently elaborated; this API-repair revision is qualified by the exact build evidence accompanying this source. -/7noncomputable section8open Set MeasureTheory TopologicalSpace9namespace MathlibAnnex10variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]11 [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]12variable {μ : Measure E} [μ.IsAddHaarMeasure]1314/-- Local conclusion on any open domain; no connectedness is needed. -/15theorem WeakDivergenceZero.nonempty_localAEConstantAt16 {U : Set E} {u : E → ℝ} (hweak : WeakDivergenceZero μ U u)17 (hU : IsOpen U) (hu : LocallyIntegrableOn u U μ)18 {x : E} (hx : x ∈ U) : Nonempty (LocalAEConstantAt μ U u x) :=19 WeakGradient.nonempty_localAEConstantAt hU hu hweak hx2021/-- Global a.e. constancy, including the empty-domain and zero-dimensional cases. -/22theorem WeakDivergenceZero.exists_aeConstantOn23 {U : Set E} {u : E → ℝ} (hweak : WeakDivergenceZero μ U u)24 (hU : IsOpen U) (hUc : IsPreconnected U) (hu : LocallyIntegrableOn u U μ) :25 ∃ c : ℝ, AEConstantOn μ u U c := by26 exact exists_aeConstantOn_of_local_preconnected μ hUc27 (HereditarilyLindelofSpace.isLindelof U)28 (fun _ hx => hweak.nonempty_localAEConstantAt hU hu hx)2930/-- Continuity is the extra hypothesis needed to upgrade the a.e. statement. -/31theorem WeakDivergenceZero.exists_eqOn32 {U : Set E} {u : E → ℝ} (hweak : WeakDivergenceZero μ U u)33 (hU : IsOpen U) (hUc : IsPreconnected U) (hu : LocallyIntegrableOn u U μ)34 (hcont : ContinuousOn u U) : ∃ c : ℝ, Set.EqOn u (fun _ => c) U := by35 rcases hweak.exists_aeConstantOn hU hUc hu with ⟨c, hc⟩36 exact ⟨c, Measure.eqOn_open_of_ae_eq hc hU hcont continuousOn_const⟩3738end MathlibAnnex