OAI/GroupTheory/PolycyclicRecognition/Algebra/RealParameterEquicontinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.uniform_nonnegative_parameter_of_joint_limit line 16

   Source documentation

   Joint continuity controls a compact initial interval of scales; the joint limit at infinity controls the remaining scales.

   theorem uniform_nonnegative_parameter_of_joint_limit
       {X : Type*} [TopologicalSpace X] (E : ℝ → X → ℝ) (x₀ : X)
       (hE : Continuous (fun p : ℝ × X => E p.1 p.2))
       (hzero : ∀ r, E r x₀ = 0)
       (htail : Tendsto (fun p : ℝ × X => E p.1 p.2)
         (atTop ×ˢ 𝓝 x₀) (𝓝 0)) :
       ∀ ε : ℝ, 0 < ε → ∀ᶠ x in 𝓝 x₀, ∀ r, 0 ≤ r → E r x < ε := by
   …

2. theorem OAI.PolycyclicRecognition.equicontinuous_nonnegative_parameter_of_joint_error line 46

   Source documentation

   The same metric modulus controls all maps and all nonnegative scales, with no choice of a scale sequence in the compact family.

   theorem equicontinuous_nonnegative_parameter_of_joint_error
       {X W A : Type*} [TopologicalSpace X] [PseudoMetricSpace W]
       (F : {r : ℝ // 0 ≤ r} → A → X → W) (E : ℝ → X → ℝ) (x₀ : X)
       (hE : Continuous (fun p : ℝ × X => E p.1 p.2))
       (hzero : ∀ r, E r x₀ = 0)
       (hbound : ∀ r a x, dist (F r a x₀) (F r a x) ≤ E r.val x)
       (htail : Tendsto (fun p : ℝ × X => E p.1 p.2)
         (atTop ×ˢ 𝓝 x₀) (𝓝 0)) :
       EquicontinuousAt (fun p : {r : ℝ // 0 ≤ r} × A => F p.1 p.2) x₀ := by
   …