-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(analysis/normed_space/finite_dimension): Riesz theorem on compact unit ball and finite dimension #9147
Conversation
sgouezel
commented
Sep 11, 2021
|
||
/-- A sequence of points in an infinite-dimensional space, which are all bounded by `R` and at | ||
distance at least `1`. Use `exists_seq_norm_le_le_norm_sub` instead. -/ | ||
noncomputable def exists_seq_norm_le_one_le_norm_sub_aux |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
noncomputable def exists_seq_norm_le_one_le_norm_sub_aux | |
noncomputable def seq_norm_le_one_le_norm_sub_aux |
Should it be private
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think Floris told me that he hated private declarations because they can't be printed or checked, so I don't mark anything as private any more.
`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∥) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I saw this kind of induction more than once. Should we have a lemma like this one?
lemma nat.exists_fun_forall_lt_imp {α : Type*} (p : α → Prop) (r : α → α → Prop)
(H : ∀ (n : ℕ) (f : ℕ → α), ∃ y, p y ∧ ∀ k < n, r (f k) y) :
∃ f : ℕ → α, (∀ n, p n) ∧ ∀ m n, m < n → r m n := sorry
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BTW, H
can assume that f
satisfies ∀ k < n, p (f k)
and ∀ k l, k < l → l < n → r (f k) (f l)
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have added a version expressed in terms of finsets: if for any finset s
one can find a point y
with r x y
for all points in the finset, then one can find a sequence with r (f m) (f n)
whenever m < n
.
`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∥) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BTW, H
can assume that f
satisfies ∀ k < n, p (f k)
and ∀ k l, k < l → l < n → r (f k) (f l)
.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Thanks! 🎉 |
…t unit ball and finite dimension (#9147)
Pull request successfully merged into master. Build succeeded: |
1 similar comment
Pull request successfully merged into master. Build succeeded: |