LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.Deriv.Inverse

`PartialHomeomorph.hasStrictDerivAt_symm` theorem PartialHomeomorph.hasStrictDerivAt_symm : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (f : PartialHomeomorph 𝕜 𝕜) {a f' : 𝕜}, a ∈ f.target → f' ≠ 0 → HasStrictDerivAt (↑f) f' (↑f.symm a) → HasStrictDerivAt (↑f.symm) f'⁻¹ a This theorem states that if `f` is a partial homeomorphism defined on a neighborhood of `f.symm a`, and `f` has a non-zero derivative `f'` at `f.symm a` in the strict sense, then the inverse of `f`, denoted as `f.symm`, has the derivative `f'⁻¹` at `a` in the strict sense. This is a component of the inverse function theorem and presumes that we already have an inverse function. In more mathematical terms, if `f` is a map with a non-zero derivative at a point in its domain, then its inverse function has a derivative at the corresponding point in its target, and the derivative of the inverse function is the reciprocal of the derivative of the function. This is under the assumption that the inverse function exists. More concisely: If `f` is a partial homeomorphism with a non-zero strict derivative at `a`, then the inverse `f.symm` has a strict derivative `f'⁻¹` at `f.symm a`.
`HasDerivAt.of_local_left_inverse` theorem HasDerivAt.of_local_left_inverse : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {f' a : 𝕜}, ContinuousAt g a → HasDerivAt f f' (g a) → f' ≠ 0 → (∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) → HasDerivAt g f'⁻¹ a The theorem `HasDerivAt.of_local_left_inverse` states that if we have two functions `f` and `g` over a nontrivially normed field, and for `y` in some neighborhood of a point `a`, `f (g y) = y`, and `g` is continuous at `a`, and `f` has an invertible derivative `f'` at `g a`, then `g` has the derivative `f'⁻¹` at `a`. This is a component of the inverse function theorem, assuming the existence of an inverse function. More concisely: If `f` and `g` are functions over a nontrivially normed field with `g` continuous at `a`, `f (g y) = y` for `y` near `a`, and `f'` is invertible at `g a`, then `g` has derivative `f'⁻¹` at `a`.
`PartialHomeomorph.hasDerivAt_symm` theorem PartialHomeomorph.hasDerivAt_symm : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (f : PartialHomeomorph 𝕜 𝕜) {a f' : 𝕜}, a ∈ f.target → f' ≠ 0 → HasDerivAt (↑f) f' (↑f.symm a) → HasDerivAt (↑f.symm) f'⁻¹ a The theorem `PartialHomeomorph.hasDerivAt_symm` states that if `f` is a partial homeomorphism defined on a neighborhood of `f.symm a`, and `f` has a non-zero derivative `f'` at `f.symm a`, then the inverse of `f`, denoted by `f.symm`, has the derivative `f'⁻¹` at `a`. This theorem is a component of the inverse function theorem, but it presumes that an inverse function is already given. More concisely: If `f` is a partial homeomorphism with non-zero derivative at `x = f.symm a`, then `f.symm` has the derivative `(f.symm).deriv (f a) = (f'. inverse) (f a)`.
`HasStrictDerivAt.of_local_left_inverse` theorem HasStrictDerivAt.of_local_left_inverse : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {f' a : 𝕜}, ContinuousAt g a → HasStrictDerivAt f f' (g a) → f' ≠ 0 → (∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) → HasStrictDerivAt g f'⁻¹ a The theorem `HasStrictDerivAt.of_local_left_inverse` states that if there exists a function `f` which satisfies the condition `f (g y) = y` for all `y` in some neighborhood of a point `a` and `f` has an invertible derivative `f'` at the point `g a` in the strict sense, and `g` is continuous at point `a`, then `g` has the derivative `f'⁻¹` at `a` in the strict sense. This is a portion of the inverse function theorem that assumes we already have an inverse function. In detail, the theorem assumes a nontrivial normed field `𝕜` and two functions `f` and `g` from `𝕜` to `𝕜`. If `f` has a strict derivative `f'` at `g a`, `g` is continuous at `a`, and `f'` is not equal to zero, and for all `y` in some neighborhood of `a` it holds that `f (g y) = y`, then `g` has a strict derivative `f'⁻¹` at `a`. More concisely: If `f` is a function with a continuous inverse `g`, `f'` is invertible and nonzero at `g a`, and `g` satisfies `f (g y) = y` for all `y` in a neighborhood of `a`, then `g` has a strict derivative `f'⁻¹` at `a`.
`HasStrictDerivAt.hasStrictFDerivAt_equiv` theorem HasStrictDerivAt.hasStrictFDerivAt_equiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜}, HasStrictDerivAt f f' x → ∀ (hf' : f' ≠ 0), HasStrictFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x The theorem `HasStrictDerivAt.hasStrictFDerivAt_equiv` states that given any type `𝕜` that is a nontrivially normed field, for any function `f : 𝕜 → 𝕜`, if `f` has a strict derivative `f'` at a point `x` (in the sense that `f y - f z = (y - z) • f' + o(y - z)` as `y, z → x`), and `f'` is not zero, then `f` has a strict Frechet derivative at `x`. This Frechet derivative is given by the continuous linear equivalence induced by embedding `f'` (which is nonzero) into the group of units of `𝕜`, which is then automatically a multiplicative group with zero removed. More concisely: If `𝕜` is a nontrivially normed field, `f : 𝕜 → 𝕜` has a nonzero strict derivative `f'` at `x ∈ 𝕜`, then `f` has a strict Frechet derivative at `x` given by the continuous linear equivalence induced by `f'` embedded in the multiplicative group of units of `𝕜`.