CompactInverseSections.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite continuous inverse sections on a compact parameter family

The common image ball is retained together with continuous amplitude choices, rather than just existential preimages. This is the form needed to sample endpoints measurably in a stationary volume argument.

theorem OAI.PolycyclicRecognition.exists_finite_uniform_inverse_sections line 26

Source documentation

Finitely many actual schemes admit bounded continuous inverse sections on one common ball, uniformly over the compact parameter set.

theorem exists_finite_uniform_inverse_sections
    (f : J → P × E → F) {K : Set P} (hK : IsCompact K)
    (h : ∀ p ∈ K, ∃ j, ContDiffAt ℝ 1 (f j) (p, 0) ∧ f j (p, 0) = 0 ∧
      Function.Bijective (fun v : E => fderiv ℝ (f j) (p, 0) (0, v)))
    {R : ℝ} (hR : 0 < R) :
    ∃ (S : Finset J) (ε : ℝ), 0 < ε ∧ ∀ p ∈ K, ∃ j ∈ S,
      ∃ s : F → E, ContinuousOn s (ball 0 ε) ∧
        ∀ y ∈ ball (0 : F) ε, f j (p, s y) = y ∧ ‖s y‖ < R := by
…