Import analytic Hamiltonian KAM on compact action domains

LeanPool/ArnoldKAM.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Bingqi Yu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bingqi Yu
+-/
+
+module
+
+public import LeanPool.ArnoldKAM.Arnold1963.Main.Theorem1
+public import LeanPool.ArnoldKAM.Arnold1963.Main.Theorem2
+public import LeanPool.ArnoldKAM.Arnold1963.Audit.W10Example
+public import LeanPool.ArnoldKAM.Arnold1963.Audit.W10Branches
+
+/-!
+# Analytic Hamiltonian KAM on compact action domains
+
+Source: doi:10.5281/zenodo.23232025
+Authors: Bingqi Yu
+Status: verified
+Main declarations: `KamProject.Arnold1963.theorem1`
+Tags: Hamiltonian dynamics, KAM theory, Fourier analysis, symplectic geometry
+MSC: 37J40, 37J35, 42A16
+-/

LeanPool/ArnoldKAM/Arnold1963/Analysis/AnalyticLift.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Bingqi Yu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bingqi Yu
+-/
+
+module
+
+public import LeanPool.ArnoldKAM.Arnold1963.Basic.Functions
+public import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
+public import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
+
+/-!
+Lift continuous multilinear maps and power series to bounded continuous function spaces.
+The norm bounds support analytic integration over compact parameter sets.
+-/
+
+@[expose] public section
+noncomputable section
+open MeasureTheory Set Filter
+open scoped Topology NNReal BoundedContinuousFunction
+namespace KamProject.Arnold1963
+
+variable {X E : Type*} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E]
+
+private theorem lift_bound {m : ℕ} (p : ContinuousMultilinearMap ℂ (fun _ : Fin m => E) ℂ)
+    (v : Fin m → X →ᵇ E) (x : X) :
+    ‖p (fun j => v j x)‖ ≤ ‖p‖ * ∏ j, ‖v j‖ := by
+  exact (p.le_opNorm _).trans (mul_le_mul_of_nonneg_left
+    (Finset.prod_le_prod₀ (fun _ _ => norm_nonneg _) (fun j _ => (v j).norm_coe_le_norm x))
+    (norm_nonneg _))
+
+omit [NormedSpace ℂ E] in
+private theorem eval_update {m : ℕ} [DecidableEq (Fin m)] (v : Fin m → X →ᵇ E) (i : Fin m)
+    (a : X →ᵇ E) (x : X) :
+    (fun j => Function.update v i a j x) = Function.update (fun j => v j x) i (a x) := by
+  ext j
+  by_cases h : j = i <;> simp [h]
+
+/-- Pointwise multilinear evaluation on bounded continuous functions, retaining an operator norm
+bound. -/
+def boundedMultilinearLift {m : ℕ}
+    (p : ContinuousMultilinearMap ℂ (fun _ : Fin m => E) ℂ) :
+    ContinuousMultilinearMap ℂ (fun _ : Fin m => X →ᵇ E) (X →ᵇ ℂ) :=
+  MultilinearMap.mkContinuous
+    { toFun := fun v => BoundedContinuousFunction.ofNormedAddCommGroup
+        (fun x => p (fun j => v j x))
+        (p.cont.comp (continuous_pi (fun j => (v j).continuous)))
+        (‖p‖ * ∏ j, ‖v j‖) (by exact lift_bound p v)
+      map_update_add' := by
+        intro _ v i a b
+        ext x
+        change p (fun j => Function.update v i (a + b) j x) =
+          p (fun j => Function.update v i a j x) + p (fun j => Function.update v i b j x)
+        simp only [eval_update, BoundedContinuousFunction.add_apply, p.map_update_add]
+      map_update_smul' := by
+        intro _ v i c a
+        ext x
+        change p (fun j => Function.update v i (c • a) j x) =
+          c • p (fun j => Function.update v i a j x)
+        simp only [eval_update, BoundedContinuousFunction.smul_apply, p.map_update_smul]
+        }
+    ‖p‖ (fun v => (BoundedContinuousFunction.norm_le (by positivity)).mpr
+      (by exact lift_bound p v))
+
+@[simp] theorem boundedMultilinearLift_apply {m : ℕ}
+    (p : ContinuousMultilinearMap ℂ (fun _ : Fin m => E) ℂ)
+    (v : Fin m → X →ᵇ E) (x : X) : boundedMultilinearLift p v x = p (fun j => v j x) := rfl
+
+theorem norm_boundedMultilinearLift_le {m : ℕ}
+    (p : ContinuousMultilinearMap ℂ (fun _ : Fin m => E) ℂ) :
+    ‖boundedMultilinearLift (X := X) p‖ ≤ ‖p‖ := by
+  apply ContinuousMultilinearMap.opNorm_le_bound (norm_nonneg _)
+  intro v
+  exact (BoundedContinuousFunction.norm_le (by positivity)).mpr (lift_bound p v)
+
+/-- A formal power series lifted coefficientwise to bounded continuous functions. -/
+def boundedSeriesLift (p : FormalMultilinearSeries ℂ E ℂ) :
+    FormalMultilinearSeries ℂ (X →ᵇ E) (X →ᵇ ℂ) := fun m => boundedMultilinearLift (p m)
+
+theorem radius_boundedSeriesLift_le (p : FormalMultilinearSeries ℂ E ℂ) :
+    p.radius ≤ (boundedSeriesLift (X := X) p).radius :=
+  FormalMultilinearSeries.radius_le_of_le (fun m => norm_boundedMultilinearLift_le (p m))
+
+theorem boundedSeriesLift_sum_apply (p : FormalMultilinearSeries ℂ E ℂ)
+    {v : X →ᵇ E} (hv : v ∈ Metric.eball 0 p.radius) (x : X) :
+    (boundedSeriesLift p).sum v x = p.sum (v x) := by
+  have hl : v ∈ Metric.eball 0 (boundedSeriesLift (X := X) p).radius :=
+    lt_of_lt_of_le hv (radius_boundedSeriesLift_le p)
+  have hs := (BoundedContinuousFunction.evalCLM ℂ x).hasSum
+    ((boundedSeriesLift p).summable hl).hasSum
+  have hx : v x ∈ Metric.eball 0 p.radius := by
+    have hv' : ENNReal.ofReal ‖v‖ < p.radius := by
+      simpa [Metric.mem_eball, edist_dist, dist_zero_right] using hv
+    simpa [Metric.mem_eball, edist_dist, dist_zero_right] using
+      (ENNReal.ofReal_le_ofReal (v.norm_coe_le_norm x)).trans_lt hv'
+  exact hs.unique (p.summable hx).hasSum
+
+/-- The continuous linear map sending a vector to its constant function. -/
+def boundedConstCLM : E →L[ℂ] (X →ᵇ E) :=
+  LinearMap.mkContinuous
+    { toFun := BoundedContinuousFunction.const X
+      map_add' := by intros; ext; rfl
+      map_smul' := by intros; ext; rfl }
+    1 (fun v => by simpa using BoundedContinuousFunction.norm_const_le (α := X) v)
+
+@[simp] theorem boundedConstCLM_apply (v : E) (x : X) : boundedConstCLM v x = v := rfl
+
+/-- Integration against a finite measure as a continuous complex linear functional. -/
+def boundedIntegralCLM [MeasurableSpace X] [OpensMeasurableSpace X]
+    (μ : Measure X) [IsFiniteMeasure μ] : (X →ᵇ ℂ) →L[ℂ] ℂ :=
+  LinearMap.mkContinuous
+    { toFun := fun f => ∫ x, f x ∂μ
+      map_add' := fun f g => integral_add (f.integrable μ) (g.integrable μ)
+      map_smul' := by intro c f; exact integral_smul c f }
+    (μ.real univ) (fun f => f.norm_integral_le_mul_norm μ)
+
+end KamProject.Arnold1963

LeanPool/ArnoldKAM/Arnold1963/Analysis/AnalyticUniformLimit.lean

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2026 Bingqi Yu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bingqi Yu
+-/
+
+module
+
+public import LeanPool.ArnoldKAM.Arnold1963.Analysis.PolydiscCauchy
+public import Mathlib.Topology.UniformSpace.UniformConvergence
+public import Mathlib.Topology.Algebra.IsUniformGroup.Order
+public import Mathlib.MeasureTheory.Integral.DominatedConvergence
+
+/-!
+Analyticity of uniform limits on complex polydiscs, using the Cauchy integral formula and
+convergence of weighted integrals over compact sets.
+-/
+
+@[expose] public section
+noncomputable section
+open Set Metric MeasureTheory Complex Filter
+open scoped Topology ENNReal
+namespace KamProject.Arnold1963
+
+theorem analyticAt_cauchyIntegral {n : ℕ} {f : ComplexSpace n → ℂ}
+    {c w : ComplexSpace n} {r : RealSpace n} (hr : ∀ i, 0 ≤ r i)
+    (hf : ContinuousOn f (pi univ (fun i => closedBall (c i) (r i))))
+    (hw : ∀ i, w i ∈ ball (c i) (r i)) :
+    AnalyticAt ℂ (fun a => torusIntegral (fun z => cauchyKernel a z * f z) c r) w := by
+  let K : Set (RealSpace n) := Icc 0 (fun _ => 2 * Real.pi)
+  let μ : Measure (RealSpace n) := volume.restrict K
+  have : IsFiniteMeasure μ := ⟨by
+    change (volume.restrict K) univ < ⊤
+    rw [Measure.restrict_apply_univ]
+    exact isCompact_Icc.measure_lt_top⟩
+  let g : RealSpace n → ComplexSpace n × ℂ := fun t =>
+    (torusMap c r t, (∏ i, (r i : ℂ) * exp (t i * I) * I) * f (torusMap c r t))
+  let F : ComplexSpace n × (ComplexSpace n × ℂ) → ℂ :=
+    fun x => cauchyKernel x.1 x.2.1 * x.2.2
+  have hg : Continuous g := by
+    apply Continuous.prodMk (continuous_torusMap c r)
+    apply Continuous.mul
+    · fun_prop
+    · exact hf.comp_continuous (continuous_torusMap c r) (torusMap_mem_pi_closedBall c hr)
+  have hF : ∀ t ∈ K, AnalyticAt ℂ F (w, g t) := by
+    intro t _
+    apply AnalyticAt.mul
+    · apply Finset.analyticAt_fun_prod
+      intro i _
+      apply AnalyticAt.inv
+      · exact (((ContinuousLinearMap.proj (R := ℂ) (φ := fun _ : Fin n => ℂ) i).analyticAt _).comp
+          (analyticAt_fst.comp analyticAt_snd)).sub
+          (((ContinuousLinearMap.proj (R := ℂ) (φ := fun _ : Fin n => ℂ) i).analyticAt _).comp
+            analyticAt_fst)
+      · exact torusMap_sub_ne_zero hw t i
+    · exact analyticAt_snd.comp analyticAt_snd
+  have hA := analyticAt_integral_compact (μ := μ) hg (K := K) isCompact_Icc measurableSet_Icc hF
+  convert! hA using 1
+  funext a
+  simp only [F, g, cauchyKernel, torusIntegral, smul_eq_mul, μ,
+    Measure.restrict_restrict measurableSet_Icc, inter_self, K]
+  apply setIntegral_congr_fun measurableSet_Icc
+  intro t _
+  ring
+
+theorem tendsto_weightedIntegral_of_uniform_compact
+    {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
+    {μ : Measure X} [IsFiniteMeasureOnCompacts μ] {K : Set X}
+    (hK : IsCompact K) (hKm : MeasurableSet K)
+    {F : ℕ → X → ℂ} {f a : X → ℂ} (hF : ∀ s, ContinuousOn (F s) K)
+    (ha : ContinuousOn a K) (hu : TendstoUniformlyOn F f atTop K) :
+    Tendsto (fun s => ∫ x in K, a x * F s x ∂μ) atTop
+      (𝓝 (∫ x in K, a x * f x ∂μ)) := by
+  have : IsFiniteMeasure (μ.restrict K) := ⟨by
+    rw [Measure.restrict_apply_univ]
+    exact hK.measure_lt_top⟩
+  obtain ⟨C, hC⟩ := hK.bddAbove_image
+    (hu.continuousOn (Eventually.of_forall hF).frequently).norm
+  obtain ⟨B, hB⟩ := hK.bddAbove_image ha.norm
+  apply tendsto_integral_filter_of_norm_le_const
+  · exact Eventually.of_forall fun s => (ha.mul (hF s)).aestronglyMeasurable hKm
+  · refine ⟨max B 0 * (C + 1), ?_⟩
+    have hb := (uniformContinuous_norm.comp_tendstoUniformlyOn hu).eventually_forall_le
+      (show C < C + 1 by linarith) (fun x hx => hC (mem_image_of_mem _ hx))
+    filter_upwards [hb] with s hs
+    filter_upwards [ae_restrict_mem hKm] with x hx
+    rw [norm_mul]
+    exact (mul_le_mul_of_nonneg_right
+      ((hB (mem_image_of_mem _ hx)).trans (le_max_left _ _)) (norm_nonneg _)).trans
+        (mul_le_mul_of_nonneg_left (hs x hx) (le_max_right _ _))
+  · filter_upwards [ae_restrict_mem hKm] with x hx
+    exact tendsto_const_nhds.mul (hu.tendsto_at hx)
+
+theorem analyticAt_uniform_limit_polydisc {n : ℕ} {F : ℕ → ComplexSpace n → ℂ}
+    {f : ComplexSpace n → ℂ} {c : ComplexSpace n} {R : ℝ} (hR : 0 < R)
+    (hF : ∀ s, AnalyticOnNhd ℂ (F s) (closedBall c R))
+    (hu : TendstoUniformlyOn F f atTop (closedBall c R)) : AnalyticAt ℂ f c := by
+  let r : RealSpace n := fun _ => R
+  have hp : closedBall c R = pi univ (fun i => closedBall (c i) (r i)) :=
+    closedBall_pi c hR.le
+  have hfc : ContinuousOn f (closedBall c R) :=
+    hu.continuousOn (Eventually.of_forall fun s => (hF s).continuousOn).frequently
+  have hm (t : RealSpace n) : torusMap c r t ∈ closedBall c R := by
+    rw [hp]
+    exact torusMap_mem_pi_closedBall c (fun _ => hR.le) t
+  have hc (w : ComplexSpace n) (hw : w ∈ ball c R) :
+      torusIntegral (fun z => cauchyKernel w z * f z) c r =
+        (2 * Real.pi * I : ℂ) ^ n * f w := by
+    have hw' : ∀ i, w i ∈ ball (c i) (r i) := by
+      simpa only [ball_pi c hR, mem_univ_pi] using hw
+    let a : RealSpace n → ℂ := fun t =>
+      (∏ i, (r i : ℂ) * exp (t i * I) * I) * cauchyKernel w (torusMap c r t)
+    have ha : Continuous a := by
+      apply Continuous.mul
+      · fun_prop
+      · apply continuous_finsetProd
+        intro i _
+        exact (((continuous_apply i).comp (continuous_torusMap c r)).sub
+          continuous_const).inv₀ (fun t => torusMap_sub_ne_zero hw' t i)
+    have ht := tendsto_weightedIntegral_of_uniform_compact
+      (μ := (volume : Measure (RealSpace n)))
+      (K := Icc (0 : RealSpace n) (fun _ => 2 * Real.pi)) isCompact_Icc measurableSet_Icc
+      (fun s => ((hF s).continuousOn.comp_continuous
+        (continuous_torusMap c r) hm).continuousOn) ha.continuousOn
+      ((hu.comp (torusMap c r)).mono (fun t _ => hm t))
+    have ht' : Tendsto (fun s => torusIntegral (fun z => cauchyKernel w z * F s z) c r)
+        atTop (𝓝 (torusIntegral (fun z => cauchyKernel w z * f z) c r)) := by
+      simpa only [torusIntegral, smul_eq_mul, a, mul_assoc, Function.comp_def] using! ht
+    have he (s : ℕ) := polydisc_cauchy (f := F s) (fun _ => hR) (hp ▸ hF s) hw'
+    have hs : Tendsto (fun s => torusIntegral (fun z => cauchyKernel w z * F s z) c r)
+        atTop (𝓝 ((2 * Real.pi * I : ℂ) ^ n * f w)) := by
+      exact (tendsto_const_nhds.mul (hu.tendsto_at (ball_subset_closedBall hw))).congr'
+        (Eventually.of_forall fun s => (he s).symm)
+    exact tendsto_nhds_unique ht' hs
+  have hA := analyticAt_cauchyIntegral (c := c) (w := c) (fun _ => hR.le)
+    (hp ▸ hfc) (fun i => mem_ball_self hR)
+  have hne : (2 * Real.pi * I : ℂ) ^ n ≠ 0 := by
+    apply pow_ne_zero
+    exact mul_ne_zero (mul_ne_zero (by norm_num) (by exact_mod_cast Real.pi_ne_zero)) I_ne_zero
+  apply (analyticAt_const.mul hA).congr
+    (g := f) (f := fun w => ((2 * Real.pi * I : ℂ) ^ n)⁻¹ *
+      torusIntegral (fun z => cauchyKernel w z * f z) c r)
+  filter_upwards [ball_mem_nhds c hR] with w hw
+  rw [hc w hw, ← mul_assoc, inv_mul_cancel₀ hne, one_mul]
+
+theorem analyticOnNhd_uniform_limit {n : ℕ} {U : Set (ComplexSpace n)}
+    (hU : IsOpen U) {F : ℕ → ComplexSpace n → ℂ} {f : ComplexSpace n → ℂ}
+    (hF : ∀ s, AnalyticOnNhd ℂ (F s) U) (hu : TendstoUniformlyOn F f atTop U) :
+    AnalyticOnNhd ℂ f U := by
+  intro c hc
+  obtain ⟨ε, hε, hsub⟩ := Metric.mem_nhds_iff.mp (hU.mem_nhds hc)
+  have hs : closedBall c (ε / 2) ⊆ U :=
+    (closedBall_subset_ball (half_lt_self hε)).trans hsub
+  exact analyticAt_uniform_limit_polydisc (half_pos hε)
+    (fun s => (hF s).mono hs) (hu.mono hs)
+
+end KamProject.Arnold1963