Smooth germs on a compact set give a uniform neighborhood and Lipschitz bound

Proved

BianchiIX.exists_compact_smooth_neighborhood

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

bianchi-ix-era-statisticsdynamical-systems

Let $E$ be a finite-dimensional real normed space, $F$ a real normed space, $S\subset E$ compact, $P$ a predicate on $E$ , and $f:E\to F$ . Suppose each $x\in S$ has a neighborhood where $P(y)$ holds and $f$ is $C^2$ at $y$ . Then there are $\delta>0$ and $C\geq1$ such that, whenever $x\in S$ and $\|y-x\|\leq\delta$ ,

P(y),\qquad f\text{ is }C^2\text{ at }y,\qquad \|f(y)\|\leq C,\qquad \|f(y)-f(x)\|\leq C\|y-x\|.

Preamble

import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Topology.Order.Compact
import Mathlib.Tactic.NormNum
import Mathlib.Topology.MetricSpace.Thickening

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set Filter Metric
open scoped Topology

Formal statement

theorem BianchiIX.exists_compact_smooth_neighborhood
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    {S : Set E} (hS : IsCompact S) {P : E → Prop} {f : E → F}
    (hreg : ∀ x ∈ S, ∀ᶠ y in 𝓝 x, P y ∧ ContDiffAt ℝ 2 f y) :
    ∃ δ > (0 : ℝ), ∃ C ≥ (1 : ℝ), ∀ x ∈ S, ∀ y : E, ‖y - x‖ ≤ δ →
      P y ∧ ContDiffAt ℝ 2 f y ∧ ‖f y‖ ≤ C ∧ ‖f y - f x‖ ≤ C * ‖y - x‖ := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/CompactSmoothNeighborhood.lean#L10-L42

View graph