Prove2Me

Smooth gauge radius at

Proved
ConvexAnalysis.smooth_gauge_radius_at

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

convex-geometryreal-analysis

The inverse-gauge scalar factor is smooth at a frontier point when a smooth frontier defining function has nonzero radial derivative there and the stated convexity, boundedness and interior hypotheses hold.

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

Preamble
import Definitions.Def_BirkhoffGlobalSection_ConvexRegularizationModel
import Mathlib.Analysis.Convex.GaugeRescale
import Mathlib.Analysis.Calculus.ImplicitContDiff
import Mathlib.Analysis.Calculus.LocalExtr.Basic
import Mathlib.Analysis.LocallyConvex.Separation

import Theorems.Thm_ConvexAnalysis_gauge_radius_frontier
open BirkhoffGlobalSection Filter Set
open scoped ContDiff Topology


set_option autoImplicit false
set_option maxHeartbeats 800000
Formal statement
theorem ConvexAnalysis.smooth_gauge_radius_at (K : Set Phase) (hK : Convex ℝ K)
    (h0 : K ∈ nhds (0 : Phase)) (hb : Bornology.IsVonNBounded ℝ K)
    (F : Phase → ℝ) (hzero : ∀ x ∈ frontier K, F x = 0)
    (u : Phase) (hu : u ∈ frontier K) (hc : ContDiffAt ℝ ∞ F u)
    (hrad : fderiv ℝ F u u ≠ 0) :
    ContDiffAt ℝ ∞ (fun x => (gauge K x)⁻¹) u := by sorry
Source
Original auxiliary result from the accepted source Solutions/Sol_ConvexAnalysis_convex_frontier_radial_derivative_ne_zero.lean:30. Exact quantified statement retained; foundational calculus and geometry are imported from Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.

View graph