Skip to content

Commit

Permalink
chore(analyis/normed_space/banach): split proof to avoid timeout (#2053)
Browse files Browse the repository at this point in the history 
* chore(analyis/normed_space/banach): split proof to avoid timeout

* delay introducing unnecessary variable

* Apply suggestions from code review

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* fix indent

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
  • Loading branch information
@semorrison @sgouezel @mergify
3 people committed Feb 25, 2020
1 parent 089d058 commit 06c5594
Showing 1 changed file with 83 additions and 72 deletions.
155 changes: 83 additions & 72 deletions src/analysis/normed_space/banach.lean
View file
Expand Up @@ -15,25 +15,27 @@ open function metric set filter finset
open_locale classical topological_space

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [complete_space E] [normed_space 𝕜 E]
{F : Type*} [normed_group F] [complete_space F] [normed_space 𝕜 F]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{F : Type*} [normed_group F] [normed_space 𝕜 F]
{f : E → F}
include 𝕜

set_option class.instance_max_depth 70

/-- 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 (hf : is_bounded_linear_map 𝕜 f) (surj : surjective f) :
∃C, 0 < C ∧ ∀y, ∃x, f x = y ∧ ∥x∥ ≤ C * ∥y∥ :=
variable [complete_space F]

/--
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. -/
lemma exists_approx_preimage_norm_le (hf : is_bounded_linear_map 𝕜 f) (surj : surjective f) :
∃C, 0 ≤ C ∧ ∀y, ∃x, dist (f x) y ≤ 1/2 * ∥y∥ ∧ ∥x∥ ≤ C * ∥y∥ :=
begin
have lin := hf.to_is_linear_map,
haveI : nonempty F := ⟨0⟩,
/- First step of the proof (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. -/
have A : (⋃n:ℕ, closure (f '' (ball 0 n))) = univ,
{ refine subset.antisymm (subset_univ _) (λy hy, _),
rcases surj y with ⟨x, hx⟩,
Expand All @@ -43,67 +45,76 @@ begin
rwa [mem_ball, dist_eq_norm, sub_zero] },
have : ∃(n:ℕ) y ε, 0 < ε ∧ ball y ε ⊆ closure (f '' (ball 0 n)) :=
nonempty_interior_of_Union_of_closed (λn, is_closed_closure) A,
have : ∃C, 0 ≤ C ∧ ∀y, ∃x, dist (f x) y ≤ (1/2) * ∥y∥ ∧ ∥x∥ ≤ C * ∥y∥,
{ rcases this with ⟨n, a, ε, ⟨εpos, H⟩⟩,
rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
refine ⟨(ε/2)⁻¹ * ∥c∥ * 2 * n, _, λy, _⟩,
{ refine mul_nonneg (mul_nonneg (mul_nonneg _ (norm_nonneg _)) (by norm_num)) _,
refine inv_nonneg.2 (div_nonneg' (le_of_lt εpos) (by norm_num)),
exact nat.cast_nonneg n },
{ by_cases hy : y = 0,
{ use 0, simp [hy, lin.map_zero] },
{ rcases rescale_to_shell hc (half_pos εpos) hy with ⟨d, hd, ydle, leyd, dinv⟩,
let δ := ∥d∥ * ∥y∥/4,
have δpos : 0 < δ :=
div_pos (mul_pos (norm_pos_iff.2 hd) (norm_pos_iff.2 hy)) (by norm_num),
have : a + d • y ∈ ball a ε,
by simp [dist_eq_norm, lt_of_le_of_lt ydle (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, 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, lin.map_sub], abel }
... ≤ ∥f x₁ - (a + d • y)∥ + ∥f x₂ - a∥ :
norm_sub_le _ _
... ≤ δ + δ : begin
apply add_le_add,
{ rw [← dist_eq_norm, dist_comm], exact le_of_lt h₁ },
{ rw [← dist_eq_norm, dist_comm], exact le_of_lt h₂ }
end
... = 2 * δ : (two_mul _).symm,
have J : ∥f (d⁻¹ • x) - y∥ ≤ 1/2 * ∥y∥ := calc
∥f (d⁻¹ • x) - y∥ = ∥d⁻¹ • f x - (d⁻¹ * d) • y∥ :
by rwa [lin.smul, inv_mul_cancel, one_smul]
... = ∥d⁻¹ • (f x - d • y)∥ : by rw [mul_smul, smul_sub]
... = ∥d∥⁻¹ * ∥f x - d • y∥ : by rw [norm_smul, normed_field.norm_inv]
... ≤ ∥d∥⁻¹ * (2 * δ) : begin
apply mul_le_mul_of_nonneg_left I,
rw inv_nonneg,
exact norm_nonneg _
end
... = (∥d∥⁻¹ * ∥d∥) * ∥y∥ /2 : by { simp only [δ], ring }
... = ∥y∥/2 : by { rw [inv_mul_cancel, one_mul], simp [norm_eq_zero, hd] }
... = (1/2) * ∥y∥ : by ring,
rw ← dist_eq_norm at J,
have 𝕜 : ∥d⁻¹ • x∥ ≤ (ε / 2)⁻¹ * ∥c∥ * 2 * ↑n * ∥y∥ := calc
∥d⁻¹ • x∥ = ∥d∥⁻¹ * ∥x₁ - x₂∥ : by rw [norm_smul, normed_field.norm_inv]
... ≤ ((ε / 2)⁻¹ * ∥c∥ * ∥y∥) * (n + n) : begin
refine mul_le_mul dinv _ (norm_nonneg _) _,
{ exact le_trans (norm_sub_le _ _) (add_le_add (le_of_lt hx₁) (le_of_lt hx₂)) },
{ apply mul_nonneg (mul_nonneg _ (norm_nonneg _)) (norm_nonneg _),
exact inv_nonneg.2 (le_of_lt (half_pos εpos)) }
end
... = (ε / 2)⁻¹ * ∥c∥ * 2 * ↑n * ∥y∥ : by ring,
exact ⟨d⁻¹ • x, J, 𝕜⟩ } } },
rcases this with ⟨C, C0, hC⟩,
rcases this with ⟨n, a, ε, ⟨εpos, H⟩⟩,
rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
refine ⟨(ε/2)⁻¹ * ∥c∥ * 2 * n, _, λy, _⟩,
{ refine mul_nonneg (mul_nonneg (mul_nonneg _ (norm_nonneg _)) (by norm_num)) _,
refine inv_nonneg.2 (div_nonneg' (le_of_lt εpos) (by norm_num)),
exact nat.cast_nonneg n },
{ by_cases hy : y = 0,
{ use 0, simp [hy, lin.map_zero] },
{ rcases rescale_to_shell hc (half_pos εpos) hy with ⟨d, hd, ydle, leyd, dinv⟩,
let δ := ∥d∥ * ∥y∥/4,
have δpos : 0 < δ :=
div_pos (mul_pos (norm_pos_iff.2 hd) (norm_pos_iff.2 hy)) (by norm_num),
have : a + d • y ∈ ball a ε,
by simp [dist_eq_norm, lt_of_le_of_lt ydle (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, 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, lin.map_sub], abel }
... ≤ ∥f x₁ - (a + d • y)∥ + ∥f x₂ - a∥ :
norm_sub_le _ _
... ≤ δ + δ : begin
apply add_le_add,
{ rw [← dist_eq_norm, dist_comm], exact le_of_lt h₁ },
{ rw [← dist_eq_norm, dist_comm], exact le_of_lt h₂ }
end
... = 2 * δ : (two_mul _).symm,
have J : ∥f (d⁻¹ • x) - y∥ ≤ 1/2 * ∥y∥ := calc
∥f (d⁻¹ • x) - y∥ = ∥d⁻¹ • f x - (d⁻¹ * d) • y∥ :
by rwa [lin.smul, inv_mul_cancel, one_smul]
... = ∥d⁻¹ • (f x - d • y)∥ : by rw [mul_smul, smul_sub]
... = ∥d∥⁻¹ * ∥f x - d • y∥ : by rw [norm_smul, normed_field.norm_inv]
... ≤ ∥d∥⁻¹ * (2 * δ) : begin
apply mul_le_mul_of_nonneg_left I,
rw inv_nonneg,
exact norm_nonneg _
end
... = (∥d∥⁻¹ * ∥d∥) * ∥y∥ /2 : by { simp only [δ], ring }
... = ∥y∥/2 : by { rw [inv_mul_cancel, one_mul], simp [norm_eq_zero, hd] }
... = (1/2) * ∥y∥ : by ring,
rw ← dist_eq_norm at J,
have 𝕜 : ∥d⁻¹ • x∥ ≤ (ε / 2)⁻¹ * ∥c∥ * 2 * ↑n * ∥y∥ := calc
∥d⁻¹ • x∥ = ∥d∥⁻¹ * ∥x₁ - x₂∥ : by rw [norm_smul, normed_field.norm_inv]
... ≤ ((ε / 2)⁻¹ * ∥c∥ * ∥y∥) * (n + n) : begin
refine mul_le_mul dinv _ (norm_nonneg _) _,
{ exact le_trans (norm_sub_le _ _) (add_le_add (le_of_lt hx₁) (le_of_lt hx₂)) },
{ apply mul_nonneg (mul_nonneg _ (norm_nonneg _)) (norm_nonneg _),
exact inv_nonneg.2 (le_of_lt (half_pos εpos)) }
end
... = (ε / 2)⁻¹ * ∥c∥ * 2 * ↑n * ∥y∥ : by ring,
exact ⟨d⁻¹ • x, J, 𝕜⟩ } },
end

variable [complete_space E]

/-- 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 (hf : is_bounded_linear_map 𝕜 f) (surj : surjective f) :
∃C, 0 < C ∧ ∀y, ∃x, f x = y ∧ ∥x∥ ≤ C * ∥y∥ :=
begin
have lin := hf.to_is_linear_map,
obtain ⟨C, C0, hC⟩ := exists_approx_preimage_norm_le hf surj,
/- Second step of the proof: starting from `y`, we want an exact preimage of `y`. Let `g y` be
the approximate preimage of `y` given by the first step, and `h y = y - f(g y)` the part that
has no preimage yet. We will iterate this process, taking the approximate preimage of `h y`,
Expand Down

0 comments on commit 06c5594

Please sign in to comment.