LocalRepresentativeGlue #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
From local continuous representatives to a global one #
An interior estimate produces, on each small ball inside an open set W, a
continuous function agreeing almost everywhere with a given u. This file
glues those local representatives into a single function continuous on all of
W and still agreeing almost everywhere with u.
No choice over a cover is used. The glued function is the canonical shrinking-average candidate
shrinkingAverageLimit u x = limUnder atTop (fun n ↦ ⨍_{euclideanBall x (n+1)⁻¹} u),
which reproduces the value of any local continuous representative at the centre of the ball, hence is automatically consistent on overlaps.
The uniqueness companion eqOn_of_continuousOn_of_ae_eq upgrades an almost
everywhere identity between two functions continuous on an open set to an
identity at every point of that set.
Two functions continuous on an open set that agree almost everywhere there agree at every point of the set.
The shrinking-average candidate #
The average of u over the Euclidean ball of radius (n+1)⁻¹ about x.
Equations
- Algsuperdiff.StochasticProcess.Common.Regularity.Ported.shrinkingBallAverage u x n = ⨍ (y : HCPolySupport.Vec d) in HCPolySupport.euclideanBall x (↑n + 1)⁻¹, u y
Instances For
The canonical candidate representative: the limit of the shrinking ball
averages of u.
Equations
Instances For
Where u agrees almost everywhere with a function continuous on a ball
about x, the shrinking ball averages of u converge to the value of that
function at x.
The candidate reproduces the value of any local continuous representative.
The candidate agrees with a local continuous representative on the whole ball on which the latter is defined.
Local continuous representatives on Euclidean balls glue to a single representative continuous on the whole open set.