Smooth radial gauge inverse

Proved

BirkhoffGlobalSection.smooth_radial_gauge_inverse

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

convex-geometryreal-analysis

For a bounded convex body containing a neighborhood of zero and a smooth frontier defining function with nonzero radial derivative, its inverse-gauge radial chart is smooth away from zero.

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

Preamble

import Definitions.Def_BirkhoffGlobalSection_ConvexRegularizationModel
import Theorems.Thm_BirkhoffGlobalSection_radial_normalization_contact_identity
import Mathlib.Analysis.Convex.GaugeRescale
import Mathlib.Analysis.Calculus.ImplicitContDiff

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


set_option autoImplicit false
set_option maxHeartbeats 800000

Formal statement

theorem BirkhoffGlobalSection.smooth_radial_gauge_inverse
    (B : Set Phase) (hc : Convex ℝ B) (h0 : B ∈ 𝓝 (0 : Phase))
    (hb : Bornology.IsVonNBounded ℝ B) (F : Phase → ℝ)
    (hzero : ∀ y ∈ frontier B, F y = 0)
    (hsmooth : ∀ y ∈ frontier B, ContDiffAt ℝ ∞ F y)
    (hrad : ∀ y ∈ frontier B, fderiv ℝ F y y ≠ 0)
    (u : Phase) (hu : u ≠ 0) :
    ContDiffAt ℝ ∞ (fun x : Phase => (gauge B x)⁻¹ • x) u := by sorry

Source

Original auxiliary result from the accepted source Solutions/Sol_BirkhoffGlobalSection_smooth_radial_gauge_chart.lean:38. Exact quantified statement retained; foundational calculus and geometry are imported from Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.

View graph