AffineLimitSet.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Topological support for the local-to-global affine-label construction. The parameter approaches zero through positive values; no continuity in that parameter is assumed.

def OAI.Problem326.positiveLimitSet line 18
Source documentation
Limit points of a state family as a positive real parameter tends to zero.
```
def positiveLimitSet (A : ℝ → Set X) : Set X :=
…
```
theorem OAI.Problem326.isClosed_positiveLimitSet line 21
theorem OAI.Problem326.mem_positiveLimitSet_of_tendsto line 25
theorem OAI.Problem326.mem_positiveLimitSet_iff_seq line 33
theorem OAI.Problem326.isCompact_positiveLimitSet_inter line 48

theorem OAI.Problem326.exists_pos_band_disjoint line 54

Source documentation

A compact set missing a level of a continuous scalar function misses a whole open band around that level. This also handles an empty compact set.

theorem exists_pos_band_disjoint {K : Set X} (hK : IsCompact K)
    {μ : X → ℝ} (hμ : ContinuousOn μ K) {t : ℝ}
    (havoid : ∀ p ∈ K, μ p ≠ t) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ p ∈ K, ρ ≤ |μ p - t| := by
…

theorem OAI.Problem326.exists_pos_band_of_limit_good line 65

Source documentation

The finite-family form of the neighborhood extension step. If every limiting active label is good at one level, then this also holds in a band around that level. The good sets are open, but the active sets may be arbitrary.

theorem exists_pos_band_of_limit_good {ι : Type uIota} [Finite ι]
    {K : Set X} (hK : IsCompact K) {μ : X → ℝ}
    (hμ : ContinuousOn μ K) {t : ℝ} (A : ι → ℝ → Set X)
    (G : ι → Set X) (hG : ∀ i, IsOpen (G i))
    (hgood : ∀ i p, p ∈ K → μ p = t →
      p ∈ positiveLimitSet (A i) → p ∈ G i) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ i p, p ∈ K → |μ p - t| < ρ →
      p ∈ positiveLimitSet (A i) → p ∈ G i := by
…

Mentions: OAI.Problem326.positiveLimitSet

theorem OAI.Problem326.exists_pos_uniform_of_limit_subset line 95

Source documentation

Compactness upgrades a limiting active-set inclusion into a uniform small-parameter inclusion. No continuity of the active sets is required.

theorem exists_pos_uniform_of_limit_subset [FirstCountableTopology X]
    {A : ℝ → Set X} {K G : Set X} (hK : IsCompact K) (hG : IsOpen G)
    (hgood : ∀ p ∈ K, p ∈ positiveLimitSet A → p ∈ G) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
      ∀ p ∈ K, p ∈ A h → p ∈ G := by
…

Mentions: OAI.Problem326.positiveLimitSet

theorem OAI.Problem326.exists_pos_uniform_of_finite_limit_subset line 121

Source documentation

Uniform small-parameter inclusion for any finite family of active sets.

theorem exists_pos_uniform_of_finite_limit_subset [FirstCountableTopology X]
    {ι : Type uIota} [Finite ι] {A : ι → ℝ → Set X} {K : Set X}
    {G : ι → Set X} (hK : IsCompact K) (hG : ∀ i, IsOpen (G i))
    (hgood : ∀ i p, p ∈ K → p ∈ positiveLimitSet (A i) → p ∈ G i) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
      ∀ i p, p ∈ K → p ∈ A i h → p ∈ G i := by
…

Mentions: OAI.Problem326.positiveLimitSet