Prove2Me

Loop actions converge under Cloc∞C^\infty_{loc} convergence

Proved
FiniteEnergyPlane.tendsto_loopAction_of_tendstoCInftyLocOn

by Mazecto · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

pseudoholomorphic-curvessymplectic-geometrysymplectization

Let S=H−1(1)⊂R2n+2S=H^{-1}(1)\subset\mathbb{R}^{2n+2} be a strictly star-shaped level, U⊆CU\subseteq\mathbb{C} open, and uk,u0:C→R2n+2u_k,u_0:\mathbb{C}\to\mathbb{R}^{2n+2} maps that are C∞C^\infty on UU and do not vanish on UU. If uk→u0u_k\to u_0 in Cloc∞(U)C^\infty_{loc}(U), then for every smooth loop γ:R→U\gamma:\mathbb{R}\to U

∫01λ0(ℓk(t)) ℓk′(t) dt  ⟶  ∫01λ0(ℓ0(t)) ℓ0′(t) dt,ℓk=proj∘uk∘γ,\int_0^1\lambda_0\big(\ell_k(t)\big)\,\ell_k'(t)\,dt\;\longrightarrow\;\int_0^1\lambda_0\big(\ell_0(t)\big)\,\ell_0'(t)\,dt,\qquad \ell_k=\mathrm{proj}\circ u_k\circ\gamma,

that is, the actions ∫γuk∗λ\int_\gamma u_k^*\lambda converge to ∫γu0∗λ\int_\gamma u_0^*\lambda.

Formalization Note Cloc∞(U)C^\infty_{loc}(U) convergence is JHolomorphic.TendstoCInftyLocOn: every derivative converges uniformly on every compact subset of UU. The action is loopAction along γ\gamma; only t∈[0,1]t\in[0,1] enters.

Preamble
import Definitions.Def_FiniteEnergyPlane_Setting
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Let `S = H⁻¹(1)` be strictly star-shaped, `U ⊆ ℂ` open, and `u k → u₀` in `C^∞_loc(U)`, where
all maps are `C^∞` on `U` and avoid `0` there. Then for every smooth loop `γ : ℝ → ℂ` with image
in `U`, the loop actions `loopAction H (u k) γ` converge to `loopAction H u₀ γ`. -/
theorem tendsto_loopAction_of_tendstoCInftyLocOn {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (U : Set ℂ) (hU : IsOpen U) (u : ℕ → ℂ → V n)
    (u₀ : ℂ → V n) (hu : ∀ k, ContDiffOn ℝ ∞ (u k) U) (hu₀ : ContDiffOn ℝ ∞ u₀ U)
    (hne : ∀ k, ∀ z ∈ U, u k z ≠ 0) (hne₀ : ∀ z ∈ U, u₀ z ≠ 0)
    (hconv : JHolomorphic.TendstoCInftyLocOn u u₀ U) (γ : ℝ → ℂ) (hγ : ContDiff ℝ ∞ γ)
    (hγU : ∀ t, γ t ∈ U) :
    Tendsto (fun k => loopAction H (u k) γ) atTop (𝓝 (loopAction H u₀ γ)) := by
  sorry

end FiniteEnergyPlane
Source
U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, arXiv:0812.4076, § 4 (supporting lemma for Lemma 4.16)

View graph