Hamiltonian radial contact continuousAt

Proved

BirkhoffGlobalSection.hamiltonian_radial_contact_continuousAt

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometryreal-analysis

The radial contact pairing with a smooth Hamiltonian vector field is continuous at the base point.

All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.

Preamble

import Theorems.Thm_BirkhoffGlobalSection_convex_model_boundary_contact_positive
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Analysis.Calculus.Deriv.MeanValue
import Mathlib.Topology.Order.IntermediateValue
import Mathlib.Topology.Order.Compact
import Mathlib.Order.Hom.Set
import Mathlib.Analysis.Calculus.Deriv.Inverse
import Mathlib.MeasureTheory.Integral.DominatedConvergence
import Mathlib.Analysis.Calculus.MeanValue
import Theorems.Thm_BirkhoffGlobalSection_hamiltonian_radial_characteristic_normalization

open Set
open scoped Topology ContDiff



set_option autoImplicit false
set_option maxHeartbeats 800000

Formal statement

theorem BirkhoffGlobalSection.hamiltonian_radial_contact_continuousAt
    (F : BirkhoffGlobalSection.Phase → ℝ) (y : BirkhoffGlobalSection.Phase)
    (hF : ContDiffAt ℝ ∞ F y) :
    ContinuousAt (fun x => BirkhoffGlobalSection.phaseRadialContact x
      (BirkhoffGlobalSection.hamiltonianVectorField F x)) y := by sorry

Source

Original auxiliary result from the accepted source Solutions/Sol_BirkhoffGlobalSection_convex_model_complete_normalized_flow_of_model_fields.lean:333. Exact quantified statement retained; foundational calculus and geometry are imported from Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.

View graph