Lean4
/-- First step of the proof of the Banach open mapping theorem (using completeness of `F`):
by Baire's theorem, there exists a ball in `E` whose image closure has nonempty interior.
Rescaling everything, it follows that any `y ∈ F` is arbitrarily well approached by
images of elements of norm at most `C * ‖y‖`.
For further use, we will only need such an element whose image
is within distance `‖y‖/2` of `y`, to apply an iterative process. -/
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
simp only [mem_interior_iff_mem_nhds, Metric.mem_nhds_iff] at this
rcases this with ⟨n, a, ε, ⟨εpos, H⟩⟩
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
refine ⟨(ε / 2)⁻¹ * ‖c‖ * 2 * n, by positivity, fun y => ?_⟩
rcases eq_or_ne y 0 with rfl | hy
· simp
· have hc' : 1 < ‖σ c‖ := by simp only [RingHomIsometric.norm_map, hc]
rcases rescale_to_shell hc' (half_pos εpos) hy with ⟨d, hd, ydlt, -, dinv⟩
let δ := ‖d‖ * ‖y‖ / 4
have δpos : 0 < δ := by positivity
have : a + d • y ∈ ball a ε := by simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self εpos)]
rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₁, z₁im, h₁⟩
rcases (mem_image _ _ _).1 z₁im with ⟨x₁, hx₁, xz₁⟩
rw [← xz₁] at h₁
rw [mem_ball, dist_eq_norm, sub_zero] at hx₁
have : a ∈ ball a ε := by
simp only [mem_ball, dist_self]
exact εpos
rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₂, z₂im, h₂⟩
rcases (mem_image _ _ _).1 z₂im with ⟨x₂, hx₂, xz₂⟩
rw [← xz₂] at h₂
rw [mem_ball, dist_eq_norm, sub_zero] at hx₂
let x := x₁ - x₂
have I : ‖f x - d • y‖ ≤ 2 * δ :=
calc
‖f x - d • y‖ = ‖f x₁ - (a + d • y) - (f x₂ - a)‖ :=
by
congr 1
simp only [x, f.map_sub]
abel
_ ≤ ‖f x₁ - (a + d • y)‖ + ‖f x₂ - a‖ := (norm_sub_le _ _)
_ ≤ 2 * δ := by grind [dist_eq_norm']
have J : ‖f (σ' d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖ :=
calc
‖f (σ' d⁻¹ • x) - y‖ = ‖d⁻¹ • f x - (d⁻¹ * d) • y‖ := by
rwa [f.map_smulₛₗ _, inv_mul_cancel₀, one_smul, map_inv₀, map_inv₀, RingHomCompTriple.comp_apply,
RingHom.id_apply]
_ = ‖d⁻¹ • (f x - d • y)‖ := by rw [mul_smul, smul_sub]
_ = ‖d‖⁻¹ * ‖f x - d • y‖ := by rw [norm_smul, norm_inv]
_ ≤ ‖d‖⁻¹ * (2 * δ) := by gcongr
_ = 1 / 2 * ‖y‖ := by simpa [δ, field] using by norm_num
rw [← dist_eq_norm] at J
have K : ‖σ' d⁻¹ • x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖ :=
calc
‖σ' d⁻¹ • x‖ = ‖d‖⁻¹ * ‖x₁ - x₂‖ := by rw [norm_smul, RingHomIsometric.norm_map, norm_inv]
_ ≤ (ε / 2)⁻¹ * ‖c‖ * ‖y‖ * (n + n) := by
gcongr
· simpa using dinv
· exact le_trans (norm_sub_le _ _) (by gcongr)
_ = (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖ := by ring
exact ⟨σ' d⁻¹ • x, J, K⟩
