Mathlib.Topology

Topology helpers for subsequential limits, mapped cluster points, and compact cluster sets.

Uniform­Convergence 1 core · 1 supporting · 1 submodule Continuity helpers for function paths in topologies of uniform convergence on compact sets.
Compact­Exclusion 4 core · 9 supporting This module provides the non-effective compactness argument that turns "the only zero of a residual is the reference point" into a positive residual margin away from that point. ★ uniformCompactCorrespondence_dichotomy

Compact exclusion away from an isolated zero

This module provides the non-effective compactness argument that turns "the only zero of a residual is the reference point" into a positive residual margin away from that point.

* For a single problem: a continuous residual that is nonnegative on a compact candidate set and vanishes there only at a reference point has a strictly positive, attained minimum on the candidates outside any open neighborhood of that point, provided such candidates exist (PositiveExclusionRadius, exists_positiveExclusionRadius). * Uniformly over a compact correspondence of parameter--candidate pairs with a continuous reference section and a continuous positive radius function: either no feasible pair is far from its reference, or a single strictly positive residual tolerance forces every feasible pair with smaller residual into its own reference ball (farFeasibleSet, UniformPositiveExclusionRadius, uniformCompactCorrespondence_dichotomy, exists_uniformExclusionTolerance_lt, exists_uniformExclusionTolerance_le).

The statements quantify over arbitrary topological parameter spaces and (pseudo)metric candidate spaces; matrix specializations live in Causalean.Discovery.LinearDisentanglement.Quantitative.CompactExclusion.

structure PositiveExclusionRadius reviewed
Causalean.Mathlib.Topology.CompactExclusion

A positive exclusion radius is a positive lower bound for a residual on the part of K outside U, together with a candidate where that lower bound is attained.

Definition (Lean source)
parameters
X :
Type*
K U :
Set X
r :
X → ℝ
fields
The strictly positive residual radius.
radius :
ℝ
The exclusion radius is strictly positive.
radius_pos :
0 < radius
Every candidate in `K` outside `U` has residual at least the radius.
lower_bound :
∀ x
if
x ∈ K
and
x ∉ U
then
radius ≤ r x
Some candidate in `K` outside `U` attains the radius.
attained :
∃ x, x ∈ K ∧ x ∉ U ∧ r x = radius
Causalean.Mathlib.Topology.CompactExclusion.PositiveExclusionRadius · Causalean/Mathlib/Topology/CompactExclusion.lean:38
def farFeasibleSet reviewed
Causalean.Mathlib.Topology.CompactExclusion

For a parameter space, a candidate pseudometric space, a set of feasible parameter--candidate pairs, a reference candidate assigned to each parameter, and a real-valued radius assigned to each parameter, the far feasible set consists exactly of the feasible pairs whose candidate is at least that parameter's assigned radius from its reference candidate.

Definition (Lean source)
parameters
P X :
Type*
TopologicalSpace P
PseudoMetricSpace X
K :
Set (P × X)
x₀ :
P → X
ρ :
P → ℝ
def
farFeasibleSet K x₀ ρ :
Set (P × X)
given by
{z | z ∈ K ∧ ρ z.1 ≤ dist z.2 (x₀ z.1)}
Causalean.Mathlib.Topology.CompactExclusion.farFeasibleSet · Causalean/Mathlib/Topology/CompactExclusion.lean:95
structure UniformPositiveExclusionRadius reviewed
Causalean.Mathlib.Topology.CompactExclusion

A uniform positive exclusion radius records a far feasible pair where the residual reaches a strictly positive value that lower-bounds its value at every far feasible pair.

Definition (Lean source)
parameters
P X :
Type*
TopologicalSpace P
PseudoMetricSpace X
K :
Set (P × X)
x₀ :
P → X
ρ :
P → ℝ
r :
P × X → ℝ
fields
The parameter at which the uniform residual minimum is attained.
parameter :
P
The candidate at which the uniform residual minimum is attained.
candidate :
X
The attaining parameter-candidate pair belongs to the far feasible set.
mem_far :
(parameter, candidate) ∈ farFeasibleSet K x₀ ρ
The uniform residual tolerance.
radius :
ℝ
The uniform residual tolerance is strictly positive.
radius_pos :
0 < radius
The residual at the attaining pair equals the uniform residual tolerance.
attained :
r (parameter, candidate) = radius
The uniform residual tolerance lower-bounds the residual on the far feasible set.
lower_bound :
∀ z ∈ farFeasibleSet K x₀ ρ, radius ≤ r z
Causalean.Mathlib.Topology.CompactExclusion.UniformPositiveExclusionRadius · Causalean/Mathlib/Topology/CompactExclusion.lean:100
theorem uniformCompactCorrespondence_dichotomy reviewed
Causalean.Mathlib.Topology.CompactExclusion

