OAI/Analysis/MassAction/UniformActivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.uniform_activity_of_sequential_bound line 14

   Source documentation

   Compactness upgrades a strict sequential activity bound to a uniform small-parameter bound. No continuity of the activity predicate is needed.

   theorem uniform_activity_of_sequential_bound
       {X : Type uX} [TopologicalSpace X] [FirstCountableTopology X]
       {K : Set X} (hK : IsCompact K) (active : ℝ → X → Prop)
       (error : X → ℝ) (herror : Continuous error) (bound : ℝ)
       (hseq : ∀ (h : ℕ → ℝ) (p : ℕ → X) (p₀ : X),
         (∀ n, 0 < h n) → Tendsto h atTop (𝓝 0) →
         p₀ ∈ K → Tendsto p atTop (𝓝 p₀) →
         (∀ n, active (h n) (p n)) → error p₀ < bound) :
       ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
         ∀ p ∈ K, active h p → error p < bound := by
   …

2. theorem OAI.Problem326.finite_uniform_activity_of_sequential_bound line 44

   Source documentation

   The uniform activity bound for finitely many labels. The error tolerance may depend arbitrarily on the label; no regularity in that dependence is used.

   theorem finite_uniform_activity_of_sequential_bound
       {X : Type uX} [TopologicalSpace X] [FirstCountableTopology X]
       {I : Type uI} [Finite I] {K : Set X} (hK : IsCompact K)
       (active : ℝ → X → I → Prop) (error : I → X → ℝ)
       (herror : ∀ i, Continuous (error i)) (bound : I → ℝ)
       (hseq : ∀ (i : I) (h : ℕ → ℝ) (p : ℕ → X) (p₀ : X),
         (∀ n, 0 < h n) → Tendsto h atTop (𝓝 0) →
         p₀ ∈ K → Tendsto p atTop (𝓝 p₀) →
         (∀ n, active (h n) (p n) i) → error i p₀ < bound i) :
       ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
         ∀ p ∈ K, ∀ i, active h p i → error i p < bound i := by
   …