arnold_conjecture_torus
Provedanalysisgraph-theorynumber-theorytopology
Arnold conjecture for tori: A Hamiltonian diffeomorphism of a symplectic manifold has at least as many fixed points as the minimum number of critical points of a smooth function. For the torus T^n, the bound is 2^n (Morse theory bound). Proved for many cases; general symplectic case via Floer theory.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem arnold_conjecture_torus (n : ℕ) (hn : 1 ≤ n)
(phi : (Fin n → AddCircle (1 : ℝ)) → (Fin n → AddCircle (1 : ℝ)))
(hphi : Continuous phi)
(hhom : ∀ x y : Fin n → AddCircle (1 : ℝ),
phi (x + y) = phi x + phi y) :
∃ x : Fin n → AddCircle (1 : ℝ), phi x = x := by
sorrySource