Documentation

TauCeti.Analysis.Calculus.ImplicitFunctionTheorem

Smoothness of the complemented-kernel implicit function theorem #

Let f : E โ†’ F be a map between Banach spaces which is strictly differentiable at a with surjective derivative f' whose kernel is complemented. Mathlib's HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented straightens f near a: it is the homeomorphism x โ†ฆ (f x, P (x - a)) onto a neighbourhood of (f a, 0) in F ร— ker f', where P is the continuous projection onto ker f' chosen by the complementation hypothesis, and its inverse restricted to the slice {f a} ร— ker f' is the implicit function of f.

Mathlib records the strict differentiability of that homeomorphism and of its inverse. This file adds the C^n statements, obtained from Mathlib's smooth inverse theorem for an OpenPartialHomeomorph, OpenPartialHomeomorph.contDiffAt_symm, and the value of the inverse homeomorphism at (f a, 0).

Smoothness of the inverse at a point of the target needs the derivative of the coordinate map to be invertible there. At the base point that is the hypothesis of the theorem; away from it, it is supplied by TauCeti.Analysis.Calculus.InverseFunctionTheorem, on the open neighbourhood HasStrictFDerivAt.implicitCoordSource of the base point that the inverse function theorem itself produced. So the implicit function is C^n on a whole neighbourhood of the origin of the slice, not only at the origin: enough to compare two implicit-function charts smoothly, which is what a manifold structure on a level set asks for.

Mathlib's ImplicitFunctionData.contDiffAt_implicitFunction is a C^n implicit function theorem for the same data. It is not usable here: it is stated over [RCLike ๐•œ] and assumes n โ‰  0, whereas the results below hold over an arbitrary [NontriviallyNormedField K] โ€” the generality in which the underlying homeomorphism, and its consumer TauCeti.levelSetChart, are stated โ€” and for every n : โ„•โˆžฯ‰. Consumers that are content with RCLike scalars and n โ‰  0 should prefer Mathlib's lemma.

Main results #

