Representative #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Transferring a bound to a fixed continuous representative #
The pointwise estimates of this directory end in an existential: some function, continuous on a ball and almost everywhere equal to the solution there, has a small value at the centre. A consumer usually carries a continuous representative of its own and needs the bound for that one.
The transfer is the standard fact that two functions continuous on an open
set and almost everywhere equal there agree at every point of it, because
Lebesgue measure is positive on nonempty open sets. That fact is
MeasureTheory.Measure.eqOn_open_of_ae_eq; the statements below are its
specialization to Euclidean balls, in the shape the pointwise estimates hand
over. Two representatives of the same solution are almost everywhere equal
to each other by transitivity, so no further hypothesis is needed.
Main results #
Two functions continuous on a Euclidean ball and almost everywhere equal there agree at every point of the ball.
A bound at the centre proved for one continuous representative holds for every continuous representative on the same ball.