Given a feasible correspondence, a reference section, a residual, and a radius function, if the correspondence is compact, the reference section is continuous, the residual is continuous, the radius function is continuous, every radius is strictly positive, the residual is nonnegative on feasible pairs, and only the reference candidate has zero residual among feasible pairs, then either no far feasible pair exists or one attains a strictly positive uniform residual minimum.

Formal statement
hypotheses
P X :
Type*
TopologicalSpace P
T2Space P
MetricSpace X
K :
Set (P × X)
x₀ :
P → X
r :
P × X → ℝ
ρ :
P → ℝ
hK :
IsCompact K
hx₀ :
Continuous x₀
hr_cont :
Continuous r
hρ_cont :
Continuous ρ
hρ_pos :
∀ p, 0 < ρ p
hr_nonneg :
∀ z ∈ K, 0 ≤ r z
hr_zero :
∀ p x
if
(p, x) ∈ K
and
r (p, x) = 0
then
x = x₀ p
conclusion
farFeasibleSet K x₀ ρ = ∅ ∨ Nonempty (UniformPositiveExclusionRadius K x₀ ρ r)
Proof (Lean source)
theorem uniformCompactCorrespondence_dichotomy {P X : Type*} [TopologicalSpace P] [T2Space P] [MetricSpace X] (K : Set (P × X)) (x₀ : P → X) (r : P × X → ℝ) (ρ : P → ℝ) (hK : IsCompact K) (hx₀ : Continuous x₀) (hr_cont : Continuous r) (hρ_cont : Continuous ρ) (hρ_pos : ∀ p, 0 < ρ p) (hr_nonneg : ∀ z ∈ K, 0 ≤ r z) (hr_zero : ∀ p x, (p, x) ∈ K → r (p, x) = 0 → x = x₀ p) : farFeasibleSet K x₀ ρ = ∅ ∨ Nonempty (UniformPositiveExclusionRadius K x₀ ρ r) := by have hfar_closed : IsClosed (farFeasibleSet K x₀ ρ) := isClosed_farFeasibleSet K x₀ ρ hK hx₀ hρ_cont rcases Set.eq_empty_or_nonempty (farFeasibleSet K x₀ ρ) with hfar | hfar · exact inl hfar · exact inr <| exists_uniformPositiveExclusionRadius_of_isClosed K x₀ r ρ hK hfar_closed hfar hr_cont hr_nonneg hr_zero hρ_pos
Causalean.Mathlib.Topology.CompactExclusion.uniformCompactCorrespondence_dichotomy · Causalean/Mathlib/Topology/CompactExclusion.lean:178 · uses UniformPositiveExclusionRadius , farFeasibleSet
9 supporting declarations (lemmas, instances)
  • exists_positiveExclusionRadius theorem — For a compact candidate set, an open local neighborhood, a continuous residual, and a reference point, if the candidate set is compact, the neighborhood is open, the reference belongs to the candidate set, the reference belongs to the neighborhood, the far set is nonempty, the residual is continuous, the residual is nonnegative on candidates, and its only zero among candidates is the reference, then the far set has a strictly positive attained residual minimum.
    hypotheses
    X :
    Type*
    TopologicalSpace X
    K U :
    Set X
    r :
    X → ℝ
    x₀ :
    X
    hK :
    IsCompact K
    hU :
    IsOpen U
    hxK :
    x₀ ∈ K
    hxU :
    x₀ ∈ U
    hfar :
    (K \ U).Nonempty
    hr_cont :
    Continuous r
    hr_nonneg :
    ∀ x ∈ K, 0 ≤ r x
    hr_zero :
    ∀ x ∈ K
    if
    r x = 0
    then
    x = x₀
    conclusion
    Nonempty (PositiveExclusionRadius K U r)
    Proof (Lean source)
    -- Proof route: `K \ U = K ∩ Uᶜ` is compact. Apply `IsCompact.exists_isMinOn` to `r` -- on this nonempty far set. Nonnegativity makes the minimum nonnegative; equality to -- zero forces its minimizer to be `x₀`, contradicting `x₀ ∈ U`. theorem exists_positiveExclusionRadius {X : Type*} [TopologicalSpace X] (K U : Set X) (r : X → ℝ) (x₀ : X) (hK : IsCompact K) (hU : IsOpen U) (hxK : x₀ ∈ K) (hxU : x₀ ∈ U) (hfar : (K \ U).Nonempty) (hr_cont : Continuous r) (hr_nonneg : ∀ x ∈ K, 0 ≤ r x) (hr_zero : ∀ x ∈ K, r x = 0 → x = x₀) : Nonempty (PositiveExclusionRadius K U r) := by have hcompact : IsCompact (K \ U) := by rw [Set.sdiff_eq] exact hK.inter_right hU.isClosed_compl obtain ⟨x, hx, hmin⟩ := hcompact.exists_isMinOn hfar hr_cont.continuousOn have hxK' : x ∈ K := hx.1 have hxU' : x ∉ U := hx.2 have hnonneg : 0 ≤ r x := hr_nonneg x hxK' have hpos : 0 < r x := lt_of_le_of_ne hnonneg fun hzero => by have heq : x = x₀ := hr_zero x hxK' hzero.symm exact hxU' (heq ▸ hxU) exact ⟨{ radius := r x radius_pos := hpos lower_bound := by intro y hyK hyU exact hmin ⟨hyK, hyU⟩ attained := ⟨x, hxK', hxU', rfl⟩ }⟩
    Causalean.Mathlib.Topology.CompactExclusion.exists_positiveExclusionRadius · Causalean/Mathlib/Topology/CompactExclusion.lean:50
  • isClosed_farFeasibleSet theorem — Given a feasible correspondence, a reference section, and a radius function, if the correspondence is compact, the reference section is continuous, and the radius function is continuous, then the parameter-dependent far feasible set is closed.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    T2Space P
    MetricSpace X
    K :
    Set (P × X)
    x₀ :
    P → X
    ρ :
    P → ℝ
    hK :
    IsCompact K
    hx₀ :
    Continuous x₀
    hρ :
    Continuous ρ
    conclusion
    IsClosed (farFeasibleSet K x₀ ρ)
    Proof (Lean source)
    theorem isClosed_farFeasibleSet {P X : Type*} [TopologicalSpace P] [T2Space P] [MetricSpace X] (K : Set (P × X)) (x₀ : P → X) (ρ : P → ℝ) (hK : IsCompact K) (hx₀ : Continuous x₀) (hρ : Continuous ρ) : IsClosed (farFeasibleSet K x₀ ρ) := by exact hK.isClosed.inter <| isClosed_le (hρ.comp continuous_fst) <| continuous_snd.dist (hx₀.comp continuous_fst)
    Causalean.Mathlib.Topology.CompactExclusion.isClosed_farFeasibleSet · Causalean/Mathlib/Topology/CompactExclusion.lean:120
  • isCompact_farFeasibleSet_of_isClosed theorem — Given a feasible correspondence, a reference section, and a radius function, if the correspondence is compact and its far feasible set is closed, then the far feasible set is compact.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    PseudoMetricSpace X
    K :
    Set (P × X)
    x₀ :
    P → X
    ρ :
    P → ℝ
    hK :
    IsCompact K
    hfar :
    IsClosed (farFeasibleSet K x₀ ρ)
    conclusion
    IsCompact (farFeasibleSet K x₀ ρ)
    Proof (Lean source)
    theorem isCompact_farFeasibleSet_of_isClosed {P X : Type*} [TopologicalSpace P] [PseudoMetricSpace X] (K : Set (P × X)) (x₀ : P → X) (ρ : P → ℝ) (hK : IsCompact K) (hfar : IsClosed (farFeasibleSet K x₀ ρ)) : IsCompact (farFeasibleSet K x₀ ρ) := by exact hK.of_isClosed_subset hfar fun _ hz => hz.1
    Causalean.Mathlib.Topology.CompactExclusion.isCompact_farFeasibleSet_of_isClosed · Causalean/Mathlib/Topology/CompactExclusion.lean:132
  • exists_uniformPositiveExclusionRadius_of_isClosed theorem — Given a feasible correspondence, a reference section, a residual, and a positive-radius function, if the correspondence is compact, the far feasible set is closed, the far feasible set is nonempty, the residual is continuous, the residual is nonnegative on feasible pairs, only the reference candidate has zero residual among feasible pairs, and every radius is strictly positive, then some far pair attains a strictly positive residual minimum on the far feasible set.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    PseudoMetricSpace X
    K :
    Set (P × X)
    x₀ :
    P → X
    r :
    P × X → ℝ
    ρ :
    P → ℝ
    hK :
    IsCompact K
    hfar_closed :
    IsClosed (farFeasibleSet K x₀ ρ)
    hfar_nonempty :
    (farFeasibleSet K x₀ ρ).Nonempty
    hr_cont :
    Continuous r
    hr_nonneg :
    ∀ z ∈ K, 0 ≤ r z
    hr_zero :
    ∀ p x
    if
    (p, x) ∈ K
    and
    r (p, x) = 0
    then
    x = x₀ p
    hρ_pos :
    ∀ p, 0 < ρ p
    conclusion
    Nonempty (UniformPositiveExclusionRadius K x₀ ρ r)
    Proof (Lean source)
    theorem exists_uniformPositiveExclusionRadius_of_isClosed {P X : Type*} [TopologicalSpace P] [PseudoMetricSpace X] (K : Set (P × X)) (x₀ : P → X) (r : P × X → ℝ) (ρ : P → ℝ) (hK : IsCompact K) (hfar_closed : IsClosed (farFeasibleSet K x₀ ρ)) (hfar_nonempty : (farFeasibleSet K x₀ ρ).Nonempty) (hr_cont : Continuous r) (hr_nonneg : ∀ z ∈ K, 0 ≤ r z) (hr_zero : ∀ p x, (p, x) ∈ K → r (p, x) = 0 → x = x₀ p) (hρ_pos : ∀ p, 0 < ρ p) : Nonempty (UniformPositiveExclusionRadius K x₀ ρ r) := by have hcompact : IsCompact (farFeasibleSet K x₀ ρ) := isCompact_farFeasibleSet_of_isClosed K x₀ ρ hK hfar_closed obtain ⟨⟨p, x⟩, hx, hmin⟩ := hcompact.exists_isMinOn hfar_nonempty hr_cont.continuousOn have hnonneg : 0 ≤ r (p, x) := hr_nonneg (p, x) hx.1 have hpos : 0 < r (p, x) := lt_of_le_of_ne hnonneg fun hzero => by have heq : x = x₀ p := hr_zero p x hx.1 hzero.symm have hnonpos : ρ p ≤ 0 := by simpa [heq] using hx.2 exact (not_lt_of_ge hnonpos) (hρ_pos p) exact ⟨{ parameter := p candidate := x mem_far := hx radius := r (p, x) radius_pos := hpos attained := rfl lower_bound := fun z hz => hmin hz }⟩
    Causalean.Mathlib.Topology.CompactExclusion.exists_uniformPositiveExclusionRadius_of_isClosed · Causalean/Mathlib/Topology/CompactExclusion.lean:141
  • uniformCompactCorrespondence_dichotomy_explicit theorem — Given a feasible correspondence, a reference section, a residual, and a radius function, if the correspondence is compact, the reference section is continuous, the residual is continuous, the radius function is continuous, every radius is strictly positive, the residual is nonnegative on feasible pairs, and only the reference candidate has zero residual among feasible pairs, then either the far feasible set is empty or a far pair and its strictly positive attained residual minimum can be exhibited explicitly.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    T2Space P
    MetricSpace X
    K :
    Set (P × X)
    x₀ :
    P → X
    r :
    P × X → ℝ
    ρ :
    P → ℝ
    hK :
    IsCompact K
    hx₀ :
    Continuous x₀
    hr_cont :
    Continuous r
    hρ_cont :
    Continuous ρ
    hρ_pos :
    ∀ p, 0 < ρ p
    hr_nonneg :
    ∀ z ∈ K, 0 ≤ r z
    hr_zero :
    ∀ p x
    if
    (p, x) ∈ K
    and
    r (p, x) = 0
    then
    x = x₀ p
    conclusion
    farFeasibleSet K x₀ ρ
    = ∅ ∨ ∃ pStar xStar ε₀, (pStar, xStar) ∈ farFeasibleSet K x₀ ρ ∧ 0 < ε₀ ∧ r (pStar, xStar) = ε₀ ∧ ∀ z ∈ farFeasibleSet K x₀ ρ, ε₀ ≤ r z
    Proof (Lean source)
    theorem uniformCompactCorrespondence_dichotomy_explicit {P X : Type*} [TopologicalSpace P] [T2Space P] [MetricSpace X] (K : Set (P × X)) (x₀ : P → X) (r : P × X → ℝ) (ρ : P → ℝ) (hK : IsCompact K) (hx₀ : Continuous x₀) (hr_cont : Continuous r) (hρ_cont : Continuous ρ) (hρ_pos : ∀ p, 0 < ρ p) (hr_nonneg : ∀ z ∈ K, 0 ≤ r z) (hr_zero : ∀ p x, (p, x) ∈ K → r (p, x) = 0 → x = x₀ p) : farFeasibleSet K x₀ ρ = ∅ ∨ ∃ pStar xStar ε₀, (pStar, xStar) ∈ farFeasibleSet K x₀ ρ ∧ 0 < ε₀ ∧ r (pStar, xStar) = ε₀ ∧ ∀ z ∈ farFeasibleSet K x₀ ρ, ε₀ ≤ r z := by rcases uniformCompactCorrespondence_dichotomy K x₀ r ρ hK hx₀ hr_cont hρ_cont hρ_pos hr_nonneg hr_zero with hfar | hnonempty · exact inl hfar · obtain ⟨h⟩ := hnonempty exact inr ⟨h.parameter, h.candidate, h.radius, h.mem_far, h.radius_pos, h.attained, h.lower_bound⟩
    Causalean.Mathlib.Topology.CompactExclusion.uniformCompactCorrespondence_dichotomy_explicit · Causalean/Mathlib/Topology/CompactExclusion.lean:203
  • dist_lt_of_residual_lt theorem — Given a uniform positive exclusion radius, a feasible pair, and a residual strictly below that radius, then the candidate lies strictly inside its parameter-dependent reference neighborhood.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    PseudoMetricSpace X
    Set (P × X)
    P → X
    P → ℝ
    P × X → ℝ
    h :
    UniformPositiveExclusionRadius K x₀ ρ r
    p :
    P
    x :
    X
    hK :
    (p, x) ∈ K
    hr :
    r (p, x) < h.radius
    conclusion
    dist x (x₀ p) < ρ p
    Proof (Lean source)
    theorem UniformPositiveExclusionRadius.dist_lt_of_residual_lt {P X : Type*} [TopologicalSpace P] [PseudoMetricSpace X] {K : Set (P × X)} {x₀ : P → X} {ρ : P → ℝ} {r : P × X → ℝ} (h : UniformPositiveExclusionRadius K x₀ ρ r) {p : P} {x : X} (hK : (p, x) ∈ K) (hr : r (p, x) < h.radius) : dist x (x₀ p) < ρ p := by by_contra hdist have hfar : (p, x) ∈ farFeasibleSet K x₀ ρ := ⟨hK, le_of_not_gt hdist⟩ exact (not_lt_of_ge (h.lower_bound (p, x) hfar)) hr
    Causalean.Mathlib.Topology.CompactExclusion.UniformPositiveExclusionRadius.dist_lt_of_residual_lt · Causalean/Mathlib/Topology/CompactExclusion.lean:228
  • dist_lt_of_residual_le_half theorem — Given a uniform positive exclusion radius, a feasible pair, and a residual at most half that radius, then the candidate lies strictly inside its parameter-dependent reference neighborhood.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    PseudoMetricSpace X
    Set (P × X)
    P → X
    P → ℝ
    P × X → ℝ
    h :
    UniformPositiveExclusionRadius K x₀ ρ r
    p :
    P
    x :
    X
    hK :
    (p, x) ∈ K
    hr :
    r (p, x) ≤ h.radius / 2
    conclusion
    dist x (x₀ p) < ρ p
    Proof (Lean source)
    theorem UniformPositiveExclusionRadius.dist_lt_of_residual_le_half {P X : Type*} [TopologicalSpace P] [PseudoMetricSpace X] {K : Set (P × X)} {x₀ : P → X} {ρ : P → ℝ} {r : P × X → ℝ} (h : UniformPositiveExclusionRadius K x₀ ρ r) {p : P} {x : X} (hK : (p, x) ∈ K) (hr : r (p, x) ≤ h.radius / 2) : dist x (x₀ p) < ρ p := by apply h.dist_lt_of_residual_lt hK exact lt_of_le_of_lt hr (div_lt_self h.radius_pos (by norm_num))
    Causalean.Mathlib.Topology.CompactExclusion.UniformPositiveExclusionRadius.dist_lt_of_residual_le_half · Causalean/Mathlib/Topology/CompactExclusion.lean:241
  • exists_uniformExclusionTolerance_lt theorem — Given a feasible correspondence, a reference section, a residual, and a radius function, if the correspondence is compact, the reference section is continuous, the residual is continuous, the radius function is continuous, every radius is strictly positive, the residual is nonnegative on feasible pairs, and only the reference candidate has zero residual among feasible pairs, then one strictly positive tolerance sends every feasible pair with smaller residual inside its own reference neighborhood.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    T2Space P
    MetricSpace X
    K :
    Set (P × X)
    x₀ :
    P → X
    r :
    P × X → ℝ
    ρ :
    P → ℝ
    hK :
    IsCompact K
    hx₀ :
    Continuous x₀
    hr_cont :
    Continuous r
    hρ_cont :
    Continuous ρ
    hρ_pos :
    ∀ p, 0 < ρ p
    hr_nonneg :
    ∀ z ∈ K, 0 ≤ r z
    hr_zero :
    ∀ p x
    if
    (p, x) ∈ K
    and
    r (p, x) = 0
    then
    x = x₀ p
    conclusion
    ∃ ε₀ : ℝ,
    0 < ε₀
    conclusion 1
    p x :
    (p, x) ∈ K
    r (p, x) < ε₀
    dist x (x₀ p) < ρ p
    Proof (Lean source)
    theorem exists_uniformExclusionTolerance_lt {P X : Type*} [TopologicalSpace P] [T2Space P] [MetricSpace X] (K : Set (P × X)) (x₀ : P → X) (r : P × X → ℝ) (ρ : P → ℝ) (hK : IsCompact K) (hx₀ : Continuous x₀) (hr_cont : Continuous r) (hρ_cont : Continuous ρ) (hρ_pos : ∀ p, 0 < ρ p) (hr_nonneg : ∀ z ∈ K, 0 ≤ r z) (hr_zero : ∀ p x, (p, x) ∈ K → r (p, x) = 0 → x = x₀ p) : ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ p x, (p, x) ∈ K → r (p, x) < ε₀ → dist x (x₀ p) < ρ p := by rcases uniformCompactCorrespondence_dichotomy K x₀ r ρ hK hx₀ hr_cont hρ_cont hρ_pos hr_nonneg hr_zero with hfar | hnonempty · refine ⟨1, by norm_num, ?_⟩ intro p x hpx _ by_contra hdist have hx : (p, x) ∈ farFeasibleSet K x₀ ρ := ⟨hpx, le_of_not_gt hdist⟩ rw [hfar] at hx exact hx.elim · obtain ⟨h⟩ := hnonempty exact ⟨h.radius, h.radius_pos, fun p x hpx hr => h.dist_lt_of_residual_lt hpx hr⟩
    Causalean.Mathlib.Topology.CompactExclusion.exists_uniformExclusionTolerance_lt · Causalean/Mathlib/Topology/CompactExclusion.lean:253
  • exists_uniformExclusionTolerance_le theorem — Given a feasible correspondence, a reference section, a residual, and a radius function, if the correspondence is compact, the reference section is continuous, the residual is continuous, the radius function is continuous, every radius is strictly positive, the residual is nonnegative on feasible pairs, and only the reference candidate has zero residual among feasible pairs, then one strictly positive tolerance sends every feasible pair with residual at most that tolerance inside its own reference neighborhood.
    hypotheses
    P X :
    Type*
    TopologicalSpace P
    T2Space P
    MetricSpace X
    K :
    Set (P × X)
    x₀ :
    P → X
    r :
    P × X → ℝ
    ρ :
    P → ℝ
    hK :
    IsCompact K
    hx₀ :
    Continuous x₀
    hr_cont :
    Continuous r
    hρ_cont :
    Continuous ρ
    hρ_pos :
    ∀ p, 0 < ρ p
    hr_nonneg :
    ∀ z ∈ K, 0 ≤ r z
    hr_zero :
    ∀ p x
    if
    (p, x) ∈ K
    and
    r (p, x) = 0
    then
    x = x₀ p
    conclusion
    ∃ ε₀ : ℝ,
    0 < ε₀
    conclusion 1
    p x :
    (p, x) ∈ K
    r (p, x) ≤ ε₀
    dist x (x₀ p) < ρ p
    Proof (Lean source)
    theorem exists_uniformExclusionTolerance_le {P X : Type*} [TopologicalSpace P] [T2Space P] [MetricSpace X] (K : Set (P × X)) (x₀ : P → X) (r : P × X → ℝ) (ρ : P → ℝ) (hK : IsCompact K) (hx₀ : Continuous x₀) (hr_cont : Continuous r) (hρ_cont : Continuous ρ) (hρ_pos : ∀ p, 0 < ρ p) (hr_nonneg : ∀ z ∈ K, 0 ≤ r z) (hr_zero : ∀ p x, (p, x) ∈ K → r (p, x) = 0 → x = x₀ p) : ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ p x, (p, x) ∈ K → r (p, x) ≤ ε₀ → dist x (x₀ p) < ρ p := by rcases uniformCompactCorrespondence_dichotomy K x₀ r ρ hK hx₀ hr_cont hρ_cont hρ_pos hr_nonneg hr_zero with hfar | hnonempty · refine ⟨1, by norm_num, ?_⟩ intro p x hpx _ by_contra hdist have hx : (p, x) ∈ farFeasibleSet K x₀ ρ := ⟨hpx, le_of_not_gt hdist⟩ rw [hfar] at hx exact hx.elim · obtain ⟨h⟩ := hnonempty refine ⟨h.radius / 2, half_pos h.radius_pos, ?_⟩ intro p x hpx hr exact h.dist_lt_of_residual_le_half hpx hr
    Causalean.Mathlib.Topology.CompactExclusion.exists_uniformExclusionTolerance_le · Causalean/Mathlib/Topology/CompactExclusion.lean:282
