The precise representative of a W^{1,p} function #
A Sobolev function is locally integrable on its domain, so by the Lebesgue differentiation
theorem it agrees almost everywhere there with its precise representative
TauCeti.MeasureTheory.preciseRepresentative, the limit of its averages over shrinking balls.
Main declarations #
TauCeti.W1p.ae_eq_preciseRepresentative: a Sobolev function agrees almost everywhere with its precise representative.
theorem
TauCeti.W1p.ae_eq_preciseRepresentative
{E : Type u_1}
[MeasurableSpace E]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
[BorelSpace E]
{mu : MeasureTheory.Measure E}
[mu.IsAddHaarMeasure]
{Omega : TopologicalSpace.Opens E}
{p : ENNReal}
[Fact (1 ≤ p)]
(u : ↥(W1p mu Omega p))
:
↑↑(value u) =ᵐ[mu.restrict ↑Omega] MeasureTheory.preciseRepresentative mu ↑↑(value u)
A Sobolev function agrees almost everywhere on its domain with its precise representative.