O teorema do ponto fixo de Banach diz que, se tivermos um espaço métrico completo não vazio , qualquer função uniformemente contrativa possui um ponto fixo único . No entanto, a prova desse teorema requer o axioma da escolha - precisamos escolher um elemento arbitrário para iniciar a iteração de, para obter a sequência de Cauchy . μ ( f ) a ∈ A f a , f ( a ) , f 2 ( a ) , f 3 ( a ) , …
- Como os teoremas do ponto fixo são declarados na análise construtiva?
- Além disso, existem referências concisas a espaços métricos construtivos?
O motivo pelo qual pergunto é que quero construir um modelo do Sistema F no qual os tipos também tenham estrutura métrica (entre outras coisas). É bastante útil que, na teoria construtiva dos conjuntos, possamos criar uma família de conjuntos , de modo que seja fechado em produtos, exponenciais e famílias indexadas em , o que facilita a criação de um modelo do Sistema F.U U
Seria muito bom se eu pudesse criar uma família semelhante de espaços ultramétricos construtivos. Mas como adicionar opções à teoria construtiva dos conjuntos a torna clássica, obviamente eu preciso ter mais cuidado com os teoremas do ponto fixo e provavelmente outras coisas também.
fonte
Respostas:
O axioma da escolha é usado quando há uma coleção de "coisas" e você escolhe um elemento para cada "coisa". Se houver apenas uma coisa na coleção, esse não é o axioma da escolha. No nosso caso, temos apenas um espaço métrico e estamos "escolhendo" um ponto nele. Então isso não é o axioma de escolha, mas a eliminação de quantificadores existenciais, ou seja, temos uma hipótese e dizemos "seja x ∈ A tal que ϕ ( x ) ". Infelizmente, as pessoas costumam dizer "∃x∈A.ϕ(x) x∈A ϕ(x) x∈A ", que se parece com a aplicação do axioma de escolha.ϕ(x)
Para referência, aqui está uma prova construtiva do teorema do ponto fixo de Banach.
Teorema: Uma contração em um espaço métrico completo habitado tem um ponto fixo exclusivo.
Prova. Suponha que seja um espaço métrico completo habitado ef : M → M é uma contração. Porque f é um contracção existe α tal que 0 < α < 1 e d ( f ( x ) , f ( y ) ) ≤ α ⋅ d ( x , y ) para todos os x , y ∈ M(M,d) f:M→M f α 0<α<1 d( f( x ) , f( y) ) ≤ α ⋅ d( x , y) x , y∈ M .
Suponha que e v são ponto de fixa f . Então temos d ( u , v ) = d ( f ( u ) , f ( v ) ) ≤ α d ( u , v ) a partir do qual se segue que 0 ≤ d ( u , v ) ≤ ( α - 1 ) d ( u , v ) ≤você v f
Resta provar a existência de um ponto fixo. Porque é habitado existe x 0 ∈ M . Defina a sequência ( x i ) recursivamente por x i + 1 = f ( x i ) . Podemos provar por indução que d ( x i , x i + 1 ) ≤ α i ⋅ d ( x 0 , x 1 ) . Daí resulta queM x0 0∈ M ( xEu)
Observações:
Tomei cuidado para não dizer "escolha " e "escolha x 0 ". É comum dizer essas coisas, e elas apenas aumentam a confusão que impede os matemáticos comuns de serem capazes de dizer o que é e o que não é o axioma da escolha.α x0 0
Finalmente, os seguintes teoremas de ponto fixo têm versões construtivas:
Agora isso é mais informações do que você pediu.
fonte