ParametricInverseSection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous local inverse sections with parameters

For the square amplitude map in a generator scheme, the parameter-preserving inverse function theorem supplies a continuous choice of amplitudes, jointly with the normalized group law. Its source bound is retained explicitly for the subsequent measurable endpoint sampling.

theorem OAI.PolycyclicRecognition.parameter_joint_derivative_bijective line 27

theorem OAI.PolycyclicRecognition.exists_parametric_inverse_section line 46

Source documentation

Nearby parameters admit a common target ball and continuous local amplitude choices of the prescribed bounded size.

theorem exists_parametric_inverse_section (f : P × E → F) (p : P)
    (hf : ContDiffAt ℝ 1 f (p, 0)) (hz : f (p, 0) = 0)
    (hbij : Function.Bijective (fun v : E => fderiv ℝ f (p, 0) (0, v)))
    {R : ℝ} (hR : 0 < R) :
    ∃ U : Set P, IsOpen U ∧ p ∈ U ∧ ∃ ε : ℝ, 0 < ε ∧
      ∃ s : P × F → E, ContinuousOn s (U ×ˢ ball 0 ε) ∧
        ∀ q ∈ U, ∀ y ∈ ball (0 : F) ε, f (q, s (q, y)) = y ∧ ‖s (q, y)‖ < R := by
…