AffineApproximation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Topological compactness tools for the affine-label construction. These lemmas concern an arbitrary activity relation, so no continuity in the small parameter or in the label-dependent tolerance is assumed.

def OAI.Problem326.AffineApproximation.smallActivity line 23
Source documentation
Points at which a label is active for some positive parameter below δ.
```
def smallActivity (A : ℝ → X → I → Prop) (δ : ℝ) (i : I) : Set X :=
…
```
def OAI.Problem326.AffineApproximation.limitActivity line 27
Source documentation
All limiting activity points as the positive parameter tends to zero.
```
def limitActivity (A : ℝ → X → I → Prop) (i : I) : Set X :=
…
```
theorem OAI.Problem326.AffineApproximation.isClosed_limitActivity line 30
theorem OAI.Problem326.AffineApproximation.smallActivity_mono line 35

theorem OAI.Problem326.AffineApproximation.uniform_activity_one line 42

Source documentation

A compact set whose limiting activity points all lie in an open set has uniformly small activity in that open set.

theorem uniform_activity_one [T2Space X]
    (A : ℝ → X → I → Prop) (i : I) {K G : Set X}
    (hK : IsCompact K) (hG : IsOpen G)
    (hlim : K ∩ limitActivity A i ⊆ G) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
      ∀ x ∈ K, A h x i → x ∈ G := by
…

Mentions: OAI.Problem326.AffineApproximation.limitActivity

theorem OAI.Problem326.AffineApproximation.uniform_activity line 74

Source documentation

Uniformity holds simultaneously for a finite family of labels.

theorem uniform_activity [T2Space X] [Fintype I]
    (A : ℝ → X → I → Prop) {K : Set X} (G : I → Set X)
    (hK : IsCompact K) (hG : ∀ i, IsOpen (G i))
    (hlim : ∀ i, K ∩ limitActivity A i ⊆ G i) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
      ∀ x ∈ K, ∀ i, A h x i → x ∈ G i := by
…

Mentions: OAI.Problem326.AffineApproximation.limitActivity

theorem OAI.Problem326.AffineApproximation.nearby_level_activity line 93

Source documentation

The fixed-minimum guarantee extends to a neighborhood of that minimum. Only the finitely many fixed tolerance values are used.

theorem nearby_level_activity [Finite I]
    (A : ℝ → X → I → Prop) {K : Set X} (hK : IsCompact K)
    (μ : X → ℝ) (hμ : Continuous μ) (t : ℝ)
    (err : I → X → ℝ) (herr : ∀ i, Continuous (err i)) (E : I → ℝ)
    (hgood : ∀ i, ∀ p ∈ K, p ∈ limitActivity A i → μ p = t → err i p < E i) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ i, ∀ p ∈ K,
      p ∈ limitActivity A i → |μ p - t| < ρ → err i p < E i := by
…

Mentions: OAI.Problem326.AffineApproximation.limitActivity

theorem OAI.Problem326.AffineApproximation.mem_limitActivity_iff_seq line 126

theorem OAI.Problem326.AffineApproximation.uniform_activity_of_sequence line 160

Source documentation

Uniform activity bound in exactly the sequential form used by the affine approximation lemma.

theorem uniform_activity_of_sequence [T2Space X] [Fintype I]
    (A : ℝ → X → I → Prop) {K : Set X} (hK : IsCompact K)
    (err : I → X → ℝ) (herr : ∀ i, Continuous (err i)) (E : I → ℝ)
    (hseq : ∀ i, ∀ p ∈ K, ∀ h : ℕ → ℝ, ∀ x : ℕ → X,
      (∀ n, 0 < h n) → Tendsto h atTop (𝓝 0) → Tendsto x atTop (𝓝 p) →
      (∀ n, A (h n) (x n) i) → err i p < E i) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
      ∀ p ∈ K, ∀ i, A h p i → err i p < E i := by
…