ApproximatesLinearOn.inverse_continuousOn
theorem ApproximatesLinearOn.inverse_continuousOn :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{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)
This theorem states that for a given function `f` from a normed additive commutative group `E` to another normed additive commutative group `F`, both over a nontrivially normed field `𝕜`, if `f` approximates a linear map `f'` on a set `s` of `E` and a nonnegative real number `c` such that either `E` has only one element or `c` is less than the reciprocal of the operator norm of the inverse of `f'`, then the inverse of the partial equivalence given by the approximation of `f` on `s` is continuous on the image of `s` under `f`.
More concisely: If `f: E -> F` is a function from a normed additive commutative group `E` to another normed additive commutative group `F` over a nontrivially normed field, `s` is a set, `f'` is a linear map, and `c` is a non-negative real number such that either `E` has only one element or `c < 1 / ||f'⁻¹||`, then the inverse of the partial equivalence induced by `f`'s approximation of `f'` on `s` is continuous on the image of `s` under `f`.
|
ApproximatesLinearOn.to_inv
theorem ApproximatesLinearOn.to_inv :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{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)
This theorem states that for a given field `𝕜` with a norm, two normed additive commutative group spaces `E` and `F` over `𝕜`, a function `f` from `E` to `F`, a continuous linear equivalence `f'` between `E` and `F`, a set `s` of elements from `E`, and a non-negative real number `c`, if `f` approximates a linear function on `s` with a rate of convergence `c`, and if `E` has only one element or `c` is less than the inverse of the norm of `f'.symm`, then the inverse of the function corresponding to the partial equivalence relation induced by `f` also approximates a linear function on the image of `s` under `f` with a rate of convergence equal to the product of the norm of `f'.symm`, the inverse of difference between the inverse of the norm of `f'.symm` and `c`, and `c`.
More concisely: Given a field `𝕜` with a norm, a continuous linear equivalence `f'` between normed additive commutative groups `E` and `F` over `𝕜`, a function `f: E → F`, a set `s ⊆ E`, and a real number `c > 0`, if `f` approximates a linear function on `s` with rate `c` and either `|E| = 1` or `c < 1 / ||f'.symm||`, then the inverse of the function induced by `f` approximately linearizes `f(s)` with rate `||f'.symm|| * (1 / ||f'.symm|| - c) * c`.
|
ApproximatesLinearOn.mono_set
theorem ApproximatesLinearOn.mono_set :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{f' : E →L[𝕜] F} {s t : Set E} {c : NNReal},
s ⊆ t → ApproximatesLinearOn f f' t c → ApproximatesLinearOn f f' s c
The theorem `ApproximatesLinearOn.mono_set` states that for any nontrivially normed field `𝕜`, normed additive commutative groups `E` and `F`, and normed spaces over `𝕜` of `E` and `F`, given the function `f : E → F`, the continuous linear map `f' : E →L[𝕜] F`, and two sets `s` and `t` of type `E`, along with the non-negative real number `c`, if set `s` is a subset of set `t` and function `f` approximates a linear function on set `t` with an error of at most `c`, then `f` also approximates a linear function on set `s` with the same error margin `c`. This theorem is a demonstration of the principle of restriction, asserting that if a property holds on a larger set, it also holds on any of its subsets.
More concisely: Given a nontrivially normed field `𝕜`, normed additive commutative groups `E` and `F`, and normed spaces over `𝕜` of `E` and `F`, if `f : E → F` is a continuous linear map, `s ⊆ t ∈ E`, and `f` approximates a linear function on `t` with error `c`, then `f` approximates a linear function on `s` with the same error `c`.
|
LipschitzOnWith.approximatesLinearOn
theorem LipschitzOnWith.approximatesLinearOn :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, LipschitzOnWith c (f - ⇑f') s → ApproximatesLinearOn f f' s c
This theorem, referred to as an alias of the reverse direction of `ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith`, states that for any nontrivially normed field `𝕜`, normed add-commutative group `E` with a normed space structure over `𝕜`, another normed add-commutative group `F` with a normed space structure over `𝕜`, a function `f` from `E` to `F`, a continuous linear map `f'` from `E` to `F`, a set `s` of elements in `E`, and a nonnegative real number `c`, if the function `f - f'` is Lipschitz continuous with constant `c` on set `s` (i.e., for all `x, y` in `s`, the extended distance between `f(x)` and `f(y)` is less than or equal to `c` times the extended distance between `x` and `y`), then `f` approximately linearly maps onto `f'` on set `s` with an approximation factor of `c`.
More concisely: If a continuous linear map and a function between two normed spaces are Lipschitz equivalent on a set with a constant c, then the function approximates the linear map with an error less than or equal to c times the distance between inputs.
|
ApproximatesLinearOn.lipschitzOnWith
theorem ApproximatesLinearOn.lipschitzOnWith :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, ApproximatesLinearOn f f' s c → LipschitzOnWith c (f - ⇑f') s
The theorem `ApproximatesLinearOn.lipschitzOnWith` states that for any nontrivially normed field `𝕜` and two normed spaces `E` and `F`, if a function `f` from `E` to `F` approximates a linear map `f'` on a set `s` with an approximation constant `c`, then the function `f - ⇑f'` is Lipschitz continuous with constant `c` on the set `s`. In other words, the distance between `f(x) - f'(x)` and `f(y) - f'(y)` is less than or equal to `c` times the distance between `x` and `y` for all `x, y` in `s`. This is an alias of the forward direction of the theorem `ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith`.
More concisely: If a function `f` from a normed space `E` to another normed space `F` over a nontrivially normed field approximates a linear map `f'` on a set `s` with an approximation constant `c`, then `f - f'` is Lipschitz continuous on `s` with constant `c`.
|
ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse
theorem ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
[inst_5 : CompleteSpace E] {f : E → F} {s : Set E} {c : NNReal} {f' : E →L[𝕜] F},
ApproximatesLinearOn f f' s c →
∀ (f'symm : f'.NonlinearRightInverse) {ε : ℝ} {b : E},
0 ≤ ε →
Metric.closedBall b ε ⊆ s →
Set.SurjOn f (Metric.closedBall b ε) (Metric.closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε))
The theorem `ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse` states that given a nontrivially normed field `𝕜`, types `E` and `F` that are both normed additive commutative groups and normed spaces over `𝕜`, and `E` is a complete space, if a function `f` from `E` to `F` approximates a continuous linear map `f'` on a set `s` with a nonnegative real number `c` as a factor of approximation, and `f'` has a nonlinear right inverse, then for any nonnegative real number `ε` and any point `b` in `E`, if a closed ball of radius `ε` centered at `b` is contained in `s`, `f` is surjective on this closed ball, in the sense that the image of this ball under `f` contains a closed ball in `F` of a certain radius centered at `f(b)`. The radius of the latter ball is given by the formula `((↑f'symm.nnnorm)⁻¹ - ↑c) * ε`.
More concisely: Given a nontrivially normed field `𝕜`, normed additive commutative groups and normed spaces `E` and `F` over `𝕜`, a complete `E`, a function `f` from `E` to `F` approximating a continuous linear map `f'` on set `s` with a nonnegative factor of approximation `c`, and `f'` having a nonlinear right inverse, if a closed ball of radius `ε` in `E` centered at `b` is contained in `s`, then `f` surjectively maps this ball in `E` to a closed ball in `F` of radius `((||f'||⁻¹ - c) * ε)` centered at `f(b)`.
|