El teorema del punto fijo de Banach dice que si tenemos un espacio métrico completo no vacío , entonces cualquier función uniformemente contractiva tiene un punto fijo único . Sin embargo, la prueba de este teorema requiere el axioma de elección: debemos elegir un elemento arbitrario para comenzar a iterar desde, para obtener la secuencia de Cauchy . f : A → A μ ( f ) a ∈ A f a , f ( a ) , f 2 ( a ) , f 3 ( a ) , …
- ¿Cómo se establecen los teoremas de punto fijo en el análisis constructivo?
- Además, ¿hay referencias concisas a espacios métricos constructivos?
La razón por la que pregunto es que quiero construir un modelo del Sistema F en el que los tipos también tengan una estructura métrica (entre otras cosas). Es bastante útil que, en la teoría de conjuntos constructivos, podamos preparar una familia de conjuntos , de modo que esté cerrada bajo productos, exponenciales y familias indexadas en , lo que facilita dar un modelo del Sistema F.U U
Sería muy bueno si pudiera cocinar una familia similar de espacios ultramétricos constructivos. Pero dado que agregar opciones a la teoría de conjuntos constructiva lo hace clásico, obviamente necesito tener más cuidado con los teoremas de punto fijo, y probablemente también con otras cosas.
fuente
Respuestas:
El axioma de elección se usa cuando hay una colección de "cosas" y usted elige un elemento para cada "cosa". Si solo hay una cosa en la colección, ese no es el axioma de elección. En nuestro caso, solo tenemos un espacio métrico y estamos "eligiendo" un punto en él. Entonces ese no es el axioma de elección sino la eliminación de cuantificadores existenciales, es decir, tenemos una hipótesis y decimos "deja que sea tal que ". Desafortunadamente, la gente a menudo dice " elija tal que ", que luego parece la aplicación del axioma de elección.x ∈ A ϕ ( x ) x ∈ A ϕ ( x )∃ x ∈ A . ϕ ( x ) x ∈ A ϕ ( x ) x ∈ A ϕ ( x )
Como referencia, aquí hay una prueba constructiva del teorema del punto fijo de Banach.
Teorema: una contracción en un espacio métrico completo habitado tiene un punto fijo único.
Prueba. Supongamos que es un espacio métrico completo habitado yf : M → M es una contracción. Debido a que f es una contracción existe α tal que 0 < α < 1 y d ( f ( x ) , f ( y ) ) ≤ α ⋅ d ( x , y ) para todo x , y ∈ M( M, d) F: M→ M F α 0 < α < 1 re( f( x ) , f( y) ) ≤ α ⋅ d( x , y) x , y∈ M .
Supongamos que y v son un punto fijo de f . Entonces tenemos d ( u , v ) = d ( f ( u ) , f ( v ) ) ≤ α d ( u , v ) de donde se deduce que 0 ≤ d ( u , v ) ≤ ( α - 1 ) d ( u , v ) ≤tu v F
Queda por demostrar la existencia de un punto fijo. Debido a que está habitado existe x 0 ∈ M . Defina la secuencia ( x i ) recursivamente por x i + 1 = f ( x i ) . Podemos demostrar por inducción que d ( x i , x i + 1 ) ≤ α i ⋅ d ( x 0 , x 1 ) . De esto se deduce queMETRO X0 0∈ M ( xyo)
Observaciones:
Tuve cuidado de no decir "elegir " y "elegir x 0 ". Es común decir tales cosas, y solo se suman a la confusión que impide que los matemáticos comunes puedan decir qué es y qué no es el axioma de elección.α X0 0
Finalmente, los siguientes teoremas de punto fijo tienen versiones constructivas:
Ahora que es más información de la que pediste.
fuente