CocycleGrowth.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Sublinear cocycle bounds from compact coboundary approximation

Compact-uniform approximation by coboundaries makes an isometric cocycle sublinear on words of linearly bounded length.

theorem OAI.PolycyclicRecognition.norm_isometric_action line 20
def OAI.PolycyclicRecognition.IsCocycle line 24
Source documentation
The left cocycle convention for an isometric representation.
```
def IsCocycle (b : G → E) : Prop := ∀ g h, b (g * h) = b g + g • b h
…
```
theorem OAI.PolycyclicRecognition.IsCocycle.map_one line 27
theorem OAI.PolycyclicRecognition.IsCocycle.corrected line 35
Source documentation
Coboundary correction preserves the cocycle identity.
```
theorem IsCocycle.corrected {b : G → E} (hb : IsCocycle b) (φ : E) :
    IsCocycle (fun g => b g + g • φ - φ) := by
…
```
Mentions: OAI.PolycyclicRecognition.IsCocycle
theorem OAI.PolycyclicRecognition.IsCocycle.norm_word_le line 42
theorem OAI.PolycyclicRecognition.norm_le_corrected_add line 58
Source documentation
The error of removing a coboundary is at most twice the vector norm, uniformly over the acting group.
```
theorem norm_le_corrected_add (b : G → E) (φ : E) (g : G) :
    ‖b g‖ ≤ ‖b g + g • φ - φ‖ + 2 * ‖φ‖ := by
…
```

theorem OAI.PolycyclicRecognition.IsCocycle.norm_word_le_of_coboundary line 70

Source documentation

The concrete word estimate used after reduced cohomology vanishing. The approximating vector is fixed before the word length tends to infinity.

theorem IsCocycle.norm_word_le_of_coboundary {b : G → E} (hb : IsCocycle b)
    (Q : Set G) (φ : E) {ε : ℝ}
    (hQ : ∀ g ∈ Q, ‖b g + g • φ - φ‖ ≤ ε)
    (l : List G) (hl : ∀ g ∈ l, g ∈ Q) :
    ‖b l.prod‖ ≤ (l.length : ℝ) * ε + 2 * ‖φ‖ :=
…

Mentions: OAI.PolycyclicRecognition.IsCocycle

theorem OAI.PolycyclicRecognition.IsCocycle.sublinear_of_coboundary_approximation line 80

Source documentation

Compact-uniform coboundary approximation implies a global sublinear estimate. The length and word-factorization hypotheses are explicit.

theorem IsCocycle.sublinear_of_coboundary_approximation
    {b : G → E} (hb : IsCocycle b) (Q : Set G) (length : G → ℝ)
    (hlen : ∀ g, 0 ≤ length g) {a : ℝ} (ha : 0 ≤ a)
    (hword : ∀ g, ∃ l : List G, (∀ q ∈ l, q ∈ Q) ∧ l.prod = g ∧
      (l.length : ℝ) ≤ a * length g + a)
    (happrox : ∀ ε : ℝ, 0 < ε → ∃ φ : E, ∀ q ∈ Q, ‖b q + q • φ - φ‖ ≤ ε) :
    ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g, ‖b g‖ ≤ ε * length g + B := by
…

Mentions: OAI.PolycyclicRecognition.IsCocycle

theorem OAI.PolycyclicRecognition.uniform_sublinear_on_balls line 112

Source documentation

A global sublinear estimate is uniform after division by scale on every linearly growing metric ball. The additive error is chosen before the scale.

theorem uniform_sublinear_on_balls {b : G → E} (length : G → ℝ)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g, ‖b g‖ ≤ ε * length g + B)
    {R : ℝ} (hR : 0 ≤ R) : ∀ ε : ℝ, 0 < ε →
      ∃ r₀ : ℝ, 0 ≤ r₀ ∧ ∀ r, r₀ ≤ r → ∀ g, length g ≤ R * r → ‖b g‖ ≤ ε * r := by
…