Generalización de la notación Big O a espacios vectoriales arbitrarios

Question

Estoy construyendo una biblioteca Coq para la notación Big-O . Naturalmente, me gustaría que fuera lo más general posible. La página de Wikipedia sobre la notación Big-O dice

La generalización a funciones que toman valores en cualquier espacio vectorial normado es sencilla (sustituyendo los valores absolutos por las normas)

Por supuesto, no hay citas en línea. Mi intento de hacerlo dio como resultado lo siguiente:

Definition big_O (f g : V -> V) : Prop :=
    ∃ k : K, 0 < k ∧ exists n0 : K, 0 < n0 ∧ ∀ n : V, n0 ≤ ∥n∥ -> ∥f n∥ ≤ k * ∥g n∥.

Lo que se traduce en lo siguiente en lenguaje informal:

Definición 1. Dado un espacio vectorial $V$ con (semi)norma $\lVert-\rVert$ sobre un campo totalmente ordenado $(K,\leq)$ y funciones $f,g:V\to V$ decimos que $f\in O(g)$ si existe algún tipo de valor positivo $k$ y $n_0$ en $K$ tal que para todos los vectores $n\in V$ con $n_0 \leq \lVert n\rVert$ , $\rVert f(n)\rVert\leq k\cdot\lVert g(n)\rVert$ .

Sin embargo, me parece que la siguiente definición es algo más elegante y general:

Definition big_O (f g : V -> V) : Prop :=
    ∃ k : K, k ≠ 0 ∧ ∃ n0 : V, ∀ n : V, ∥n0∥ ≤ ∥n∥ -> ∥f n∥ ≤ ∥k · g n∥.

Lo que se traduce en lo siguiente:

Definición 2. Dado un espacio vectorial $V$ con (semi)norma $\lVert-\rVert$ sobre un campo totalmente ordenado $(K,\leq)$ y funciones $f,g:V\to V$ decimos que $f\in O(g)$ si existe algún tipo de $k$ y algunos $n_0$ en $V$ tal que para todos los vectores $n\in V$ con $\lVert n_0\rVert \leq \lVert n\rVert$ , $\lVert f(n)\rVert\leq \lVert k\cdot g(n)\rVert$ .

Así que creo que tengo algunas preguntas:

1. ¿Alguien tiene una buena referencia para la generalización a los espacios vectoriales?
2. ¿Crees que estas definiciones son equivalentes? ¿Alguna prueba o contraejemplo?
3. Esto es algo basado en la opinión, pero ¿algún argumento para usar uno u otro?

Answer 1

He aquí una generalización directa de la notación asintótica para funciones que toman valores en espacios vectoriales normados:

Dejemos que $X$ sea un espacio topológico, $\overline X\supseteq X$ un superespacio en el que $X$ es denso, y $a\in\overline X$ . Sea $Y$ sea un espacio vectorial normado, y $f,g\colon X\to Y$ . Entonces decimos

• $f(x)=O(g(x))$ como $x\to a$ si hay una vecindad $U\ni a$ y $q>0$ tal que $\|f(x)\|\le q\left\|g(x)\right\|$ para todos $x\in U\cap X$ ;

• $f(x)=o(g(x))$ como $x\to a$ si para cada $q>0$ hay una vecindad $U\ni a$ tal que $\|f(x)\|\le q\left\|g(x)\right\|$ para todos $x\in U\cap X$ .

Esto es para normas estándar de valor real. Parece que también te interesan las normas valoradas en campos ordenados no arquimédicos $K$ . En este caso, hay al menos dos posibilidades útiles de cómo lanzar la definición, a saber (1) tomando $q\in\mathbb Q$ o (2) tomando $q\in K$ . La elección de uno u otro depende del caso de uso previsto.

Es posible hacer más generalizaciones, ya que en realidad no utilizamos la mayor parte de la estructura de $Y$ .

Al parecer, usted está tratando de definir sólo el caso especial con $a=\infty$ . Por lo tanto, hay que decidir cuáles son las vecindades adecuadas del infinito en sus espacios (¿complementos de conjuntos acotados? ¿complementos de conjuntos compactos?).