Convex model radial derivative positive
ProvedBirkhoffGlobalSection.convex_model_radial_derivative_positiveconvex-geometryreal-analysis
The convex model Hamiltonian has strictly positive radial derivative at every boundary point.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained. This is a conditional result for the defined convex regularization model, not a global-section or index-existence theorem.
Preamble
import Theorems.Thm_ConvexAnalysis_convex_frontier_radial_derivative_positive import Definitions.Def_BirkhoffGlobalSection_TransverseHopf open BirkhoffGlobalSection ConvexAnalysis Filter Set open scoped ContDiff Topology set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.convex_model_radial_derivative_positive {μ c : ℝ}
(M : ConvexRegularizationModel μ c) :
∀ y ∈ frontier M.body, 0 < fderiv ℝ M.modelHamiltonian y y := by sorrySource
Original auxiliary result from the accepted source Solutions/Sol_BirkhoffGlobalSection_convex_model_boundary_contact_positive.lean:7. Exact quantified statement retained; foundational calculus and geometry are imported from Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.