AffineLocalization.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.compact_uniform_gap_of_ne line 15

Source documentation

A continuous scalar function on a compact set stays uniformly away from any value which it never attains. Empty compact sets are allowed.

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

theorem OAI.Problem326.finite_closed_family_extend_fiber line 27

Source documentation

The strict conclusions of finitely many closed active-label conditions extend from one level of a continuous function to a neighborhood of that level. Each tolerance is fixed separately; no continuity in the label is required.

theorem finite_closed_family_extend_fiber
    {X : Type uX} {ι : Type uIota} [TopologicalSpace X] [Finite ι]
    {K : Set X} (hK : IsCompact K)
    (A : ι → Set X) (hA : ∀ i, IsClosed (A i))
    (μ : X → ℝ) (hμ : Continuous μ)
    (error : ι → X → ℝ) (herror : ∀ i, Continuous (error i))
    (E : ι → ℝ) (t : ℝ)
    (hgood : ∀ i x, x ∈ K → x ∈ A i → μ x = t → error i x < E i) :
    ∃ ρ : ℝ, 0 < ρ ∧
      ∀ i x, x ∈ K → x ∈ A i → |μ x - t| < ρ → error i x < E i := by
…

def OAI.Problem326.AsymptoticActive line 55
Source documentation
Limit points of active parameters as the positive scale tends to zero. This neighborhood formulation needs no regularity of the activity predicate.
```
def AsymptoticActive {X : Type uX} [PseudoMetricSpace X]
    (active : ℝ → X → Prop) (p : X) : Prop :=
…
```
theorem OAI.Problem326.isClosed_asymptoticActive line 62
Source documentation
Diagonal closure of asymptotic activity, without assuming continuity of any scale-dependent affine offset.
```
theorem isClosed_asymptoticActive {X : Type uX} [PseudoMetricSpace X]
    (active : ℝ → X → Prop) : IsClosed {p | AsymptoticActive active p} := by
…
```
Mentions: OAI.Problem326.AsymptoticActive

theorem OAI.Problem326.asymptoticActive_of_sequences line 74

Source documentation

An actual convergent active sequence yields asymptotic activity.

theorem asymptoticActive_of_sequences {X : Type uX} [PseudoMetricSpace X]
    (active : ℝ → X → Prop) {h : ℕ → ℝ} {q : ℕ → X} {p : X}
    (hhpos : ∀ n, 0 < h n) (hh : Tendsto h atTop (𝓝 0))
    (hq : Tendsto q atTop (𝓝 p)) (hactive : ∀ n, active (h n) (q n)) :
    AsymptoticActive active p := by
…

Mentions: OAI.Problem326.AsymptoticActive

theorem OAI.Problem326.AsymptoticActive.exists_sequences line 88

Source documentation

Every asymptotically active point has a realizing sequence.

theorem AsymptoticActive.exists_sequences {X : Type uX} [PseudoMetricSpace X]
    {active : ℝ → X → Prop} {p : X} (hp : AsymptoticActive active p) :
    ∃ (h : ℕ → ℝ) (q : ℕ → X),
      (∀ n, 0 < h n) ∧ Tendsto h atTop (𝓝 0) ∧ Tendsto q atTop (𝓝 p) ∧
      ∀ n, active (h n) (q n) := by
…

Mentions: OAI.Problem326.AsymptoticActive

theorem OAI.Problem326.active_family_extend_fiber line 109

Source documentation

The localization step for arbitrary scale-dependent active families. Its hypothesis is precisely a strict error bound for every active sequence whose limit lies in one prescribed level set.

theorem active_family_extend_fiber
    {X : Type uX} {ι : Type uIota} [PseudoMetricSpace X] [Finite ι]
    {K : Set X} (hK : IsCompact K)
    (active : ι → ℝ → X → Prop)
    (μ : X → ℝ) (hμ : Continuous μ)
    (error : ι → X → ℝ) (herror : ∀ i, Continuous (error i))
    (E : ι → ℝ) (t : ℝ)
    (hgood : ∀ (i : ι) (h : ℕ → ℝ) (q : ℕ → X) (p : X),
      p ∈ K → μ p = t → (∀ n, 0 < h n) → Tendsto h atTop (𝓝 0) →
      Tendsto q atTop (𝓝 p) → (∀ n, active i (h n) (q n)) → error i p < E i) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ i p, p ∈ K → |μ p - t| < ρ →
      AsymptoticActive (active i) p → error i p < E i := by
…

Mentions: OAI.Problem326.AsymptoticActive

theorem OAI.Problem326.uniform_activity_of_asymptotic line 131

Source documentation

Compactness turns a strict bound on all limiting active points into a uniform bound at every sufficiently small positive scale.

theorem uniform_activity_of_asymptotic
    {X : Type uX} [PseudoMetricSpace X] {K : Set X} (hK : IsCompact K)
    (active : ℝ → X → Prop) (error : X → ℝ) (herror : Continuous error) (E : ℝ)
    (hgood : ∀ p ∈ K, AsymptoticActive active p → error p < E) :
    ∃ h0 : ℝ, 0 < h0 ∧ ∀ h : ℝ, 0 < h → h < h0 →
      ∀ p ∈ K, active h p → error p < E := by
…

Mentions: OAI.Problem326.AsymptoticActive

theorem OAI.Problem326.finite_uniform_activity_of_asymptotic line 158

Source documentation

The scale in the uniform activity estimate can be chosen simultaneously for finitely many labels.

theorem finite_uniform_activity_of_asymptotic
    {X : Type uX} {ι : Type uIota} [PseudoMetricSpace X] [Finite ι]
    {K : Set X} (hK : IsCompact K)
    (active : ι → ℝ → X → Prop) (error : ι → X → ℝ)
    (herror : ∀ i, Continuous (error i)) (E : ι → ℝ)
    (hgood : ∀ i p, p ∈ K → AsymptoticActive (active i) p → error i p < E i) :
    ∃ h0 : ℝ, 0 < h0 ∧ ∀ h : ℝ, 0 < h → h < h0 →
      ∀ i p, p ∈ K → active i h p → error i p < E i := by
…

Mentions: OAI.Problem326.AsymptoticActive