MathlibAnnex.BilipschitzOrientation.fderiv_lower_bound
theorem
Preserves the same lower constant in the difference-quotient limit.
Statement
Let and let have the sup norm . Let be open, and let be globally Lipschitz maps whose restrictions and are mutually inverse. Fix a number such that
Suppose is differentiable at a point . Let denote its Fréchet derivative there. Then
Assumptions
The map is differentiable at this particular ; the point need not lie in . The sets are open. The inverse and image conditions are The global bounds use specified constants and : The estimates hold on all of , not just on or . The inverse identities are required only on and .
Conclusion
The derivative has the same positive lower constant as the original map. In particular, Thus is injective. The estimate also includes the direction .
Applying the same estimate to proves that forces , as in the derivative-injectivity corollary. Since is a linear endomorphism of the finite-dimensional space , the determinant corollary gives . Similarly, the original lower bound gives global injectivity of by applying it when .
Proof route
Apply the lower bound to and , divide by , and pass to the derivative as .
Proof steps
Write the difference-quotient estimate. Fix . For every real ,
The first line is the global lower bound at these two points. The second follows from and homogeneity of the norm; it does not require .
Take the limit. Differentiability at gives
Consequently,
This is precisely the difference-quotient lemma with linear map , lower constant , the displayed global estimate, and differentiability at . No derivative at any other point is needed.
Main citations
- Exact
declaration and its source —
MathlibAnnex.BilipschitzOrientation.fderiv_lower_bound - Difference
quotients and their derivative limit —
MathlibAnnex.BilipschitzOrientation.fderiv_lower_bound_of_global_lower - The
lower bound forces global injectivity —
MathlibAnnex.BilipschitzOrientation.BiLipschitzOpenData.f_injective - A
positive derivative bound gives injectivity —
MathlibAnnex.BilipschitzOrientation.fderiv_injective - An
injective square derivative has nonzero determinant —
MathlibAnnex.BilipschitzOrientation.det_fderiv_ne_zero
Lean source signature (exact)
theorem fderiv_lower_bound {n : ℕ} (D : BiLipschitzOpenData n)
{x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) (v : Fin n → ℝ) :
D.lower * ‖v‖ ≤ ‖(fderiv ℝ D.f x) v‖| In the source | Mathematical meaning |
|---|---|
(D : BiLipschitzOpenData n) |
The record described in this Card: open
,
maps
restricting to inverse bijections
,
global upper Lipschitz bounds
,
and global lower bound
with
.
The source name D is not the derivative symbol. |
D.source; D.target; D.f; D.g |
The local mathematical objects , respectively, throughout this Card. |
{x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) |
The input point is a differentiability point of . There is no condition . |
| In the source | Mathematical meaning |
|---|---|
(v : Fin n → ℝ) |
The arbitrary vector . |
D.lower * ‖v‖ ≤ ‖(fderiv ℝ D.f x) v‖ |
The output . The derivative of the same keeps its global positive lower constant. |
Exact surrounding binder context (separate excerpts)
Exact source lines 23–29:
noncomputable section
open Set MeasureTheory Filter
open scoped ENNReal NNReal Topology
namespace MathlibAnnex
namespace BilipschitzOrientationRead exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.BilipschitzOrientation.fderiv_lower_bound
Accepted content SHA-256: d13cfea772f82cdc47f7ef8bc5877579187689451484645ae6d6131d5c8d8420
Accepted source guide SHA-256: ceb153037636e289a4e391d81836cd09a8b48fac700bd2a2c1c8c0d9bda9eeb4
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73