C-infinity convergence of a periodic map evaluated along a convergent family
ProvedFiniteEnergyPlane.tendstoZeroCInfty_comp_periodicasymptotic-analysisdifferential-calculusreal-analysis
Let be a finite-dimensional real normed space, a real normed space, , , and let be on , -periodic in its first variable there, with . If satisfies in , uniformly in , as , then also
This carries convergence through coordinates built along a periodic orbit, such as tube coordinates near a Reeb orbit.
Formalization Note convergence is TendstoZeroCInfty (smooth on some , every derivative tends to uniformly in ). is a finite-dimensional real normed space and any real normed space; is only assumed smooth and periodic on .
Preamble
import Definitions.Def_FiniteEnergyPlane_Asymptotics
Formal statement
namespace FiniteEnergyPlane
open Metric
open scoped ContDiff
/-- Let `Φ(φ, v)` be smooth on `ℝ × B(0, r)`, `T`-periodic in `φ`, with `Φ(φ, 0) = 0`. If
`v(s, t) → 0` in `C^∞` on the end, then so does `Φ(a t + b, v(s, t))`, for any `a, b ∈ ℝ`. -/
theorem tendstoZeroCInfty_comp_periodic {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
(Φ : ℝ × E → F) (T r a b : ℝ) (hT : 0 < T) (hr : 0 < r)
(hΦ : ContDiffOn ℝ ∞ Φ (Set.univ ×ˢ ball (0 : E) r))
(hper : ∀ (φ : ℝ) (v : E), ‖v‖ < r → Φ (φ + T, v) = Φ (φ, v))
(h0 : ∀ φ : ℝ, Φ (φ, 0) = 0)
(v : ℝ × ℝ → E) (hv : TendstoZeroCInfty v) :
TendstoZeroCInfty (fun p : ℝ × ℝ => Φ (a * p.2 + b, v p)) := by
sorry
end FiniteEnergyPlane
Source
Used for U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Theorems 2.10-2.11, and H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13 (1996)