Consider

\[ f(x)= \begin{cases} 1,&x=0,\\ 0,&x\ne0. \end{cases} \]

If \(x_j\to0\), then \(f(x_j)\le1=f(0)\), so

\[ \limsup_{j\to\infty}f(x_j)\le f(0). \]

The function is upper semicontinuous at zero even though it is not continuous there. Its values may jump downward away from zero. Reversing the two values would create an upward jump at zero and would fail upper semicontinuity.

Definition

A real-valued function \(f:X\to\mathbb R\) is sequentially upper semicontinuous at \(x\) when every sequence \(x_j\to x\) satisfies

\[ \limsup_{j\to\infty}f(x_j)\le f(x). \]

An equivalent epsilon formulation is:

\[ \forall\varepsilon\gt0,\quad f(x_j)\le f(x)+\varepsilon \quad\text{for all sufficiently large }j. \]

In general topological spaces, the neighborhood or filter definition is the primary one. The sequential definition completely detects the topology in metric and first-countable settings, but not in every topological space.

A point at x has height f of x. Nearby function values remain below the horizontal roof f of x plus epsilon. One nearby value lies far below f of x, showing that downward jumps are allowed.
FigureThe epsilon roof: nearby values must eventually stay below \(f(x)+\varepsilon\). Upper semicontinuity does not place a matching floor under them, so it does not imply continuity.

In RMT-36

The input is a measurable finite-dimensional matrix generator over one fixed probability-preserving base. The output is its signed integrated real-log growth rate \(\lambda(G)\). RMT-36 proves the sequential statement

\[ G_j\longrightarrow G_0\ \text{uniformly} \quad\Longrightarrow\quad \forall\varepsilon\gt0,\quad \lambda(G_j)\le\lambda(G_0)+\varepsilon \ \text{eventually}, \]

within a class having shared forward and inverse norm bounds and pointwise invertibility.

One idea, three languages Read across, then read the syntax map
A human says
No positive tolerance above the limiting rate is crossed by all sufficiently late perturbed rates.
On paper
\(\forall\varepsilon>0,\ \lambda(G_j)\le\lambda(G_0)+\varepsilon\) eventually.
In Lean
eventually_integratedRealLogGrowthRate_le_add\n  hT hG hε
Syntax map
hT fixes the probability-preserving base. hG is uniform convergence of the generators. hε : 0 < ε records that the tolerance is positive. eventually is expressed in the theorem by the filter notation ∀ᶠ n in atTop.
Try it in the repository NonlinearDynamics/Random/RandomCocycles/GrowthRateStability.lean
This full project command checks the exact matrix-cocycle upper-stability theorem. It can require substantial disk space and build time. The theorem is sequential and one-sided; the command does not check a full-continuity claim.
Full project check, from the repository root
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/GrowthRateStability.lean

Resource note: this exact file uses the repository's pinned Lean and Mathlib dependencies. Initial project setup can require substantial disk space and build time. For a lightweight first step on macOS or Linux, use the page's standalone Lean-core or Std tutorial.

Why infima often produce upper semicontinuity

Suppose

\[ f(x)=\inf_{k\ge1}q_k(x) \]

and each fixed \(q_k\) is continuous. If \(y\gt f(x)\), one index \(k\) has \(q_k(x)\lt y\). Continuity preserves that strict inequality near \(x\), and \(f\le q_k\) transfers it to \(f\). This selects one upper witness.

RMT-36 follows exactly this pattern. The functions \(q_k\) are normalized finite-horizon signed log-norm integrals, and dominated convergence supplies their sequential continuity.

Boundaries

  • Upper semicontinuity controls upward displacement, not downward displacement.
  • It does not imply lower semicontinuity or continuity.
  • A sequential theorem should not be silently promoted to a theorem for all nets in an arbitrary topology.
  • RMT-36 varies the matrix generator only. It does not vary the base map or probability measure.
  • The term stochastic stability may instead concern stationary measures or random attractors. Those are different outputs.

References

  1. J. Bochi, “Genericity of zero Lyapunov exponents,” Ergodic Theory and Dynamical Systems 22(6), 1667–1696 (2002), doi:10.1017/S0143385702001165.
  2. L. Backes, A. Brown, and C. Butler, “Continuity of Lyapunov exponents for cocycles with invariant holonomies,” Journal of Modern Dynamics 12, 223–260 (2018), doi:10.3934/jmd.2018009.