Subsequential­Limits 1 core · 1 supporting This module relates limits along strictly increasing subsequences to mapped cluster points and proves compactness of the subsequential-limit set when a sequence is eventually contained in a compact set. ★ subsequentialLimitSet_nonempty_compact_of_eventually_mem_compact

Subsequential limits

This module relates limits along strictly increasing subsequences to mapped cluster points and proves compactness of the subsequential-limit set when a sequence is eventually contained in a compact set.

theorem subsequentialLimitSet_nonempty_compact_of_eventually_mem_compact reviewed
Causalean.Mathlib.Topology

If a sequence is eventually contained in a compact set, then its set of limits along strictly increasing subsequences is nonempty and compact.

Formal statement
hypotheses
X :
Type u_1
shared
x :
ℕ → X
s :
Set X
hs :
IsCompact s
hx :
∀ᶠ n in atTop, x n ∈ s
conclusion
conclusion 1
∃ y : X, ∃ φ : ℕ → ℕ,
StrictMono φ
Tendsto (x ∘ φ) atTop (nhds y)
conclusion 2
IsCompact {y : X | ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (nhds y)}
Proof (Lean source)
theorem subsequentialLimitSet_nonempty_compact_of_eventually_mem_compact (x : ℕ → X) {s : Set X} (hs : IsCompact s) (hx : ∀ᶠ n in atTop, x n ∈ s) : (∃ y : X, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (nhds y)) ∧ IsCompact {y : X | ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (nhds y)} := by obtain ⟨y, _hy, φ, hφ, hy⟩ := hs.tendsto_subseq' hx.frequently refine ⟨⟨y, φ, hφ, hy⟩, ?_⟩ have heq : {y : X | ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (nhds y)} = {y : X | MapClusterPt y atTop x} := by ext z exact isSubsequentialLimit_iff_mapClusterPt x z rw [heq] apply hs.of_isClosed_subset · simpa only [MapClusterPt] using (isClosed_setOfPred_clusterPt (f := Filter.map x atTop)) · intro z hz exact hs.isClosed.mem_of_mapClusterPt hz hx
Causalean.Mathlib.Topology.subsequentialLimitSet_nonempty_compact_of_eventually_mem_compact · Causalean/Mathlib/Topology/SubsequentialLimits.lean:36
1 supporting declaration (lemmas, instances)