source
noncomputable def ContinuousLinearMap.implicitCoordEquiv {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] (f' : E โ†’L[K] F) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
E โ‰ƒL[K] F ร— โ†ฅ(โ†‘f').ker

The derivative at the base point of the implicit-function coordinate map x โ†ฆ (f x, P (x - a)), as a continuous linear equivalence E โ‰ƒL[K] F ร— ker f': it is x โ†ฆ (f' x, P x), where P is the projection onto ker f' chosen by the complementation hypothesis.

Equations
Instances For
    source
    @[simp]
    theorem ContinuousLinearMap.coe_implicitCoordEquiv {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] (f' : E โ†’L[K] F) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
    โ†‘(f'.implicitCoordEquiv hf' hker) = f'.prod (Classical.choose hker)
    source
    @[simp]
    theorem HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_symm_self {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
    โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm (f a, 0) = a

    The inverse of Mathlib's complemented-kernel implicit-function homeomorphism sends the image (f a, 0) of the base point back to the base point.

    source
    theorem HasStrictFDerivAt.contDiffAt_implicitToOpenPartialHomeomorphOfComplemented {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} {n : WithTop โ„•โˆž} {x : E} (hf : HasStrictFDerivAt f f' a) (hcont : ContDiffAt K n f x) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
    ContDiffAt K n (โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker)) x

    Mathlib's complemented-kernel implicit-function homeomorphism is as smooth as the original map at every point where the original map is smooth.

    source
    theorem HasStrictFDerivAt.hasStrictFDerivAt_implicitCoord {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
    HasStrictFDerivAt (fun (x : E) => (f x, (Classical.choose hker) (x - a))) (โ†‘(f'.implicitCoordEquiv hf' hker)) a

    The implicit-function coordinate map x โ†ฆ (f x, P (x - a)) is strictly differentiable at the base point, with derivative the equivalence ContinuousLinearMap.implicitCoordEquiv.

    source
    theorem HasStrictFDerivAt.contDiffAt_implicitToOpenPartialHomeomorphOfComplemented_symm_of_isInvertible {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} {n : WithTop โ„•โˆž} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) {y : F ร— โ†ฅ(โ†‘f').ker} (hy : y โˆˆ (implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).target) {A : E โ†’L[K] F} (hA : HasFDerivAt f A (โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm y)) (hAinv : (A.prod (Classical.choose hker)).IsInvertible) (hcont : ContDiffAt K n f (โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm y)) :
    ContDiffAt K n (โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm) y

    The inverse of the implicit-function homeomorphism is C^n wherever the coordinate map has invertible derivative. Mathlib's OpenPartialHomeomorph.contDiffAt_symm asks for an invertible derivative at the point one inverts around; A below is the derivative of the equation there, and (A, P) is the derivative of the coordinate map.

    source
    theorem HasStrictFDerivAt.contDiffAt_implicitToOpenPartialHomeomorphOfComplemented_symm {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} {n : WithTop โ„•โˆž} (hf : HasStrictFDerivAt f f' a) (hcont : ContDiffAt K n f a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
    ContDiffAt K n โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm (f a, 0)

    The inverse of Mathlib's complemented-kernel implicit-function homeomorphism is as smooth as the original map at the image of the base point.

    The neighbourhood on which the coordinate map stays invertible #

    source
    noncomputable def HasStrictFDerivAt.implicitCoordSource {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
    Set E

    An open neighbourhood of the base point on which the derivative of the implicit-function coordinate map x โ†ฆ (f x, P (x - a)) is still invertible: the source of the homeomorphism that the inverse function theorem builds from that map. Like Mathlib's implicit-function homeomorphism itself, it is a choice, and is described only through the lemmas below.

    Equations
    Instances For
      source
      theorem HasStrictFDerivAt.isOpen_implicitCoordSource {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
      IsOpen (hf.implicitCoordSource hf' hker)
      source
      theorem HasStrictFDerivAt.mem_implicitCoordSource {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
      a โˆˆ hf.implicitCoordSource hf' hker
      source
      theorem HasStrictFDerivAt.isInvertible_prod_of_mem_implicitCoordSource {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) {x : E} (hx : x โˆˆ hf.implicitCoordSource hf' hker) {A : E โ†’L[K] F} (hA : HasFDerivAt f A x) :
      (A.prod (Classical.choose hker)).IsInvertible

      The derivative of the coordinate map stays invertible on HasStrictFDerivAt.implicitCoordSource. If f has derivative A at a point of that neighbourhood, then (A, P) is a continuous linear equivalence, exactly as (f', P) is at the base point.

      source
      theorem HasStrictFDerivAt.surjective_of_mem_implicitCoordSource {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) {x : E} (hx : x โˆˆ hf.implicitCoordSource hf' hker) {A : E โ†’L[K] F} (hA : HasFDerivAt f A x) :
      Function.Surjective โ‡‘A

      The derivative of the equation stays surjective on HasStrictFDerivAt.implicitCoordSource. The pair (A, P) is invertible there, and a pair is invertible only if its first component is onto.

      Surjectivity of the derivative is the hypothesis under which the level set of f is locally a manifold, so this says that a regular point of a level set has a whole neighbourhood of regular points, with no continuity argument on x โ†ฆ fderiv f x.

      source
      theorem HasStrictFDerivAt.contDiffAt_implicitToOpenPartialHomeomorphOfComplemented_symm_of_mem {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} {n : WithTop โ„•โˆž} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) {y : F ร— โ†ฅ(โ†‘f').ker} (hy : y โˆˆ (implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).target) (hmem : โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm y โˆˆ hf.implicitCoordSource hf' hker) {A : E โ†’L[K] F} (hA : HasFDerivAt f A (โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm y)) (hcont : ContDiffAt K n f (โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm y)) :
      ContDiffAt K n (โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm) y

      The implicit function is C^n on a whole neighbourhood of the origin of the slice. The inverse of the implicit-function homeomorphism is C^n at every point of its target whose preimage lies in HasStrictFDerivAt.implicitCoordSource.

      source
      theorem HasStrictFDerivAt.eventually_implicitFunctionOfComplemented_eq {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) :
      โˆ€แถ  (k : โ†ฅ(โ†‘f').ker) in nhds 0, implicitFunctionOfComplemented f f' hf hf' hker (f a) k = โ†‘(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).symm (f a, k)

      Near 0, the implicit function of f at the value f a agrees on the slice {f a} ร— ker f' with the inverse of the complemented-kernel implicit-function homeomorphism.

      source
      theorem HasStrictFDerivAt.exists_isSliceChart_preimage_zero {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[K] F} {a : E} {n : WithTop โ„•โˆž} (hn : n โ‰  0) (hf : HasStrictFDerivAt f f' a) (hf' : (โ†‘f').range = โŠค) (hker : (โ†‘f').ker.ClosedComplemented) {U : Set E} (hU : IsOpen U) (haU : a โˆˆ U) (hC : โˆ€ z โˆˆ U, ContDiffAt K n f z) :
      โˆƒ (e : OpenPartialHomeomorph E E), a โˆˆ e.source โˆง e.source โŠ† U โˆง (โˆ€ z โˆˆ e.source, ContDiffAt K n (โ†‘e) z) โˆง (โˆ€ z โˆˆ e.target, ContDiffAt K n (โ†‘e.symm) z) โˆง TauCeti.IsSliceChart e (โ†‘(โ†‘f').ker) (f โปยน' {0})

      A regular zero set is flattened by an ambient chart. If f is C^n (n โ‰  0) on an open set U around a, with surjective strict derivative f' at a whose kernel is complemented, then a C^n chart of E with C^n inverse, defined around a with source inside U, flattens the zero set of f onto ker f'.