ControlledTupleMaps.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Properness estimates for controlled tuple maps

A bounded-difference tuple is determined up to finitely many choices once its first vertex belongs to a finite set. This is the support estimate used for the prism homotopy between close coarse maps.

theorem OAI.PolycyclicRecognition.finite_controlled_tuples_first line 20
Source documentation
Fixing a finite set of possible first vertices makes a controlled set of tuples finite.
```
theorem finite_controlled_tuples_first (S A : Set G) (hS : S.Finite) (hA : A.Finite) :
    {x : Fin (n + 1) → G | IsControlledTuple S x ∧ x 0 ∈ A}.Finite := by
…
```
Mentions: OAI.PolycyclicRecognition.IsControlledTuple

theorem OAI.PolycyclicRecognition.finite_controlled_tuple_map_fiber line 31

Source documentation

A tuple map whose first output is the image of its first input has finite fibers on controlled tuples whenever the underlying map is proper.

theorem finite_controlled_tuple_map_fiber
    (f : G → H) (hf : ∀ y, (f ⁻¹' {y}).Finite)
    (F : (Fin (n + 1) → G) → (Fin (m + 1) → H))
    (hF : ∀ x, F x 0 = f (x 0))
    (S : Set G) (hS : S.Finite) (y : Fin (m + 1) → H) :
    {x | IsControlledTuple S x ∧ F x = y}.Finite := by
…

Mentions: OAI.PolycyclicRecognition.IsControlledTuple

theorem OAI.PolycyclicRecognition.controlled_mixed_tuple line 45

Source documentation

Mixed tuples of two close maps have uniformly controlled differences. This is precisely the estimate required by the usual prism construction.

theorem controlled_mixed_tuple
    (f g : G → H) (hf : GroupBornologous f) (hg : GroupBornologous g)
    (hclose : (Set.range fun x => (f x)⁻¹ * g x).Finite)
    (S : Set G) (hS : S.Finite) :
    ∃ T : Set H, T.Finite ∧
      ∀ (x : Fin (n + 1) → G), IsControlledTuple S x →
      ∀ (a : Fin (m + 1) → Fin (n + 1)) (choose : Fin (m + 1) → Bool),
        IsControlledTuple T (fun i => if choose i then g (x (a i)) else f (x (a i))) := by
…

Mentions: OAI.PolycyclicRecognition.GroupBornologous, OAI.PolycyclicRecognition.IsControlledTuple