controlled_closure_of_complete
theorem controlled_closure_of_complete :
∀ {G : Type u_1} [inst : NormedAddCommGroup G] [inst_1 : CompleteSpace G] {H : Type u_2}
[inst_2 : NormedAddCommGroup H] {f : NormedAddGroupHom G H} {K : AddSubgroup H} {C ε : ℝ},
0 < C → 0 < ε → f.SurjectiveOnWith K C → f.SurjectiveOnWith K.topologicalClosure (C + ε)
This theorem states that given a normed additive group homomorphism `f` from a complete normed additive commutative group `G` to a normed additive commutative group `H`, and a subgroup `K` of `H`, if each element `x` in `K` has a preimage under `f` such that the norm of the preimage is at most `C*‖x‖` for some positive real number `C`, then the same property holds for every element in the topological closure of `K`, with a slight increase in the constant to `C+ε` for any positive `ε`. In other words, the control we have over the norm of the preimage extends to the limit points of `K` in the topological space.
More concisely: Given a normed additive group homomorphism from a complete normed additive commutative group to another such group, if every element in a subgroup has a preimage with norm at most C times its image norm, then every element in the subgroup's topological closure has a preimage with norm at most C+ε times its image norm for any ε > 0.
|
controlled_closure_range_of_complete
theorem controlled_closure_range_of_complete :
∀ {G : Type u_1} [inst : NormedAddCommGroup G] [inst_1 : CompleteSpace G] {H : Type u_2}
[inst_2 : NormedAddCommGroup H] {f : NormedAddGroupHom G H} {K : Type u_3} [inst_3 : SeminormedAddCommGroup K]
{j : NormedAddGroupHom K H},
(∀ (x : K), ‖j x‖ = ‖x‖) →
∀ {C ε : ℝ},
0 < C →
0 < ε →
(∀ (k : K), ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖) → f.SurjectiveOnWith j.range.topologicalClosure (C + ε)
The theorem `controlled_closure_range_of_complete` states that for any complete normed additive commutative group `G` and normed additive commutative group `H`, if there is a norm-preserving function `j` from another seminormed additive commutative group `K` to `H` and a function `f` from `G` to `H` such that for every element in `K`, there exists a preimage under `f` with a norm smaller or equal to `C` times the norm of the element, then the same property holds for all elements in the topological closure of the image of `j` with a slightly larger constant `C + ε`, where both `C` and `ε` are positive real numbers. This theorem is particularly useful when `j` is the inclusion of a normed group into its completion, in which case the closure is the full target group.
More concisely: For any complete normed additive commutative groups `G` and `H`, if there's a norm-preserving function `j: K -> H` from a seminormed additive commutative group `K`, and a function `f: G -> H` such that for every `x in K`, there exists `y in G` with `f(y) = x` and `||y|| <= C ||x||`, then every element in the closure of `j(K)` has a preimage `z in G` with `f(z)` and `||z|| <= C + ε ||z_0||`, for some `z_0 in j(K)` and `ε > 0`.
|