Automatic uniformity

This module formalizes the automatic uniformity results of the blueprint's Basic notation chapter (notation-chapter): pointwise boundedness or infinitesimality along every variable sequence can be made uniform after passing to a subsequence.

Auxiliary lemmas for subsequence extraction

Automatic uniformity (auto)

theorem Expdb.automatic_uniformity_of_pointwise_bounded {α : Type u_1} [SeminormedAddCommGroup α] (E : VariableObject (Set ℝ)) (hE : ∀ (i : ℕ), (E i).Nonempty) (f : VariableFunction (fun (i : ℕ) => ↑(E i)) α) (hf : f.IsPointwiseBounded) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (C : ℝ), ∀ (i : ℕ) (x : ↑(E (φ i))), ‖f (φ i) x‖ ≤ C

Automatic uniform bound (blueprint auto, case (i)). If f(x) = O(1) for every variable x ∈ E, then after passing to a subsequence there exists a fixed C with |f(x)| ≤ C for all x ∈ E.

theorem Expdb.automatic_uniformity_of_pointwise_infinitesimal {α : Type u_1} [SeminormedAddCommGroup α] (E : VariableObject (Set ℝ)) (hE : ∀ (i : ℕ), (E i).Nonempty) (f : VariableFunction (fun (i : ℕ) => ↑(E i)) α) (hf : f.IsPointwiseInfinitesimal) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (c : VariableObject ℝ), c.IsInfinitesimal ∧ ∀ (i : ℕ) (x : ↑(E (φ i))), ‖f (φ i) x‖ ≤ c i

Automatic uniform infinitesimal (blueprint auto, case (ii)). If f(x) = o(1) for every variable x ∈ E, then after passing to a subsequence there exists an infinitesimal c with |f(x)| ≤ c for all x ∈ E.

Full-tail uniformity

theorem Expdb.VariableFunction.isPointwiseBounded_iff_eventually_uniform {α : Type u_1} [SeminormedAddCommGroup α] (E : VariableObject (Set ℝ)) (hE : ∀ (i : ℕ), (E i).Nonempty) (f : VariableFunction (fun (i : ℕ) => ↑(E i)) α) : f.IsPointwiseBounded ↔ ∃ (C : ℝ), ∀ᶠ (i : ℕ) in Filter.atTop, ∀ (x : ↑(E i)), ‖f i x‖ ≤ C

Boundedness along every variable choice is equivalent to an eventual bound uniform over the original variable sets. This strengthens automatic_uniformity_of_pointwise_bounded.

theorem Expdb.VariableFunction.isPointwiseInfinitesimal_iff_forall_pos_uniform {α : Type u_1} [SeminormedAddCommGroup α] (E : VariableObject (Set ℝ)) (hE : ∀ (i : ℕ), (E i).Nonempty) (f : VariableFunction (fun (i : ℕ) => ↑(E i)) α) : f.IsPointwiseInfinitesimal ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (i : ℕ) in Filter.atTop, ∀ (x : ↑(E i)), ‖f i x‖ < ε

Infinitesimality along every variable choice is equivalent to convergence that is eventually uniform over the original variable sets. This strengthens automatic_uniformity_of_pointwise_infinitesimal.