ProfileFlowConvergence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform evaluation of compact profile families along converging flows

def OAI.PolycyclicRecognition.profileAlongMap line 20
Source documentation
Evaluate a profile and a coordinate map jointly on fixed profile and parameter sets.
```
def profileAlongMap (S : Set C(V, W)) (K : Set U) (T : C(U, V)) : C(S × K, W) :=
…
```
theorem OAI.PolycyclicRecognition.continuous_profileAlongMap line 26
Source documentation
Compact-open continuity of joint profile evaluation.
```
theorem continuous_profileAlongMap (S : Set C(V, W)) (K : Set U) :
    Continuous (profileAlongMap (W := W) S K) := by
…
```
Mentions: OAI.PolycyclicRecognition.profileAlongMap

theorem OAI.PolycyclicRecognition.profileAlongMap_tendstoUniformly line 37

Source documentation

Convergence of the coordinate maps is uniform after evaluating every profile in one compact family at every parameter in one compact set.

theorem profileAlongMap_tendstoUniformly
    (S : Set C(V, W)) (hS : IsCompact S) (K : Set U) (hK : IsCompact K)
    {ι : Type*} {l : Filter ι} {T : ι → C(U, V)} {T₀ : C(U, V)}
    (hT : Tendsto T l (𝓝 T₀)) :
    TendstoUniformly (fun i (p : S × K) => p.1.val (T i p.2.val))
      (fun p : S × K => p.1.val (T₀ p.2.val)) l := by
…