Continuous representatives from internal L-infinity translations
Abstract
Internal essential-supremum translations produce unique continuous representatives with a common modulus on a closed interval.
Throughout, E is a real Banach space in any universe. Ioc(a,b) is the right-closed interval (a,b], and Icc(a,b) is the closed interval [a,b]. RestrictedVolume denotes restricted Lebesgue measure. Average(f,A) is the Bochner integral of f over A divided by its measure. InternalDifference(f,h) is the function t mapped to f(t+h)-f(t). AEEq(mu,f,g) means equality of the two functions almost everywhere for mu. The projection projIcc(0,T,t) clamps t to [0,T] and takes values in that closed-interval subtype. IccExtend(g,0,T) is the real-line function t mapped to g(projIcc(0,T,t)).
Theorem 1.1 (Consistency of arbitrary short interval averages).
Proof. Machine-checked in Lean as D5/S3/Topology/Measures/IntervalLInfinityRepresentative.local_average_consistency (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let f be strongly measurable on the real line and integrable on Ioc(0,T). Suppose every positive internal translation below delta has L-infinity seminorm less than ofReal(epsilon), where epsilon is nonnegative. Consider any two positive-length interval windows Ioc(a,b) and Ioc(c,d) contained in Ioc(0,T). If every point of one window has distance less than delta from every point of the other, then the distance of their averages is at most epsilon. The windows may have different lengths, overlap, or meet either endpoint of the original interval.
For each fixed shift the essential-supremum estimate holds outside a null set. Fubini’s theorem and the measure-preserving shear (x,h) mapped to (x,x+h) give the corresponding estimate for almost every pair of times. Symmetry covers negative separations, and the diagonal has zero difference. Restricting that pair estimate to the product of the two windows and applying Mathlib’s convex-set average theorem twice proves the average estimate. There is no intersection over uncountably many shift-dependent sets.
Theorem 1.2 (A common modulus for the unique continuous representatives).
Proof. Machine-checked in Lean as D5/S3/Topology/Measures/IntervalLInfinityRepresentative.exists_continuous_representatives (✓ std3). ∎
Source. Repository-derived.
Commentary.
T is positive and S is an arbitrary, possibly empty subset of the actual Lp(E,infinity,RestrictedVolume(Ioc(0,T))) space. The translation scale is uniform over S. The map R has domain S itself and codomain the continuous maps on Icc(0,T). The first conclusion identifies each original almost-everywhere class. The second gives one epsilon-delta continuity condition for all members and all pairs of points, including 0 and T. The third gives uniqueness among all continuous representatives. The fourth permits every almost-everywhere equal real-line representative u, preserving both its identification with R(f) and every positive internal translation seminorm.
For x in [0,T] and r>0, take the average over Ioc(max(0,x-r),min(T,x+r)). This window has positive length even at x=0 or x=T. With r=1/(n+1), the consistency estimate makes these averages Cauchy. Completeness of E gives a limit at every x. The same estimate for windows centered at nearby points passes to the limits and supplies a common continuity modulus. For each of the countably many accuracies 1/(k+1), the pair estimate also makes the shrinking averages close to f(x) for almost every x. Passing to their limits identifies the continuous function with the original class. Full support of Lebesgue measure on the interval and continuity then give uniqueness.
There is no separate common bound on the norms of S, no restriction on the dimension of E, and no separability or reflexivity assumption. The integral construction uses only the individual integrability inherited from L-infinity on a finite interval. It assumes no pointwise time modulus, continuous representative, endpoint value, boundary-tail condition, or whole-line translation estimate. In particular the unbounded family of all scalar constant functions satisfies the translation condition and has a common continuity modulus; this assertion does not claim that such a family is compact.
Simon, Compact sets in the space Lp(0,T;B), DOI 10.1007/BF01762360, Section 3, Theorem 1, includes a compactness conclusion in C(0,T;B) for p=infinity and uses right means and opposite time directions. Its C convention uses the closed interval. That source does not separately state the entire arbitrary-family lifting and uniqueness assertion displayed here. The present local-window construction is a derived argument; no originality or open-problem claim is made.