LogUniform.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.eventually_uniform_pos line 15

Source documentation

Compactness supplies a single positive bound, and uniform convergence preserves half of it simultaneously at every point.

theorem eventually_uniform_pos {X I : Type*} [TopologicalSpace X]
    {K : Set X} {l : Filter I} {u : I → X → ℝ} {t : X → ℝ}
    (hK : IsCompact K) (ht : ContinuousOn t K)
    (hp : ∀ x ∈ K, 0 < t x) (hu : TendstoUniformlyOn u t l K) :
    ∃ c : ℝ, 0 < c ∧ (∀ x ∈ K, 2*c ≤ t x) ∧
      ∀ᶠ i in l, ∀ x ∈ K, c ≤ u i x := by
…

theorem OAI.SymmetricMahler.uniform_comp_of_compact line 40

Source documentation

A continuous operation preserves uniform convergence when its inputs converge uniformly to a continuous function on a compact set in a proper space.

theorem uniform_comp_of_compact {X I E H : Type*} [TopologicalSpace X]
    [NormedAddCommGroup E] [ProperSpace E] [UniformSpace H]
    {K : Set X} {l : Filter I} {u : I → X → E} {t : X → E}
    (hK : IsCompact K) (ht : ContinuousOn t K)
    (hu : TendstoUniformlyOn u t l K) {g : E → H} (hg : Continuous g) :
    TendstoUniformlyOn (fun i x => g (u i x)) (fun x => g (t x)) l K := by
…

theorem OAI.SymmetricMahler.uniform_finite_pi line 63

Source documentation

Uniform convergence of a finite family, in its product norm.

theorem uniform_finite_pi {X I J V : Type*} [Fintype J] [PseudoMetricSpace V]
    {K : Set X} {l : Filter I} {u : I → J → X → V} {t : J → X → V}
    (h : ∀ j, TendstoUniformlyOn (fun i => u i j) (t j) l K) :
    TendstoUniformlyOn (fun i x j => u i j x) (fun x j => t j x) l K := by
…

theorem OAI.SymmetricMahler.uniform_pair line 76

Source documentation

Same-parameter product version of uniform convergence.

theorem uniform_pair {X I V W : Type*} [UniformSpace V] [UniformSpace W]
    {K : Set X} {l : Filter I} {u : I → X → V} {v : I → X → W}
    {t : X → V} {s : X → W}
    (hu : TendstoUniformlyOn u t l K) (hv : TendstoUniformlyOn v s l K) :
    TendstoUniformlyOn (fun i x => (u i x, v i x)) (fun x => (t x, s x)) l K := by
…