Prove2Me

Radial contact differentiable

Proved
BirkhoffGlobalSection.radial_contact_differentiable

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

differential-geometryreal-analysis

For each fixed phase vector w, the radial contact functional in its base variable is differentiable, and its differential on v is the radial contact pairing of v with w.

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

Preamble
import Definitions.Def_BirkhoffGlobalSection_TransverseHopf
import Mathlib.Analysis.Calculus.FDeriv.Mul

open scoped ContDiff Topology
open BirkhoffGlobalSection Set


set_option autoImplicit false
set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.radial_contact_differentiable (u w : Phase) :
    DifferentiableAt ℝ (fun x : Phase => phaseRadialContact x w) u ∧
      (∀ v : Phase, fderiv ℝ (fun x : Phase => phaseRadialContact x w) u v =
        phaseRadialContact v w) := by sorry
Source
Original auxiliary result from the accepted source Solutions/Sol_BirkhoffGlobalSection_weighted_radial_contact_exterior_derivative.lean:7. Exact quantified statement retained; foundational calculus and geometry are imported from Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.

View graph