Uniform Asymptotics

For a family of functions f : ι × α → E and g : α → E, we can think of f =O[𝓟 s ×ˢ l] fun (i, x) ↦ g x as expressing that f i is O(g) uniformly on s.

This file provides methods for constructing =O[𝓟 s ×ˢ l] relations (similarly Θ) and deriving their consequences.

theorem Asymptotics.isBigO_of_isBigOUniformly {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [Norm E] [Norm F] {f : ι × α → E} {g : α → F} {l : Filter α} (h : f =O[Filter.principal s ×ˢ l] (g ∘ Prod.snd)) {i : ι} (hi : i ∈ s) : (fun (x : α) => f (i, x)) =O[l] g

If f = O(g) uniformly on s, then f_i = O(g) for any i.`

theorem Asymptotics.isBigO_rev_of_isBigOUniformly_rev {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [Norm E] [Norm F] {f : ι × α → E} {g : α → F} {l : Filter α} (h : (g ∘ Prod.snd) =O[Filter.principal s ×ˢ l] f) {i : ι} (hi : i ∈ s) : g =O[l] fun (x : α) => f (i, x)

If f = Ω(g) uniformly on s, then f_i = Ω(g) for any i.`

theorem Asymptotics.isTheta_of_isThetaUniformly {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [Norm E] [Norm F] {f : ι × α → E} {g : α → F} {l : Filter α} (h : f =Θ[Filter.principal s ×ˢ l] (g ∘ Prod.snd)) {i : ι} (hi : i ∈ s) : (fun (x : α) => f (i, x)) =Θ[l] g

If f = Θ(g) uniformly on s, then f_i = Θ(g) for any i.`

theorem Asymptotics.isLittleO_const_fst_atBot {α : Type u_1} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup α] [LinearOrder α] [ProperSpace α] [NormedAddCommGroup F] [NoMinOrder α] [ClosedIicTopology α] (c : F) (ly : Filter E) : (fun (x : α × E) => c) =o[Filter.atBot ×ˢ ly] Prod.fst

theorem Asymptotics.isLittleO_const_snd_atBot {α : Type u_1} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup α] [LinearOrder α] [ProperSpace α] [NormedAddCommGroup F] [NoMinOrder α] [ClosedIicTopology α] (c : F) (lx : Filter E) : (fun (x : E × α) => c) =o[lx ×ˢ Filter.atBot] Prod.snd

theorem Asymptotics.isLittleO_const_fst_atTop {α : Type u_1} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup α] [LinearOrder α] [ProperSpace α] [NormedAddCommGroup F] [NoMaxOrder α] [ClosedIciTopology α] (c : F) (ly : Filter E) : (fun (x : α × E) => c) =o[Filter.atTop ×ˢ ly] Prod.fst

theorem Asymptotics.isLittleO_const_snd_atTop {α : Type u_1} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup α] [LinearOrder α] [ProperSpace α] [NormedAddCommGroup F] [NoMaxOrder α] [ClosedIciTopology α] (c : F) (lx : Filter E) : (fun (x : E × α) => c) =o[lx ×ˢ Filter.atTop] Prod.snd

theorem ContinuousOn.const_isBigOWithUniformlyOn_isCompact {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [TopologicalSpace ι] {C : ι → E} {c : F} [SeminormedAddGroup E] [Norm F] (hf : ContinuousOn C s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (l : Filter α) : Asymptotics.IsBigOWith (sSup (Norm.norm '' (C '' s)) / ‖c‖) (Filter.principal s ×ˢ l) (fun (x : ι × α) => match x with | (i, _x) => C i) fun (x : ι × α) => c

A family of constant functions f (i, x) = C i is uniformly bounded w.r.t. s by ⨆ i ∈ s, ‖C i‖, if s is compact and C is continuous.

theorem ContinuousOn.const_isBigOUniformlyOn_isCompact {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [TopologicalSpace ι] {C : ι → E} {c : F} [SeminormedAddGroup E] [Norm F] (hf : ContinuousOn C s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (l : Filter α) : (fun (x : ι × α) => match x with | (i, _x) => C i) =O[Filter.principal s ×ˢ l] fun (x : ι × α) => c

A family of constant functions f (i, x) = C i is uniformly O(1) w.r.t. s, if s is compact and C is continuous.

theorem ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [TopologicalSpace ι] {C : ι → E} {c : F} [NormedAddGroup E] [SeminormedAddGroup F] (hf : ContinuousOn C s) (hs : IsCompact s) (hC : ∀ i ∈ s, C i ≠ 0) (l : Filter α) : Asymptotics.IsBigOWith (‖c‖ / sInf (Norm.norm '' (C '' s))) (Filter.principal s ×ˢ l) (fun (x : ι × α) => c) fun (x : ι × α) => match x with | (i, _x) => C i

A family of constant functions f (i, x) = C i is uniformly bounded below w.r.t. s by ⊓ i ∈ s, ‖C i‖, if s is compact and C is continuous.

theorem ContinuousOn.const_isBigOUniformlyOn_isCompact_rev {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [TopologicalSpace ι] {C : ι → E} {c : F} [NormedAddGroup E] [SeminormedAddGroup F] (hf : ContinuousOn C s) (hs : IsCompact s) (hC : ∀ i ∈ s, C i ≠ 0) (l : Filter α) : (fun (x : ι × α) => c) =O[Filter.principal s ×ˢ l] fun (x : ι × α) => match x with | (i, _x) => C i

A family of constant functions f (i, x) = C i is uniformly Ω(1) w.r.t. s, if s is compact and C is continuous with no zeros on s.

theorem ContinuousOn.const_isThetaUniformlyOn_isCompact {α : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {s : Set ι} [TopologicalSpace ι] {C : ι → E} {c : F} [NormedAddGroup E] [SeminormedAddGroup F] (hf : ContinuousOn C s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (hC : ∀ i ∈ s, C i ≠ 0) (l : Filter α) : (fun (x : ι × α) => match x with | (i, _x) => C i) =Θ[Filter.principal s ×ˢ l] fun (x : ι × α) => c

A family of constant functions f (i, x) = C i is uniformly Θ(1) w.r.t. s, if s is compact and C is continuous with no zeros on s.