Sublevels of real functions #

If a real function has a unique global minimum and one compact sublevel strictly above it, then sufficiently small sublevels lie in any prescribed open neighbourhood of the minimum (TauCeti.exists_pos_sublevel_subset_of_unique_min). This allows local descriptions near the minimum to describe whole sublevels. Continuity is needed only on the one compact sublevel, not on the entire space. Similarly, if a superlevel {w ≥ -δ} of a continuous w is compact, a closed set avoiding the zero level of w avoids a whole band {|w| ≤ η} around it (TauCeti.exists_forall_abs_le_notMem).

The local counterpart concerns a strict local minimum x of a function f continuous near x on a locally compact Hausdorff space: for every neighbourhood U of x, a preconnected set through a point y close to x, on which f stays at most f y, lies in U (TauCeti.eventually_forall_isPreconnected_subset_of_strictLocalMin). The trajectories of a dynamical system along which f does not increase are such sets, so this is the topological core of Lyapunov stability.

Conversely, restricting a function to a set S which is not closed can destroy compactness of sublevels: if S accumulates at a point p ∉ S with f p < r, then {x ∈ S | f x ≤ r} is not compact (TauCeti.not_isCompact_inter_preimage_Iic). A compact sublevel {f ≤ b}, on which f is continuous, lies strictly above some value a ≤ b, whose sublevel is then empty (TauCeti.exists_le_forall_lt_of_isCompact_sublevel).

If a continuous motion of the space lowers f at unit speed through the band a ≤ f ≤ b, then following it until the level a is reached retracts the sublevel {f ≤ b} onto {f ≤ a}, by a homotopy fixing {f ≤ a} pointwise (TauCeti.exists_sublevelDeformation_of_apply_eq_sub); here TauCeti.sublevelInclusion is the inclusion of {f ≤ a} into {f ≤ b}, a closed embedding when f is continuous (TauCeti.isClosedEmbedding_sublevelInclusion). This is the topological half of the deformation of sublevels across a band without critical points, where the motion is the flow of a vector field X with df(X) = -1 on the band. The sublevels form the topological pair TauCeti.sublevelPair f : ({f ≤ b}, {f ≤ a}), whose relative homology measures the change in topology across the band. The band itself, relative to its lower level, is the pair TauCeti.bandPair f : (f⁻¹[a, b], f⁻¹(a)), which includes into the sublevel pair by TauCeti.bandPairInclusion; when f⁻¹[a, b] is a cobordism between regular levels, this is the cobordism relative to its incoming boundary. Relative to its upper level, the band is the pair TauCeti.upperBandPair f : (f⁻¹[a, b], f⁻¹(b)), the cobordism relative to its outgoing boundary; negating f exchanges the two (TauCeti.bandPair_neg). All sublevels together form the functor TauCeti.sublevelFunctor f from the levels to spaces, with the cocone TauCeti.sublevelCocone f of their inclusions into X.

If the motion is a flow along whose lines f never increases, then its time-(b - a) map carries {f ≤ b} exactly onto {f ≤ a} (Flow.apply_le_iff_of_apply_eq_sub), and, when f strictly decreases along flow lines starting on the level a, the level f⁻¹(b) exactly onto f⁻¹(a) (Flow.apply_eq_iff_of_apply_eq_sub). This is the topological half of the homeomorphism between the sublevels on either side of a band without critical points.

Under the same hypotheses the band f⁻¹[a, b] is homeomorphic to f⁻¹(a) × [a, b] by a homeomorphism preserving the value of f (Flow.bandHomeomorph): a point of the band is sent to the point where its flow line meets the level a, together with its value.

Along an inducing map j : M → X whose range contains a band F⁻¹[a, b], compactness of the band pulls back to the band of F ∘ j (Topology.IsInducing.isCompact_comp_preimage_Icc).