feat: Bounded Range versus IsBigO Asymptotics (#40664)

Show that for a continuous function `f : ℝ → E` into a seminormed space, having bounded range is equivalent to being `O(1)` along both `atTop` and `atBot`. If `f` is even, then a single `O(1)` bound along `atTop` already suffices. This material is used in Value Distribution Theory, where boundedness is traditionally expressed as being `O(1)`.

Author: kebekus

Mathlib/Algebra/Group/EvenFunction.lean

@@ -34,12 +34,18 @@ protected def Even (f : α → β) : Prop := ∀ a, f (-a) = f a
 /-- A function `f` is _odd_ if it satisfies `f (-x) = -f x` for all `x`. -/
 protected def Odd [Neg β] (f : α → β) : Prop := ∀ a, f (-a) = -(f a)
 
+/-- An even function `f` satisfies `f (-x) = f x`. -/
+lemma Even.eq {f : α → β} (hf : f.Even) (x : α) : f (-x) = f x := hf x
+
 /-- Any constant function is even. -/
 lemma Even.const (b : β) : Function.Even (fun _ : α ↦ b) := fun _ ↦ rfl
 
 /-- The zero function is even. -/
 lemma Even.zero [Zero β] : Function.Even (fun (_ : α) ↦ (0 : β)) := Even.const 0
 
+/-- An odd function `f` satisfies `f (-x) = -f x`. -/
+lemma Odd.eq [Neg β] {f : α → β} (hf : f.Odd) (x : α) : f (-x) = -f x := hf x
+
 /-- The zero function is odd. -/
 lemma Odd.zero [NegZeroClass β] : Function.Odd (fun (_ : α) ↦ (0 : β)) := fun _ ↦ neg_zero.symm
 

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -18,10 +18,7 @@ theory developed in `Mathlib/Analysis/Asymptotics/Defs.lean` and
 
 public section
 
-
-open Filter Asymptotics
-
-open Topology
+open Bornology Filter Asymptotics Set Topology
 
 section NormedField
 
@@ -209,3 +206,66 @@ theorem Asymptotics.isEquivalent_nat_ceil :
   isEquivalent_of_tendsto_one tendsto_nat_ceil_div_atTop
 
 end NormedLinearOrderedField
+
+section boundedRange
+
+/-!
+## Bounded Range versus `IsBigO` Asymptotics
+
+For a continuous function `f` into a seminormed space, defined on an unbounded linear order whose
+order topology has compact intervals, having bounded range is equivalent to being `O(1)` along both
+`atTop` and `atBot` (`Continuous.isBounded_range_iff_isBigO_atTop_atBot`). For an even function a
+single `O(1)` bound along `atTop` already suffices
+(`Continuous.isBounded_range_iff_isBigO_atTop_of_even`), since `Function.Even` transports an `atTop`
+bound to an `atBot` bound (`Function.Even.isBigO_atTop_iff_isBigO_atBot`).
+-/
+
+variable
+  {E : Type*} [SeminormedAddCommGroup E]
+  {D : Type*} [TopologicalSpace D]
+  {β : Type*} [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] [CompactIccSpace β]
+    [NoMaxOrder β] [NoMinOrder β]
+
+/--
+A continuous function `f` has bounded range if and only if it is `O(1)` with respect to the
+cocompact filter.
+-/
+theorem Continuous.isBounded_range_iff_isBigO {f : D → E} (hf : Continuous f) :
+    IsBounded (range f) ↔ f =O[cocompact D] (1 : D → ℝ) := by
+  constructor <;> intro h
+  · rw [isBounded_iff_forall_norm_le] at h
+    obtain ⟨c, hc⟩ := h
+    simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hc
+    rw [isBigO_iff]
+    use c
+    apply Eventually.of_forall
+    simpa using hc
+  · simp_rw [isBigO_iff, Filter.Eventually, Filter.mem_cocompact] at h
+    simp only [Pi.one_apply, norm_one, mul_one] at h
+    obtain ⟨c, t, hcompact, h⟩ := h
+    rw [← Set.image_union_image_compl_eq_range (s := t)]
+    apply IsBounded.union
+    · apply (IsCompact.image hcompact hf).isBounded
+    · rw [isBounded_iff_forall_norm_le]
+      refine ⟨c, fun x hx ↦ ?_⟩
+      rw [Set.mem_image] at hx
+      obtain ⟨y, hy, rfl⟩ := hx
+      simpa using mem_of_mem_of_subset hy h
+
+/--
+A continuous function `f` on an unbounded linear order with compact intervals has bounded range if
+and only if it is `O(1)` at both `atTop` and `atBot`.
+-/
+theorem Continuous.isBounded_range_iff_isBigO_atTop_atBot {f : β → E} (hf : Continuous f) :
+    IsBounded (range f) ↔ f =O[atTop] (1 : β → ℝ) ∧ f =O[atBot] (1 : β → ℝ) := by
+  rw [hf.isBounded_range_iff_isBigO, cocompact_eq_atBot_atTop, isBigO_sup, and_comm]
+
+/-- A continuous even function has bounded range if and only if `f =O[atTop] 1`. -/
+theorem Continuous.isBounded_range_iff_isBigO_atTop_of_even [AddCommGroup β] [IsOrderedAddMonoid β]
+    {f : β → E} (hf : Continuous f) (heven : Function.Even f) :
+    IsBounded (range f) ↔ f =O[atTop] (1 : β → ℝ) :=
+  ⟨fun h ↦ (hf.isBounded_range_iff_isBigO_atTop_atBot.mp h).1,
+   fun h ↦ hf.isBounded_range_iff_isBigO_atTop_atBot.mpr
+     ⟨h, by simpa only [← neg_atTop, ← Filter.map_neg, isBigO_map, Function.comp_def, heven.eq]⟩⟩
+
+end boundedRange