CocyclePullbackSublinear.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Pulling compact-word sublinearity to a proper chain metric

theorem OAI.PolycyclicRecognition.sublinear_comp_of_compact_word_estimates line 19

Source documentation

A continuous homomorphism maps a compact generating ball to a compact set. Its pulled-back cocycle inherits the metric sublinearity estimate.

theorem sublinear_comp_of_compact_word_estimates
    (f : H →* G) (hf : Continuous f) (b : G → E) (C : LinearMetricChains H)
    (hsub : ∀ K : Set G, IsCompact K →
      ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ (u : ℕ → G) (m : ℕ),
        (∀ i < m, u i ∈ K) → ‖b (wordPrefix u m)‖ ≤ ε * (m : ℝ) + B) :
    ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ h, ‖b (f h)‖ ≤ ε * dist 1 h + B := by
…

Mentions: OAI.PolycyclicRecognition.wordPrefix