UniformSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform estimates from arbitrary parameter selections

theorem OAI.PolycyclicRecognition.tendstoUniformly_const_of_all_selections line 16
Source documentation
To prove uniform convergence to a constant, it suffices to control every choice of one parameter at each index. No topology on the parameter set is needed. This lets a common word-coefficient envelope control whole families.
```
theorem tendstoUniformly_const_of_all_selections
    {ι Z V : Type*} [PseudoMetricSpace V] {l : Filter ι}
    (F : ι → Z → V) (v : V)
    (h : ∀ z : ι → Z, Tendsto (fun i => F i (z i)) l (𝓝 v)) :
    TendstoUniformly F (fun _ => v) l := by
…
```

theorem OAI.PolycyclicRecognition.tendsto_selection_of_tendstoUniformly_const line 40

Source documentation

Uniform convergence to a constant permits a different parameter at every index.

theorem tendsto_selection_of_tendstoUniformly_const
    {ι Z V : Type*} [PseudoMetricSpace V] {l : Filter ι}
    {F : ι → Z → V} {v : V}
    (h : TendstoUniformly F (fun _ => v) l) (z : ι → Z) :
    Tendsto (fun i => F i (z i)) l (𝓝 v) := by
…