feat(analysis/normed_space/finite_dimension): Riesz theorem on compac…

…t unit ball and finite dimension (#9147)

docs/undergrad.yaml

@@ -424,7 +424,7 @@ Topology:
     normed space of bounded continuous functions: 'bounded_continuous_function.normed_space'
     its completeness: 'bounded_continuous_function.complete_space'
     Heine-Borel theorem (closed bounded subsets are compact in finite dimension): 'finite_dimensional.proper'
-    Riesz' lemma (unit-ball characterization of finite dimension):
+    Riesz' lemma (unit-ball characterization of finite dimension): 'finite_dimensional_of_is_compact_closed_ball'
     Arzela-Ascoli theorem: 'bounded_continuous_function.arzela_ascoli'
   Hilbert spaces:
     Hilbert projection theorem: 'exists_norm_eq_infi_of_complete_convex'
@@ -456,7 +456,7 @@ Multivariable calculus:
     differentiable functions: 'differentiable'
     $k$-times continuously differentiable functions: 'times_cont_diff'
     $k$-th order partial derivatives:
-    partial derivatives commute:
+    partial derivatives commute: 'second_derivative_symmetric'
     Taylor's theorem with little-o remainder:
     Taylor's theorem with integral form for remainder:
     local extrema: 'is_local_min.fderiv_eq_zero'

src/analysis/normed_space/basic.lean

@@ -1632,7 +1632,7 @@ instance submodule.semi_normed_space {𝕜 R : Type*} [has_scalar 𝕜 R] [norme
   semi_normed_space 𝕜 s :=
 { norm_smul_le := λc x, le_of_eq $ norm_smul c (x : E) }
 
-/-- If there is a scalar `c` with `∥c∥>1`, then any element of with norm different from `0` can be
+/-- If there is a scalar `c` with `∥c∥>1`, then any element with nonzero norm can be
 moved by scalar multiplication to any shell of width `∥c∥`. Also recap information on the norm of
 the rescaling element that shows up in applications. -/
 lemma rescale_to_shell_semi_normed {c : α} (hc : 1 < ∥c∥) {ε : ℝ} (εpos : 0 < ε) {x : E}

src/analysis/normed_space/finite_dimension.lean

@@ -28,6 +28,8 @@ are continuous. Moreover, a finite-dimensional subspace is always complete and c
   resolution. It is however registered as an instance for `𝕜 = ℝ` and `𝕜 = ℂ`. As properness
   implies completeness, there is no need to also register `finite_dimensional.complete` on `ℝ` or
   `ℂ`.
+* `finite_dimensional_of_is_compact_closed_ball`: Riesz' theorem: if the closed unit ball is
+  compact, then the space is finite-dimensional.
 
 ## Implementation notes
 
@@ -403,6 +405,91 @@ lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dime
   is_closed (s : set E) :=
 s.complete_of_finite_dimensional.is_closed
 
+section riesz
+
+/-- In an infinite dimensional space, given a finite number of points, one may find a point
+with norm at most `R` which is at distance at least `1` of all these points. -/
+theorem exists_norm_le_le_norm_sub_of_finset {c : 𝕜} (hc : 1 < ∥c∥) {R : ℝ} (hR : ∥c∥ < R)
+  (h : ¬ (finite_dimensional 𝕜 E)) (s : finset E) :
+  ∃ (x : E), ∥x∥ ≤ R ∧ ∀ y ∈ s, 1 ≤ ∥y - x∥ :=
+begin
+  let F := submodule.span 𝕜 (s : set E),
+  haveI : finite_dimensional 𝕜 F,
+  { apply is_noetherian_span_of_finite _ (finset.finite_to_set s), apply_instance },
+  have Fclosed : is_closed (F : set E) := submodule.closed_of_finite_dimensional _,
+  have : ∃ x, x ∉ F,
+  { contrapose! h,
+    have : (⊤ : submodule 𝕜 E) = F, by { ext x, simp [h] },
+    have : finite_dimensional 𝕜 (⊤ : submodule 𝕜 E), by rwa this,
+    exact is_noetherian_top_iff.1 this },
+  obtain ⟨x, xR, hx⟩ : ∃ (x : E), ∥x∥ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ∥x - y∥ :=
+    riesz_lemma_of_norm_lt hc hR Fclosed this,
+  have hx' : ∀ (y : E), y ∈ F → 1 ≤ ∥y - x∥,
+  { assume y hy, rw ← norm_neg, simpa using hx y hy },
+  exact ⟨x, xR, λ y hy, hx' _ (submodule.subset_span hy)⟩,
+end
+
+/-- In an infinite-dimensional normed space, there exists a sequence of points which are all
+bounded by `R` and at distance at least `1`. For a version not assuming `c` and `R`, see
+`exists_seq_norm_le_one_le_norm_sub`. -/
+theorem exists_seq_norm_le_one_le_norm_sub' {c : 𝕜} (hc : 1 < ∥c∥) {R : ℝ} (hR : ∥c∥ < R)
+  (h : ¬ (finite_dimensional 𝕜 E)) :
+  ∃ f : ℕ → E, (∀ n, ∥f n∥ ≤ R) ∧ (∀ m n, m ≠ n → 1 ≤ ∥f m - f n∥) :=
+begin
+  haveI : is_symm E (λ (x y : E), 1 ≤ ∥x - y∥),
+  { constructor,
+    assume x y hxy,
+    rw ← norm_neg,
+    simpa },
+  apply exists_seq_of_forall_finset_exists' (λ (x : E), ∥x∥ ≤ R) (λ (x : E) (y : E), 1 ≤ ∥x - y∥),
+  assume s hs,
+  exact exists_norm_le_le_norm_sub_of_finset hc hR h s,
+end
+
+theorem exists_seq_norm_le_one_le_norm_sub (h : ¬ (finite_dimensional 𝕜 E)) :
+  ∃ (R : ℝ) (f : ℕ → E), (1 < R) ∧ (∀ n, ∥f n∥ ≤ R) ∧ (∀ m n, m ≠ n → 1 ≤ ∥f m - f n∥) :=
+begin
+  obtain ⟨c, hc⟩ : ∃ (c : 𝕜), 1 < ∥c∥ := normed_field.exists_one_lt_norm 𝕜,
+  have A : ∥c∥ < ∥c∥ + 1, by linarith,
+  rcases exists_seq_norm_le_one_le_norm_sub' hc A h with ⟨f, hf⟩,
+  exact ⟨∥c∥ + 1, f, hc.trans A, hf.1, hf.2⟩
+end
+
+variable (𝕜)
+/-- Riesz's theorem: if the unit ball is compact in a vector space, then the space is
+finite-dimensional. -/
+theorem finite_dimensional_of_is_compact_closed_ball {r : ℝ} (rpos : 0 < r)
+  (h : is_compact (metric.closed_ball (0 : E) r)) : finite_dimensional 𝕜 E :=
+begin
+  by_contra hfin,
+  obtain ⟨R, f, Rgt, fle, lef⟩ :
+    ∃ (R : ℝ) (f : ℕ → E), (1 < R) ∧ (∀ n, ∥f n∥ ≤ R) ∧ (∀ m n, m ≠ n → 1 ≤ ∥f m - f n∥) :=
+      exists_seq_norm_le_one_le_norm_sub hfin,
+  have rRpos : 0 < r / R := div_pos rpos (zero_lt_one.trans Rgt),
+  obtain ⟨c, hc⟩ : ∃ (c : 𝕜), 0 < ∥c∥ ∧ ∥c∥ < (r / R) := normed_field.exists_norm_lt _ rRpos,
+  let g := λ (n : ℕ), c • f n,
+  have A : ∀ n, g n ∈ metric.closed_ball (0 : E) r,
+  { assume n,
+    simp only [norm_smul, dist_zero_right, metric.mem_closed_ball],
+    calc ∥c∥ * ∥f n∥ ≤ (r / R) * R : mul_le_mul hc.2.le (fle n) (norm_nonneg _) rRpos.le
+    ... = r : by field_simp [(zero_lt_one.trans Rgt).ne'] },
+  obtain ⟨x, hx, φ, φmono, φlim⟩ : ∃ (x : E) (H : x ∈ metric.closed_ball (0 : E) r) (φ : ℕ → ℕ),
+    strict_mono φ ∧ tendsto (g ∘ φ) at_top (𝓝 x) := h.tendsto_subseq A,
+  have B : cauchy_seq (g ∘ φ) := φlim.cauchy_seq,
+  obtain ⟨N, hN⟩ : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → dist ((g ∘ φ) n) ((g ∘ φ) N) < ∥c∥ :=
+    metric.cauchy_seq_iff'.1 B (∥c∥) hc.1,
+  apply lt_irrefl (∥c∥),
+  calc ∥c∥ ≤ dist (g (φ (N+1))) (g (φ N)) : begin
+    conv_lhs { rw [← mul_one (∥c∥)] },
+    simp only [g, dist_eq_norm, ←smul_sub, norm_smul, -mul_one],
+    apply mul_le_mul_of_nonneg_left (lef _ _ (ne_of_gt _)) (norm_nonneg _),
+    exact φmono (nat.lt_succ_self N)
+  end
+  ... < ∥c∥ : hN (N+1) (nat.le_succ N)
+end
+
+end riesz
+
 lemma continuous_linear_map.exists_right_inverse_of_surjective [finite_dimensional 𝕜 F]
   (f : E →L[𝕜] F) (hf : f.range = ⊤) :
   ∃ g : F →L[𝕜] E, f.comp g = continuous_linear_map.id 𝕜 F :=

src/analysis/normed_space/riesz_lemma.lean

@@ -9,8 +9,11 @@ import topology.metric_space.hausdorff_distance
 # Riesz's lemma
 
 Riesz's lemma, stated for a normed space over a normed field: for any
-closed proper subspace F of E, there is a nonzero x such that ∥x - F∥
-is at least r * ∥x∥ for any r < 1.
+closed proper subspace `F` of `E`, there is a nonzero `x` such that `∥x - F∥`
+is at least `r * ∥x∥` for any `r < 1`. This is `riesz_lemma`.
+
+In a nondiscrete normed field (with an element `c` of norm `> 1`) and any `R > ∥c∥`, one can
+guarantee `∥x∥ ≤ R` and `∥x - y∥ ≥ 1` for any `y` in `F`. This is `riesz_lemma_of_norm_lt`.
 -/
 
 variables {𝕜 : Type*} [normed_field 𝕜]
@@ -20,7 +23,8 @@ variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
 vector with norm 1 whose distance to a closed proper subspace is
 arbitrarily close to 1. The statement here is in terms of multiples of
 norms, since in general the existence of an element of norm exactly 1
-is not guaranteed. -/
+is not guaranteed. For a variant giving an element with norm in `[1, R]`, see
+`riesz_lemma_of_norm_lt`. -/
 lemma riesz_lemma {F : subspace 𝕜 E} (hFc : is_closed (F : set E))
   (hF : ∃ x : E, x ∉ F) {r : ℝ} (hr : r < 1) :
   ∃ x₀ : E, x₀ ∉ F ∧ ∀ y ∈ F, r * ∥x₀∥ ≤ ∥x₀ - y∥ :=
@@ -51,3 +55,38 @@ begin
     ... ≤ dist x (y₀ + y) : metric.inf_dist_le_dist_of_mem hy₀y
     ... = ∥x - y₀ - y∥ : by { rw [sub_sub, dist_eq_norm] }
 end
+
+/--
+A version of Riesz lemma: given a strict closed subspace `F`, one may find an element of norm `≤ R`
+which is at distance  at least `1` of every element of `F`. Here, `R` is any given constant
+strictly larger than the norm of an element of norm `> 1`. For a version without an `R`, see
+`riesz_lemma`.
+
+Since we are considering a general nondiscrete normed field, there may be a gap in possible norms
+(for instance no element of norm in `(1,2)`). Hence, we can not allow `R` arbitrarily close to `1`,
+and require `R > ∥c∥` for some `c : 𝕜` with norm `> 1`.
+-/
+lemma riesz_lemma_of_norm_lt
+  {c : 𝕜} (hc : 1 < ∥c∥) {R : ℝ} (hR : ∥c∥ < R)
+  {F : subspace 𝕜 E} (hFc : is_closed (F : set E)) (hF : ∃ x : E, x ∉ F) :
+  ∃ x₀ : E, ∥x₀∥ ≤ R ∧ ∀ y ∈ F, 1 ≤ ∥x₀ - y∥ :=
+begin
+  have Rpos : 0 < R := (norm_nonneg _).trans_lt hR,
+  have : ∥c∥ / R < 1, by { rw div_lt_iff Rpos, simpa using hR },
+  rcases riesz_lemma hFc hF this with ⟨x, xF, hx⟩,
+  have x0 : x ≠ 0 := λ H, by simpa [H] using xF,
+  obtain ⟨d, d0, dxlt, ledx, -⟩ :
+    ∃ (d : 𝕜), d ≠ 0 ∧ ∥d • x∥ < R ∧ R / ∥c∥ ≤ ∥d • x∥ ∧ ∥d∥⁻¹ ≤ R⁻¹ * ∥c∥ * ∥x∥ :=
+      rescale_to_shell hc Rpos x0,
+  refine ⟨d • x, dxlt.le, λ y hy, _⟩,
+  set y' := d⁻¹ • y with hy',
+  have y'F : y' ∈ F, by simp [hy', submodule.smul_mem _ _ hy],
+  have yy' : y = d • y', by simp [hy', smul_smul, mul_inv_cancel d0],
+  calc 1 = (∥c∥/R) * (R/∥c∥) : by field_simp [Rpos.ne', (zero_lt_one.trans hc).ne']
+  ... ≤ (∥c∥/R) * (∥d • x∥) :
+    mul_le_mul_of_nonneg_left ledx (div_nonneg (norm_nonneg _) Rpos.le)
+  ... = ∥d∥ * (∥c∥/R * ∥x∥) : by { simp [norm_smul], ring }
+  ... ≤ ∥d∥ * ∥x - y'∥ :
+    mul_le_mul_of_nonneg_left (hx y' (by simp [hy', submodule.smul_mem _ _ hy])) (norm_nonneg _)
+  ... = ∥d • x - y∥ : by simp [yy', ← smul_sub, norm_smul],
+end

src/data/fintype/basic.lean

@@ -1861,3 +1861,65 @@ begin
 end
 
 end fintype
+
+/-- Auxiliary definition to show `exists_seq_of_forall_finset_exists`. -/
+noncomputable def seq_of_forall_finset_exists_aux
+  {α : Type*} [decidable_eq α] (P : α → Prop) (r : α → α → Prop)
+  (h : ∀ (s : finset α), ∃ y, (∀ x ∈ s, P x) → (P y ∧ (∀ x ∈ s, r x y))) : ℕ → α
+| n := classical.some (h (finset.image (λ (i : fin n), seq_of_forall_finset_exists_aux i)
+        (finset.univ : finset (fin n))))
+using_well_founded {dec_tac := `[exact i.2]}
+
+/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
+relation with respect to all the previously chosen points.
+
+More precisely, Assume that, for any finite set `s`, one can find another point satisfying
+some relation `r` with respect to all the points in `s`. Then one may construct a
+function `f : ℕ → α` such that `r (f m) (f n)` holds whenever `m < n`.
+We also ensure that all constructed points satisfy a given predicate `P`. -/
+lemma exists_seq_of_forall_finset_exists {α : Type*} (P : α → Prop) (r : α → α → Prop)
+  (h : ∀ (s : finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ (∀ x ∈ s, r x y)) :
+  ∃ (f : ℕ → α), (∀ n, P (f n)) ∧ (∀ m n, m < n → r (f m) (f n)) :=
+begin
+  classical,
+  haveI : nonempty α,
+  { rcases h ∅ (by simp) with ⟨y, hy⟩,
+    exact ⟨y⟩ },
+  choose! F hF using h,
+  have h' : ∀ (s : finset α), ∃ y, (∀ x ∈ s, P x) → (P y ∧ (∀ x ∈ s, r x y)) := λ s, ⟨F s, hF s⟩,
+  set f := seq_of_forall_finset_exists_aux P r h' with hf,
+  have A : ∀ (n : ℕ), P (f n),
+  { assume n,
+    induction n using nat.strong_induction_on with n IH,
+    have IH' : ∀ (x : fin n), P (f x) := λ n, IH n.1 n.2,
+    rw [hf, seq_of_forall_finset_exists_aux],
+    exact (classical.some_spec (h' (finset.image (λ (i : fin n), f i)
+      (finset.univ : finset (fin n)))) (by simp [IH'])).1 },
+  refine ⟨f, A, λ m n hmn, _⟩,
+  nth_rewrite 1 hf,
+  rw seq_of_forall_finset_exists_aux,
+  apply (classical.some_spec (h' (finset.image (λ (i : fin n), f i)
+    (finset.univ : finset (fin n)))) (by simp [A])).2,
+  exact finset.mem_image.2 ⟨⟨m, hmn⟩, finset.mem_univ _, rfl⟩,
+end
+
+/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
+symmetric relation with respect to all the previously chosen points.
+
+More precisely, Assume that, for any finite set `s`, one can find another point satisfying
+some relation `r` with respect to all the points in `s`. Then one may construct a
+function `f : ℕ → α` such that `r (f m) (f n)` holds whenever `m ≠ n`.
+We also ensure that all constructed points satisfy a given predicate `P`. -/
+lemma exists_seq_of_forall_finset_exists' {α : Type*} (P : α → Prop) (r : α → α → Prop)
+  [is_symm α r]
+  (h : ∀ (s : finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ (∀ x ∈ s, r x y)) :
+  ∃ (f : ℕ → α), (∀ n, P (f n)) ∧ (∀ m n, m ≠ n → r (f m) (f n)) :=
+begin
+  rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩,
+  refine ⟨f, hf, λ m n hmn, _⟩,
+  rcases lt_trichotomy m n with h|rfl|h,
+  { exact hf' m n h },
+  { exact (hmn rfl).elim },
+  { apply symm,
+    exact hf' n m h }
+end

src/ring_theory/noetherian.lean

@@ -378,6 +378,14 @@ theorem is_noetherian_of_linear_equiv (f : M ≃ₗ[R] P)
   [is_noetherian R M] : is_noetherian R P :=
 is_noetherian_of_surjective _ f.to_linear_map f.range
 
+lemma is_noetherian_top_iff :
+  is_noetherian R (⊤ : submodule R M) ↔ is_noetherian R M :=
+begin
+  unfreezingI { split; assume h },
+  { exact is_noetherian_of_linear_equiv (linear_equiv.of_top (⊤ : submodule R M) rfl) },
+  { exact is_noetherian_of_linear_equiv (linear_equiv.of_top (⊤ : submodule R M) rfl).symm },
+end
+
 lemma is_noetherian_of_injective [is_noetherian R P] (f : M →ₗ[R] P) (hf : f.ker = ⊥) :
   is_noetherian R M :=
 is_noetherian_of_linear_equiv (linear_equiv.of_injective f $ linear_map.ker_eq_bot.mp hf).symm