Local nullity of the zero level at a regular scalar coordinate

Proved

BianchiIX.exists_local_null_scalar_level

by trppppp · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

Let $g:\mathbb R^n\to\mathbb R$ be $C^1$ at $x$ and suppose $Dg_x e_i\ne0$ for some coordinate $i$ . There exists an open $U\ni x$ such that $\lambda_n(U\cap g^{-1}(0))=0$ .

Preamble

import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
import Mathlib.MeasureTheory.Function.Jacobian
import Mathlib.Topology.Compactness.Lindelof

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set MeasureTheory

Formal statement

theorem BianchiIX.exists_local_null_scalar_level {n : ℕ} {g : (Fin n → ℝ) → ℝ} {x : Fin n → ℝ}
    (hg : ContDiffAt ℝ 1 g x) {i : Fin n}
    (hi : fderiv ℝ g x (Pi.single i 1) ≠ 0) :
    ∃ U : Set (Fin n → ℝ), IsOpen U ∧ x ∈ U ∧ volume (U ∩ {y | g y = 0}) = 0 := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Measure/RegularLevelNull.lean#L25-L71

View graph