First integral variation conserved

Proved

BirkhoffGlobalSection.first_integral_variation_conserved

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

differential-geometryreal-analysis

For a smooth first integral and supplied trajectory and variational solution of a differentiable vector field, the first integral's differential applied to the variation is conserved under the displayed local first-integral hypotheses.

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

Preamble

import Theorems.Thm_BirkhoffGlobalSection_reverse_radial_variation_bundle
open BirkhoffGlobalSection Set Filter SignType
open scoped ContDiff Topology
set_option linter.unusedVariables false


set_option autoImplicit false
set_option maxHeartbeats 800000

Formal statement

theorem BirkhoffGlobalSection.first_integral_variation_conserved :
∀ (F : Phase → ℝ) (X : Phase → Phase)
    (x v : ℝ → Phase) (hF : ∀ t, ContDiffAt ℝ ∞ F (x t))
    (hX : ∀ t, DifferentiableAt ℝ X (x t))
    (hx : ∀ t, HasDerivAt x (X (x t)) t)
    (hv : ∀ t, HasDerivAt v (fderiv ℝ X (x t) (v t)) t)
    (hzero : ∀ t, (fun y => fderiv ℝ F y (X y)) =ᶠ[𝓝 (x t)] (fun _ => (0 : ℝ))),
    ∀ t, fderiv ℝ F (x t) (v t) = fderiv ℝ F (x 0) (v 0) := by sorry

Source

Independent extraction of component 2 of the Proved theorem BirkhoffGlobalSection.reverse_radial_variation_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_reverse_radial_variation_bundle.lean. Exact original component retained.

View graph