Successive maximum refinement by an ordered list of functionals

MathlibAnnex.lexicographicRefine

def

Defines a nonempty compact set of survivors after maximizing finitely many functionals in order.

Statement

For a nonempty compact set in a real normed space and a finite ordered list of continuous linear functionals, successively retain the points maximizing , then those maximizing on the retained set, and so on. The resulting set is denoted .

Definition

Let . The complete recursion is

The maximum of each later functional is taken on the current retained set. Changing the order can therefore change the resulting set.

Assumptions

The ambient space is any real normed vector space. The set is nonempty and compact, and the list is finite and ordered. No finite-dimensionality or point-separation assumption is needed for this definition.

Conclusion

The result is a nonempty compact set. For the empty list it is itself. A singleton conclusion requires a separate point-separation hypothesis; this definition does not select a single point.

Each maximum slice is nonempty compact by continuity on a nonempty compact set. Thus every recursive step is defined. Later lemmas show that the final set lies in and that all survivors have the same value under every functional in the list. If the list separates points, those equalities force the final set to be a singleton.

noncomputable def lexicographicRefine :
    List (E →L[ℝ] ℝ) → TopologicalSpace.NonemptyCompacts E →
      TopologicalSpace.NonemptyCompacts E
  | [], K => K
  | ℓ :: ls, K => lexicographicRefine ls (refine K ℓ)

noncomputable section

open Set
open TopologicalSpace

namespace MathlibAnnex

universe u

variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project