ActivityLimits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.activityLimitSet line 14
Source documentation
Limiting points of activity as the positive parameter tends to zero, expressed using closed sets; no continuity of active is required.
```
def activityLimitSet {X : Type uX} [TopologicalSpace X]
    (active : ℝ → X → Prop) : Set X :=
…
```
theorem OAI.Problem326.isClosed_activityLimitSet line 18

theorem OAI.Problem326.mem_activityLimitSet_of_tendsto line 24

Source documentation

Every limit of active points at positive parameters tending to zero belongs to the closed activity-limit set.

theorem mem_activityLimitSet_of_tendsto
    {X : Type uX} [TopologicalSpace X] {active : ℝ → X → Prop}
    {h : ℕ → ℝ} {p : ℕ → X} {z : X}
    (hhpos : ∀ n, 0 < h n) (hh : Tendsto h atTop (𝓝 0))
    (hp : Tendsto p atTop (𝓝 z)) (ha : ∀ n, active (h n) (p n)) :
    z ∈ activityLimitSet active := by
…

Mentions: OAI.Problem326.activityLimitSet

theorem OAI.Problem326.exists_active_sequence_of_mem_activityLimitSet line 40

Source documentation

In a pseudometric space every point of the activity-limit set is realized by an actual sequence, even when activity is not a closed relation.

theorem exists_active_sequence_of_mem_activityLimitSet
    {X : Type uX} [PseudoMetricSpace X] {active : ℝ → X → Prop} {z : X}
    (hz : z ∈ activityLimitSet active) :
    ∃ (h : ℕ → ℝ) (p : ℕ → X), (∀ n, 0 < h n) ∧
      Tendsto h atTop (𝓝 0) ∧ Tendsto p atTop (𝓝 z) ∧
      ∀ n, active (h n) (p n) := by
…

Mentions: OAI.Problem326.activityLimitSet

theorem OAI.Problem326.compact_avoid_level_has_uniform_gap line 63

Source documentation

Compactness upgrades avoidance of one level to a positive uniform gap.

theorem compact_avoid_level_has_uniform_gap
    {X : Type uX} [TopologicalSpace X] {K : Set X} (hK : IsCompact K)
    {f : X → ℝ} (hf : ContinuousOn f K) (t : ℝ)
    (hne : ∀ x ∈ K, f x ≠ t) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ x ∈ K, ρ ≤ |f x - t| := by
…

theorem OAI.Problem326.activity_limits_good_near_level line 76

Source documentation

A good-label guarantee at one level extends to nearby levels. This is the compact bad-limit-set argument; tolerances may vary arbitrarily between labels.

theorem activity_limits_good_near_level
    {X : Type uX} [TopologicalSpace X] {ι : Type uIota} [Finite ι]
    {K : Set X} (hK : IsCompact K) (active : ι → ℝ → X → Prop)
    (good : ι → Set X) (hgood : ∀ i, IsOpen (good i))
    {f : X → ℝ} (hf : ContinuousOn f K) (t : ℝ)
    (hlevel : ∀ i z, z ∈ K → f z = t →
      z ∈ activityLimitSet (active i) → z ∈ good i) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ z ∈ K, |f z - t| < ρ →
      ∀ i, z ∈ activityLimitSet (active i) → z ∈ good i := by
…

Mentions: OAI.Problem326.activityLimitSet