Extending a backward bound on a normed group homomorphism from a dense set #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Possible TODO (from the PR's review, https://github.com/leanprover-community/mathlib/pull/8498 ): "This feels a lot like the second step in the proof of the Banach open mapping theorem (exists_preimage_norm_le) ... wonder if it would be possible to refactor it using one of [the lemmas in this file]."

source

theorem controlled_closure_of_complete {G : Type u_1} [normed_add_comm_group G] [complete_space G] {H : Type u_2} [normed_add_comm_group H] {f : normed_add_group_hom G H} {K : add_subgroup H} {C ε : ℝ} (hC : 0 < C) (hε : 0 < ε) (hyp : f.surjective_on_with K C) :

f.surjective_on_with K.topological_closure (C + ε)

Given f : normed_add_group_hom G H for some complete G and a subgroup K of H, if every element x of K has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of K with constant C+ε instead of C, for any positive ε.

source

theorem controlled_closure_range_of_complete {G : Type u_1} [normed_add_comm_group G] [complete_space G] {H : Type u_2} [normed_add_comm_group H] {f : normed_add_group_hom G H} {K : Type u_3} [seminormed_add_comm_group K] {j : normed_add_group_hom K H} (hj : ∀ (x : K), ‖⇑j x‖ = ‖x‖) {C ε : ℝ} (hC : 0 < C) (hε : 0 < ε) (hyp : ∀ (k : K), ∃ (g : G), ⇑f g = ⇑j k ∧ ‖g‖ ≤ C * ‖k‖) :

f.surjective_on_with j.range.topological_closure (C + ε)

Given f : normed_add_group_hom G H for some complete G, if every element x of the image of an isometric immersion j : normed_add_group_hom K H has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of this image with constant C+ε instead of C, for any positive ε. This is useful in particular if j is the inclusion of a normed group into its completion (in this case the closure is the full target group).