English
An open affine map of normed spaces is open: if an affine map f: P → Q is continuous and surjective, then it is an open map.
Русский
Открытое отображение аффинного отображения между нормированными пространствами сохраняется: если f непрерывно и сюръективно, то оно открытое.
LaTeX
$$$$\\text{IsOpenMap}(f)$$$$
Lean4
/-- The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then
any point has a preimage with controlled norm. -/
theorem exists_preimage_norm_le (surj : Surjective f) : ∃ C > 0, ∀ y, ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖ :=
by
obtain ⟨C, C0, hC⟩ := exists_approx_preimage_norm_le f surj
choose g hg using hC
let h y := y - f (g y)
have hle : ∀ y, ‖h y‖ ≤ 1 / 2 * ‖y‖ := by
intro y
rw [← dist_eq_norm, dist_comm]
exact (hg y).1
refine ⟨2 * C + 1, by linarith, fun y => ?_⟩
have hnle : ∀ n : ℕ, ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖ := by
intro n
induction n with
| zero => simp only [one_div, one_mul, iterate_zero_apply, pow_zero, le_rfl]
| succ n IH =>
rw [iterate_succ']
apply le_trans (hle _) _
rw [pow_succ', mul_assoc]
gcongr
let u n := g (h^[n] y)
have ule : ∀ n, ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖) := fun n ↦
by
apply le_trans (hg _).2
calc
C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := mul_le_mul_of_nonneg_left (hnle n) C0
_ = (1 / 2) ^ n * (C * ‖y‖) := by ring
have sNu : Summable fun n => ‖u n‖ :=
by
refine .of_nonneg_of_le (fun n => norm_nonneg _) ule ?_
exact Summable.mul_right _ (summable_geometric_of_lt_one (by simp) (by norm_num))
have su : Summable u := sNu.of_norm
let x := tsum u
have x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖ :=
calc
‖x‖ ≤ ∑' n, ‖u n‖ := norm_tsum_le_tsum_norm sNu
_ ≤ ∑' n, (1 / 2) ^ n * (C * ‖y‖) := (sNu.tsum_le_tsum ule <| Summable.mul_right _ summable_geometric_two)
_ = (∑' n, (1 / 2) ^ n) * (C * ‖y‖) := tsum_mul_right
_ = 2 * C * ‖y‖ := by rw [tsum_geometric_two, mul_assoc]
_ ≤ 2 * C * ‖y‖ + ‖y‖ := (le_add_of_nonneg_right (norm_nonneg y))
_ = (2 * C + 1) * ‖y‖ := by ring
have fsumeq : ∀ n : ℕ, f (∑ i ∈ Finset.range n, u i) = y - h^[n] y :=
by
intro n
induction n with
| zero => simp [f.map_zero]
| succ n IH => rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]
have : Tendsto (fun n => ∑ i ∈ Finset.range n, u i) atTop (𝓝 x) := su.hasSum.tendsto_sum_nat
have L₁ : Tendsto (fun n => f (∑ i ∈ Finset.range n, u i)) atTop (𝓝 (f x)) := (f.continuous.tendsto _).comp this
simp only [fsumeq] at L₁
have L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0)) :=
by
refine tendsto_const_nhds.sub ?_
rw [tendsto_iff_norm_sub_tendsto_zero]
simp only [sub_zero]
refine squeeze_zero (fun _ => norm_nonneg _) hnle ?_
rw [← zero_mul ‖y‖]
refine (_root_.tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds <;> norm_num
have feq : f x = y - 0 := tendsto_nhds_unique L₁ L₂
rw [sub_zero] at feq
exact ⟨x, feq, x_ineq⟩
