leanprover-community/mathlib4

Prove that inversion is discontinuous at the center

Aberta

#5.939 aberto em 16 de jul. de 2023

Ver no GitHubGuia do colaborador
 (4 comentários) (0 reação) (0 responsável)Lean (1.592 forks)github user discovery
good first issuet-analysist-euclidean-geometryt-topology

Métricas do repositório

Stars
 (3.869 estrelas)
Métricas de merge de PR
 (Nenhuma PRs mesclada em 30d)

Description

  • Prove Tendsto (inversion c R) (𝓝[≠] c) cobounded if R ≠ 0.
  • Deduce that inversion c R is discontinuous at c if R ≠ 0 and the vector space is nontrivial.
  • Deduce that fderiv (inversion c R) c is zero, thus fderiv (inversion c R) x = ((R / dist x c) ^ 2 • (reflection (ℝ ∙ (x - c))ᗮ : F →L[ℝ] F)) x for all x (see #5937 for the case x ≠ c).

Guia do colaborador

Direção de pesquisa
Estude as definições existentes de inversão e reflexão no mathlib4. Examine o PR #5937 para o caso x ≠ c. Prove o primeiro ponto mostrando que a inversão tende a cobounded. Depois, deduza a descontinuidade e calcule a derivada de Fréchet.
Pilha de tecnologia
None
Domain
backend
Tipo Issue
Pesquisa
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
3
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
1-2 dias
Status da atividadeQuão disponível o issue aparece agora: novo, ativo, obsoleto, bloqueado ou aguardando entrada do mantenedor.
Ativo
ClarityCom que clareza o issue explica a mudança esperada, os critérios de aceitação e a próxima etapa.
Claro
Prerequisites
GitLean basics
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
35