Radial normalize regular

Proved

BirkhoffGlobalSection.radial_normalize_regular

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

differential-geometryreal-analysis

Radial normalization is smooth at a phase point with positive squared radius, and its value lies on the unit three-sphere.

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

Preamble

import Theorems.Thm_BirkhoffGlobalSection_smooth_sphere_reeb_bundle
open BirkhoffGlobalSection Set Filter SignType
open scoped ContDiff Topology
set_option linter.unusedVariables false


set_option autoImplicit false
set_option maxHeartbeats 800000

Formal statement

theorem BirkhoffGlobalSection.radial_normalize_regular :
∀ (x : Phase) (hx : 0 < zNormSq x + wNormSq x),
    ContDiffAt ℝ ∞ radialNormalize x ∧ radialNormalize x ∈ unitThreeSphere := by sorry

Source

Independent extraction of component 1 of the Proved theorem BirkhoffGlobalSection.smooth_sphere_reeb_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_smooth_sphere_reeb_bundle.lean. Exact original component retained.

View graph