ParametricSubmersion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform local images for nearby parameters

Apply the ordinary submersion theorem to the joint map (p,x) ↦ (p,f(p,x)). A surjective derivative in the second variable then gives a common image neighborhood for all nearby parameters. This is the persistence step for normalized generator product schemes.

theorem OAI.PolycyclicRecognition.parameter_joint_derivative_surjective line 30

Source documentation

Surjectivity in the second variable makes the parameter-preserving joint differential surjective.

theorem parameter_joint_derivative_surjective (D : (P × E) →L[ℝ] F)
    (hD : Function.Surjective (fun v : E => D (0, v))) :
    Function.Surjective ((ContinuousLinearMap.fst ℝ P E).prod D) := by
…

theorem OAI.PolycyclicRecognition.exists_uniform_local_image line 45

Source documentation

A fixed source ball covers a common target ball for all parameters in one open neighborhood of the given parameter.

theorem exists_uniform_local_image (f : P × E → F) (p : P)
    (hf : ContDiffAt ℝ 1 f (p, 0)) (hz : f (p, 0) = 0)
    (hsurj : Function.Surjective (fun v : E => fderiv ℝ f (p, 0) (0, v)))
    {R : ℝ} (hR : 0 < R) :
    ∃ U : Set P, IsOpen U ∧ p ∈ U ∧ ∃ ε : ℝ, 0 < ε ∧
      ∀ q ∈ U, ball (0 : F) ε ⊆ (fun x : E => f (q, x)) '' ball 0 R := by
…