OAI/GroupTheory/PolycyclicRecognition/Analysis/AsymptoticEquicontinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.equicontinuousAt_of_joint_error_tendsto line 18

   Source documentation

   A bound vanishing jointly as the scale grows and the point approaches x₀, together with equicontinuity at each fixed scale, controls the entire family. The auxiliary index allows all random chart samples at each scale.

   theorem equicontinuousAt_of_joint_error_tendsto
       (F : ℕ → A → X → W) (E : ℕ → X → ℝ) (x₀ : X)
       (hhead : ∀ n, EquicontinuousAt (F n) x₀)
       (hbound : ∀ n a x, dist (F n a x₀) (F n a x) ≤ E n x)
       (htail : Tendsto (fun p : ℕ × X => E p.1 p.2)
         (atTop ×ˢ 𝓝 x₀) (𝓝 0)) :
       EquicontinuousAt (fun p : ℕ × A => F p.1 p.2) x₀ := by
   …

2. theorem OAI.PolycyclicRecognition.equicontinuousAt_of_continuous_joint_error line 41

   Source documentation

   The fixed-scale hypothesis can itself be supplied by the continuous metric error bound; no common modulus at small scales is needed.

   theorem equicontinuousAt_of_continuous_joint_error
       (F : ℕ → A → X → W) (E : ℕ → X → ℝ) (x₀ : X)
       (hE : ∀ n, ContinuousAt (E n) x₀) (hzero : ∀ n, E n x₀ = 0)
       (hbound : ∀ n a x, dist (F n a x₀) (F n a x) ≤ E n x)
       (htail : Tendsto (fun p : ℕ × X => E p.1 p.2)
         (atTop ×ˢ 𝓝 x₀) (𝓝 0)) :
       EquicontinuousAt (fun p : ℕ × A => F p.1 p.2) x₀ := by
   …