Documentation

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Non-linear maps close to affine maps #

In this file we study a map f such that ‖f x - f y - f' (x - y)‖ ≤ c * ‖x - y‖ on an open set s, where f' : E →L[𝕜] F is a continuous linear map and c is suitably small. Maps of this type behave like f a + f' (x - a) near each a ∈ s.

When f' is onto, we show that f is locally onto.

When f' is a continuous linear equiv, we show that f is a homeomorphism between s and f '' s. More precisely, we define ApproximatesLinearOn.toPartialHomeomorph to be a PartialHomeomorph with toFun = f, source = s, and target = f '' s. between s and f '' s. More precisely, we define ApproximatesLinearOn.toPartialHomeomorph to be a PartialHomeomorph with toFun = f, source = s, and target = f '' s.

Maps of this type naturally appear in the proof of the inverse function theorem (see next section), and ApproximatesLinearOn.toPartialHomeomorph will imply that the locally inverse function and ApproximatesLinearOn.toPartialHomeomorph will imply that the locally inverse function exists.

We define this auxiliary notion to split the proof of the inverse function theorem into small lemmas. This approach makes it possible

Notations #

We introduce some local notation to make formulas shorter:

def ApproximatesLinearOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (f' : E →L[𝕜] F) (s : Set E) (c : NNReal) :

We say that f approximates a continuous linear map f' on s with constant c, if ‖f x - f y - f' (x - y)‖ ≤ c * ‖x - y‖ whenever x, y ∈ s.

This predicate is defined to facilitate the splitting of the inverse function theorem into small lemmas. Some of these lemmas can be useful, e.g., to prove that the inverse function is defined on a specific set.

Equations
Instances For
    @[simp]
    theorem approximatesLinearOn_empty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) (f' : E →L[𝕜] F) (c : NNReal) :

    First we prove some properties of a function that ApproximatesLinearOn a (not necessarily invertible) continuous linear map.

    theorem ApproximatesLinearOn.mono_num {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} {c' : NNReal} (hc : c c') (hf : ApproximatesLinearOn f f' s c) :
    theorem ApproximatesLinearOn.mono_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {t : Set E} {c : NNReal} (hst : s t) (hf : ApproximatesLinearOn f f' t c) :
    theorem ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} :
    ApproximatesLinearOn f f' s c LipschitzOnWith c (f - f') s
    theorem LipschitzOnWith.approximatesLinearOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} :
    LipschitzOnWith c (f - f') sApproximatesLinearOn f f' s c

    Alias of the reverse direction of ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith.

    theorem ApproximatesLinearOn.lipschitzOnWith {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} :
    ApproximatesLinearOn f f' s cLipschitzOnWith c (f - f') s

    Alias of the forward direction of ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith.

    theorem ApproximatesLinearOn.lipschitz_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
    LipschitzWith c fun (x : s) => f x - f' x
    theorem ApproximatesLinearOn.lipschitz {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
    LipschitzWith (f'‖₊ + c) (s.restrict f)
    theorem ApproximatesLinearOn.continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
    Continuous (s.restrict f)
    theorem ApproximatesLinearOn.continuousOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :

    We prove that a function which is linearly approximated by a continuous linear map with a nonlinear right inverse is locally onto. This will apply to the case where the approximating map is a linear equivalence, for the local inverse theorem, but also whenever the approximating map is onto, by Banach's open mapping theorem.

    theorem ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {ε : } {b : E} (ε0 : 0 ε) (hε : Metric.closedBall b ε s) :
    Set.SurjOn f (Metric.closedBall b ε) (Metric.closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - c) * ε))

    If a function is linearly approximated by a continuous linear map with a (possibly nonlinear) right inverse, then it is locally onto: a ball of an explicit radius is included in the image of the map.

    theorem ApproximatesLinearOn.open_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) (hs : IsOpen s) (hc : Subsingleton F c < f'symm.nnnorm⁻¹) :
    IsOpen (f '' s)
    theorem ApproximatesLinearOn.image_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {x : E} (hs : s nhds x) (hc : Subsingleton F c < f'symm.nnnorm⁻¹) :
    f '' s nhds (f x)
    theorem ApproximatesLinearOn.map_nhds_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {x : E} (hs : s nhds x) (hc : Subsingleton F c < f'symm.nnnorm⁻¹) :
    Filter.map f (nhds x) = nhds (f x)

    From now on we assume that f approximates an invertible continuous linear map f : E ≃L[𝕜] F.

    We also assume that either E = {0}, or c < ‖f'⁻¹‖⁻¹. We use N as an abbreviation for ‖f'⁻¹‖.

    theorem ApproximatesLinearOn.antilipschitz {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :
    AntilipschitzWith (f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)
    theorem ApproximatesLinearOn.injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :
    Function.Injective (s.restrict f)
    theorem ApproximatesLinearOn.injOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :
    theorem ApproximatesLinearOn.surjective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E ≃L[𝕜] F} {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') Set.univ c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :
    def ApproximatesLinearOn.toPartialEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :

    A map approximating a linear equivalence on a set defines a partial equivalence on this set. Should not be used outside of this file, because it is superseded by toPartialHomeomorph below.

    This is a first step towards the inverse function.

    Equations
    Instances For
      theorem ApproximatesLinearOn.inverse_continuousOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :
      ContinuousOn (↑(hf.toPartialEquiv hc).symm) (f '' s)

      The inverse function is continuous on f '' s. Use properties of PartialHomeomorph instead.

      theorem ApproximatesLinearOn.to_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :
      ApproximatesLinearOn (↑(hf.toPartialEquiv hc).symm) (↑f'.symm) (f '' s) (f'.symm‖₊ * (f'.symm‖₊⁻¹ - c)⁻¹ * c)

      The inverse function is approximated linearly on f '' s by f'.symm.

      def ApproximatesLinearOn.toPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) (hs : IsOpen s) :

      Given a function f that approximates a linear equivalence on an open set s, returns a partial homeomorphism with toFun = f and source = s.

      Equations
      Instances For
        @[simp]
        theorem ApproximatesLinearOn.toPartialHomeomorph_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) (hs : IsOpen s) :
        @[simp]
        theorem ApproximatesLinearOn.toPartialHomeomorph_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) (hs : IsOpen s) :
        @[simp]
        theorem ApproximatesLinearOn.toPartialHomeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) (hs : IsOpen s) :
        def ApproximatesLinearOn.toHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : EF) {f' : E ≃L[𝕜] F} {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') Set.univ c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) :
        E ≃ₜ F

        A function f that approximates a linear equivalence on the whole space is a homeomorphism.

        Equations
        Instances For
          theorem ApproximatesLinearOn.closedBall_subset_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ε : } {f : EF} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E c < f'.symm‖₊⁻¹) (hs : IsOpen s) {b : E} (ε0 : 0 ε) (hε : Metric.closedBall b ε s) :
          Metric.closedBall (f b) ((f'.symm‖₊⁻¹ - c) * ε) (ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs).target