mathlib3 documentation

analysis.normed.group.controlled_closure

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]."

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) :

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 ε.

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) :

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).