refactor `ContinuousLinearMap.isOpenMap`

Stream: mathlib4

[Yi.Yuan]

I encountered difficulties in proving [Rudin, Functional Analysis (Theorem 4.3 (b) ⇒ (c))][rudin1991].
I need the following version of the Open Mapping Theorem

protected theorem isOpenMap' (h : ∃ (n : ℕ) (x : _), x ∈ interior (closure (f '' ball 0 n))) :
    IsOpenMap f := by

However, the Open Mapping Theorem in mathlib is stated as:

protected theorem isOpenMap (surj : Surjective f) : IsOpenMap f := by

My version can be easily proved by replacing

theorem exists_approx_preimage_norm_le (surj : Surjective f) :
    ∃ C ≥ 0, ∀ y, ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖ := by
  have A : ⋃ n : ℕ, closure (f '' ball 0 n) = Set.univ := by
    refine Subset.antisymm (subset_univ _) fun y _ => ?_
    rcases surj y with ⟨x, hx⟩
    rcases exists_nat_gt ‖x‖ with ⟨n, hn⟩
    refine mem_iUnion.2 ⟨n, subset_closure ?_⟩
    refine (mem_image _ _ _).2 ⟨x, ⟨?_, hx⟩⟩
    rwa [mem_ball, dist_eq_norm, sub_zero]
  have : ∃ (n : ℕ) (x : _), x ∈ interior (closure (f '' ball 0 n)) :=
    nonempty_interior_of_iUnion_of_closed (fun n => isClosed_closure) A

with

theorem exists_approx_preimage_norm_le'
    (h : ∃ (n : ℕ) (x : _), x ∈ interior (closure (f '' ball 0 n))) :
    ∃ C ≥ 0, ∀ y, ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖ := by

and keeping everything else unchanged.

[Yi.Yuan]

4.13 Theorem Let $U$ and $V$ be the open unit balls in the Banach spaces $X$ and $Y$, respectively. If $T \in \mathscr{B}(X, Y)$ and $\delta>0$, then the implications

$$
(a) \rightarrow(b) \rightarrow(c) \rightarrow(d)
$$

hold among the following statements:
(a) $\left\|T^* y^*\right\| \geq \delta\left\|y^*\right\|$ for every $y^* \in Y^*$.
(b) $\overline{T(U)} \supset \delta V$.
(c) $T(U) \supset \delta V$.
(d) $T(X)=Y$.

Moreover, if (d) holds, then (a) holds for some $\delta>0$.
proof. Assume (a), and pick $y_0 \notin \overline{T(U)}$. Since $\overline{T(U)}$ is convex, closed, and balanced, Theorem 3.7 shows that there is a $y^*$ such that $\left|\left\langle y, y^*\right\rangle\right| \leq 1$ for every $y \in \overline{T(U)}$, but $\left|\left\langle y_0, y^*\right\rangle\right|>1$. If $x \in U$, it follows that

$$
\left|\left\langle x, T^* y^*\right\rangle\right|=\left|\left\langle T x, y^*\right\rangle\right| \leq 1
$$


Thus $\left\|T^* y^*\right\| \leq 1$, and now (a) gives

$$
\delta<\delta\left|\left\langle y_0, y^*\right\rangle\right| \leq \delta\left\|y_0\right\|\left\|y^*\right\| \leq\left\|y_0\right\|\left\|T^* y^*\right\| \leq\left\|y_0\right\| .
$$


It follows that $y \in \overline{T(U)}$ if $\|y\| \leq \delta$. Thus $(a) \rightarrow(b)$.
Next, assume (b). Take $\delta=1$, without loss of generality. Then $\overline{T(U)} \supset \bar{V}$. To every $y \in Y$ and every $\varepsilon>0$ corresponds therefore an $x \in X$ with $\|x\| \leq\|y\|$ and $\|y-T x\|<\varepsilon$.

Pick $y_1 \in V$. Pick $\varepsilon_n>0$ so that

$$
\sum_{n=1}^{\infty} \varepsilon_n<1-\left\|y_1\right\| .
$$


Assume $n \geq 1$ and $y_n$ is picked. There exists $x_n$ such that $\left\|x_n\right\| \leq\left\|y_n\right\|$ and $\left\|y_n-T x_n\right\|<\varepsilon_n$. Put

$$
y_{n+1}=y_n-T x_n .
$$


By induction, this process defines two sequences $\left\{x_n\right\}$ and $\left\{y_n\right\}$. Note that

$$
\left\|x_{n+1}\right\| \leq\left\|y_{n+1}\right\|=\left\|y_n-T x_n\right\|<\varepsilon_n .
$$

Hence

$$
\sum_{n=1}^{\infty}\left\|x_n\right\| \leq\left\|x_1\right\|+\sum_{n=1}^{\infty} \varepsilon_n \leq\left\|y_1\right\|+\sum_{n=1}^{\infty} \varepsilon_n<1 .
$$


It follows that $x=\sum x_n$ is in $U$ (see Exercise 23) and that

$$
T x=\lim _{N \rightarrow \infty} \sum_{n=1}^N T x_n=\lim _{N \rightarrow \infty} \sum_{n=1}^N\left(y_n-y_{n+1}\right)=y_1
$$

since $y_{N+1} \rightarrow 0$ as $N \rightarrow \infty$. Thus $y_1=T x \in T(U)$, which proves (c).
Note that the preceding argument is just a specialized version of part of the proof of the open mapping theorem 2.11.

That (c) implies (d) is obvious.
Assume (d). By the open mapping theorem, there is a $\delta>0$ such that $T(U) \supset \delta V$. Hence

$$
\begin{aligned}
\left\|T^* y^*\right\| & =\sup \left\{\left|\left\langle x, T^* y^*\right\rangle\right|: x \in U\right\} \\
& =\sup \left\{\left|\left\langle T x, y^*\right\rangle\right|: x \in U\right\} \\
& \geq \sup \left\{\left|\left\langle y, y^*\right\rangle\right|: y \in \delta V\right\}=\delta\left\|y^*\right\|
\end{aligned}
$$

for every $y^* \in Y^*$. This is (a).

[David Loeffler]

Please don't cut-and-paste big chunks of LaTeX source formatted as code, it's not very readable. I am no expert here, but the existing version of isOpenMap seems like the "standard" one and we definitely shouldn't remove it; but it certainly does no harm to add additional related statements alongside it.

Is it easy to deduce the existing statement isOpenMap from your isOpenMap'?

[Yi.Yuan]

David Loeffler said:

Please don't cut-and-paste big chunks of LaTeX source formatted as code, it's not very readable. I am no expert here, but the existing version of isOpenMap seems like the "standard" one and we definitely shouldn't remove it; but it certainly does no harm to add additional related statements alongside it.

Is it easy to deduce the existing statement isOpenMap from your isOpenMap'?

Thanks for the reminder. It seems like there is no LaTeX editor on Zulip.

[Yi.Yuan]

This issue is addressed in PR #29776. Could anyone please review it?

[Kenny Lau]

that looks good, but i haven't really interacted with analysis

[Violeta Hernández]

There is LaTeX support in Zulip: $\LaTeX$

[Violeta Hernández]

you have to use double $$ signs though