The precise representative of a function #
For a function f on a metric measure space, the precise representative is the limit of the
averages of f over the closed balls closedBall x r as r → 0⁺, taken at every point where
this limit exists (and a junk value elsewhere). It depends only on the almost-everywhere class of
f, and by the Lebesgue differentiation theorem it agrees almost everywhere with f when f is
locally integrable and the measure is doubling. It is therefore a canonical pointwise choice of
representative of an L¹_loc class, and the natural candidate for a continuous representative.
The second half of the file turns bounds on the essential oscillation of f on small balls into
continuity and Hölder estimates for the precise representative. If f takes values almost
everywhere on ball x r in a closed convex set S, then the averages over the closed balls
around x lie in S once their radius is below r, and so does their limit. This gives:
- if the essential oscillation of
fonball x rtends to0withr, the averages converge atx, and the precise representative is their limit there; - if the essential oscillation of
fonball x ris at mostC r^αfor the pointsxof a setsand all radiir ≤ ρ, andfis essentially bounded nears, then the precise representative is Hölder continuous onswith exponentα.
The second statement is how an a-priori estimate on the decay of the oscillation, such as the one for solutions of elliptic equations in De Giorgi's theorem, becomes Hölder continuity of a representative.
Main declarations #
TauCeti.MeasureTheory.preciseRepresentative: the limit of the averages over shrinking closed balls.TauCeti.MeasureTheory.preciseRepresentative_congr_ae: the precise representative depends only on the almost-everywhere class.TauCeti.MeasureTheory.ae_eq_restrict_preciseRepresentative: a function locally integrable on an open set agrees almost everywhere there with its precise representative.TauCeti.MeasureTheory.preciseRepresentative_eq_of_continuousAt: the precise representative atxof a function equal almost everywhere nearxto a functiongcontinuous atxisg x.TauCeti.MeasureTheory.tendsto_setAverage_closedBall_preciseRepresentative: the averages converge at points where the essential oscillation vanishes.TauCeti.MeasureTheory.tendsto_setAverage_closedBall_preciseRepresentative_of_rpow: the averages converge at points where the essential oscillation decays like a power of the radius.TauCeti.MeasureTheory.dist_preciseRepresentative_le: two points of a ball on whichftakes values in a closed ball of radiusLhave precise representatives at distance at most2 L.TauCeti.MeasureTheory.holderOnWith_preciseRepresentative: oscillation decaying liker^αmakes the precise representative Hölder continuous.
References #
- L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, §1.7 and §4.8 (Lebesgue points and the precise representative).
The precise representative of f with respect to μ: at each point x, the limit of the
averages of f over closedBall x r as r → 0⁺. Where this limit does not exist, the value is
the junk value of limUnder.
Equations
- TauCeti.MeasureTheory.preciseRepresentative μ f x = (nhdsWithin 0 (Set.Ioi 0)).limUnder fun (r : ℝ) => ⨍ (y : X) in Metric.closedBall x r, f y ∂μ
Instances For
The precise representative is the limit of the averages over shrinking closed balls, whenever this limit exists.
The precise representative at x only depends on the almost-everywhere class of f on a
neighbourhood of x.
The precise representative only depends on the almost-everywhere class of f.
Lebesgue differentiation for the precise representative. For a uniformly locally doubling
measure, a function which is locally integrable on an open set U agrees almost everywhere on U
with its precise representative.
Lebesgue differentiation for the precise representative. For a uniformly locally doubling measure, a locally integrable function agrees almost everywhere with its precise representative.
If f takes values almost everywhere on ball x r in a closed convex set S, then so do its
averages over the closed balls around x of small radius.
If f takes values almost everywhere on ball x r in a closed convex set S, and the
averages of f over the closed balls around x converge, then the precise representative of f
at x lies in S.
The precise representative reproduces continuous representatives. If f agrees almost
everywhere near x with a function g which is continuous at x, then the precise
representative of f at x is g x.
The precise representative of a function agrees on an open set U with any function g
continuous on U which equals it almost everywhere on U.
The precise representative of a locally integrable continuous function is the function itself.
Vanishing oscillation gives convergence of the averages. If the essential oscillation of
f on ball x r tends to 0 with r, in the sense that for every ε > 0 the function takes
values almost everywhere on some ball around x in a closed ball of radius ε, then the averages
of f over the closed balls around x converge to the precise representative of f at x.
If f takes values almost everywhere on ball x r in the closed ball closedBall c L, then
the precise representatives of f at x and at any y ∈ ball x r are at distance at most
2 L, provided the averages of f over the closed balls around x and around y converge.
If f is essentially bounded by M on ball x r and the averages of f over the closed balls
around x converge, then the precise representative of f at x has norm at most M.
Power-law oscillation decay gives convergence of the averages. Let α > 0 and ρ > 0. If
for every 0 < r ≤ ρ the function f takes values almost everywhere on ball x r in a closed
ball of radius C r^α, then the averages of f over the closed balls around x converge to the
precise representative of f at x.
Hölder continuity from oscillation decay. Let s be a set, ρ > 0 and α > 0. Suppose
f is integrable near every point of s, essentially bounded by M on the balls ball x ρ,
x ∈ s, and that its essential oscillation decays like a power of the radius: for every x ∈ s
and 0 < r ≤ ρ, almost everywhere on ball x r the function takes values in a closed ball of
radius C r^α. Then the precise representative of f is Hölder continuous on s with exponent
α, with a constant depending only on C, M, ρ and α.