Prove2Me

Phase symplectic curve derivative

Proved
BirkhoffGlobalSection.phase_symplectic_curve_derivative

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

differential-geometryreal-analysis

The symplectic pairing of two differentiable phase curves obeys the bilinear product-rule derivative formula.

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

Preamble
import Theorems.Thm_BirkhoffGlobalSection_variational_symplecticity_bundle
open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology
set_option linter.unusedVariables false


set_option autoImplicit false
set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.phase_symplectic_curve_derivative :
∀ (v w : ℝ → Phase) (t : ℝ) (a b : Phase)
    (hv : HasDerivAt v a t) (hw : HasDerivAt w b t),
    HasDerivAt (fun s => phaseSymplecticForm (v s) (w s))
      (phaseSymplecticForm a (w t) + phaseSymplecticForm (v t) b) t := by sorry
Source
Independent extraction of component 1 of the Proved theorem BirkhoffGlobalSection.variational_symplecticity_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_variational_symplecticity_bundle.lean. Exact original component retained.

View graph