Weighted contact curve derivative

Proved

BirkhoffGlobalSection.weighted_contact_curve_derivative

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

differential-geometryreal-analysis

Along differentiable base and vector curves, a differentiable weighted radial contact pairing obeys the displayed scalar and 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_contact_variation_preservation_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.weighted_contact_curve_derivative :
∀ (f : Phase → ℝ) (q v : ℝ → Phase)
    (t : ℝ) (a b : Phase) (hf : DifferentiableAt ℝ f (q t))
    (hq : HasDerivAt q a t) (hv : HasDerivAt v b t),
    HasDerivAt (fun s => f (q s) * phaseRadialContact (q s) (v s))
      (fderiv ℝ f (q t) a * phaseRadialContact (q t) (v t) +
        f (q t) * (phaseRadialContact a (v t) + phaseRadialContact (q t) b)) t := by sorry

Source

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

View graph