Prove2Me

Positive clock reparametrized derivative

Proved
BirkhoffGlobalSection.positive_clock_reparametrized_derivative

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

differential-geometryreal-analysis

Reparametrizing a differentiable real-time curve by the inverse of a positive differentiable order clock divides its velocity by the forward clock rate at inverse time.

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

import Theorems.Thm_BirkhoffGlobalSection_positive_clock_inverse_derivative
open Set
open scoped Topology ContDiff



set_option autoImplicit false
set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.positive_clock_reparametrized_derivative
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (clock : ℝ ≃o ℝ) (r : ℝ → ℝ) (y X : ℝ → E)
    (hd : ∀ t, HasDerivAt clock (r t) t) (hpos : ∀ t, 0 < r t)
    (hy : ∀ t, HasDerivAt y (X t) t) (t : ℝ) :
    HasDerivAt (fun v => y (clock.symm v))
      ((r (clock.symm t))⁻¹ • X (clock.symm t)) t := by sorry
Source
Original auxiliary result from the accepted source Solutions/Sol_BirkhoffGlobalSection_convex_model_complete_normalized_flow_of_model_fields.lean:152. Exact quantified statement retained; foundational calculus and geometry are imported from Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.

View graph