Uniform weak-star perturbations

Abstract

Weak-star closed norm balls transfer dense uniform estimates to the entire compactification.

Theorem 1.1 (The estimate at every point).

$$\forall X:Type,[\mathrm{NormedAddCommGroup}\left(X\right)][\mathrm{NormedSpace}\left(Real,X\right)]\forall A:Type,\forall T:Type,[\mathrm{TopologicalSpace}\left(T\right)]\forall i:A\to T,\forall f:T\to \mathrm{WeakDual}\left(Real,X\right),\forall g:T\to \mathrm{WeakDual}\left(Real,X\right),\forall epsilon:Real,\mathrm{DenseRange}\left(i\right)\wedge \mathrm{Continuous}\left(f\right)\wedge \mathrm{Continuous}\left(g\right)\wedge \forall a:A,\mathrm{norm}\left(\mathrm{toStrongDual}\left(f\left(i\left(a\right)\right)-g\left(i\left(a\right)\right)\right)\right)\le epsilon\Rightarrow \forall p:T,\mathrm{norm}\left(\mathrm{toStrongDual}\left(f\left(p\right)-g\left(p\right)\right)\right)\le epsilon$$

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/WeakStarPerturbation.norm_sub_le_of_denseRange (✓ std3). ∎

Source. Repository-derived.

Commentary.

X is any real normed space; A is any index type and T any topological space. The image of i is dense. For weak-star continuous f and g, the strong-dual norm of f minus g is at most epsilon everywhere if it is at most epsilon at every i(a). The inverse image of the weak-star closed epsilon ball under f minus g is closed and contains the dense range. No continuity of the norm is asserted.

Theorem 1.2 (Injection survives when twice the error is below the gap).

$$\forall X:Type,[\mathrm{NormedAddCommGroup}\left(X\right)][\mathrm{NormedSpace}\left(Real,X\right)]\forall A:Type,\forall T:Type,[\mathrm{TopologicalSpace}\left(T\right)]\forall i:A\to T,\forall f:T\to \mathrm{WeakDual}\left(Real,X\right),\forall g:T\to \mathrm{WeakDual}\left(Real,X\right),\forall c:Real,\forall epsilon:Real,\mathrm{DenseRange}\left(i\right)\wedge \mathrm{Continuous}\left(f\right)\wedge \mathrm{Continuous}\left(g\right)\wedge \forall p:T,\forall q:T,p\ne q\Rightarrow c\le \mathrm{norm}\left(\mathrm{toStrongDual}\left(f\left(p\right)-f\left(q\right)\right)\right)\wedge 2\cdot epsilon<c\wedge \forall a:A,\mathrm{norm}\left(\mathrm{toStrongDual}\left(f\left(i\left(a\right)\right)-g\left(i\left(a\right)\right)\right)\right)\le epsilon\Rightarrow \mathrm{Injective}\left(g\right)$$

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/WeakStarPerturbation.injective_of_approximation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume every unequal pair of f-values has strong-dual norm distance at least c, and twice epsilon is less than c. The dense estimate transfers to every p and q. If g(p)=g(q), the triangle inequality gives norm(f(p)-f(q)) at most twice epsilon, contradicting the gap. The signed-ball application obtains c directly from WeakStarNormSeparation.exists_pos_le_norm_sub on the full Stone–Čech domain.

Theorem 1.3 (The bounded extension exists).

$$\forall X:Type,[\mathrm{NormedAddCommGroup}\left(X\right)][\mathrm{NormedSpace}\left(Real,X\right)]\forall a:Nat\to \mathrm{StrongDual}\left(Real,X\right),\forall R:Real,\forall n:Nat,\mathrm{norm}\left(a\left(n\right)\right)\le R\Rightarrow \exists f:\mathrm{Ultrafilter}\left(Nat\right)\to \mathrm{WeakDual}\left(Real,X\right),\mathrm{Continuous}\left(f\right)\wedge \forall n:Nat,f\left(\mathrm{pure}\left(n\right)\right)=\mathrm{toWeakDual}\left(a\left(n\right)\right)\wedge \forall p:\mathrm{Ultrafilter}\left(Nat\right),\mathrm{norm}\left(\mathrm{toStrongDual}\left(f\left(p\right)\right)\right)\le R$$

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/WeakStarPerturbation.exists_bounded_extension (✓ std3). ∎

Source. Repository-derived.

Commentary.

Banach–Alaoglu makes the full radius R dual ball compact in the weak-star topology. Extend the sequence into that actual compact subtype and then forget the subtype. The extension agrees at every principal ultrafilter and remains in the same ball at every free ultrafilter.

Theorem 1.4 (Normalize by the actual norms).

$$\forall E:Type,[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{NormedSpace}\left(Real,E\right)]\forall a:Nat\to E,\forall B:Real,\forall r:Real,\forall n:Nat,\mathrm{norm}\left(a\left(n\right)\right)\le B\wedge 0<r\wedge \mathrm{Tendsto}\left(n\mapsto \mathrm{norm}\left(a\left(n\right)\right),atTop,\mathrm{nhds}\left(r\right)\right)\Rightarrow \mathrm{Tendsto}\left(n\mapsto \mathrm{smul}\left(\mathrm{inv}\left(\mathrm{norm}\left(a\left(n\right)\right)\right),a\left(n\right)\right)-\mathrm{smul}\left(\mathrm{inv}\left(r\right),a\left(n\right)\right),atTop,\mathrm{nhds}\left(0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Topology/Measures/WeakStarPerturbation.normalize_sub_tendsto_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a bounded sequence a(n) in an arbitrary real normed space with norms tending to r greater than zero, the displayed difference is norm(a(n)) inverse times a(n), minus r inverse times a(n). It tends to zero in norm. The scalar coefficient norm(a(n)) inverse minus r inverse tends to zero; multiplying its norm by the fixed bound B gives a vanishing upper bound. No equality of the raw norms is assumed.

References

• Truth anchor: D5/S3/Topology/Measures/WeakStarPerturbation.exists_bounded_extension
• Truth anchor: D5/S3/Topology/Measures/WeakStarPerturbation.injective_of_approximation
• Truth anchor: D5/S3/Topology/Measures/WeakStarPerturbation.norm_sub_le_of_denseRange
• Truth anchor: D5/S3/Topology/Measures/WeakStarPerturbation.normalize_sub_tendsto_zero
• Dependency: D5/S3/Topology/ExtremallyDisconnected/WeakStarNormSeparation