[Merged by Bors] - feat(analysis/convex/uniform): Uniformly convex spaces #13480
Conversation
YaelDillies
added
the
awaiting-review
| /-- An inner product space is strictly convex. We do not register this as an instance for an inner | ||
| space over `𝕜`, `is_R_or_C 𝕜`, because there is no order of the typeclass argument that does not | ||
| lead to a search of `[is_scalar_tower ℝ ?m E]` with unknown `?m`. -/ | ||
| instance inner_product_space.strict_convex_space : strict_convex_space ℝ F := | ||
| begin | ||
| refine strict_convex_space.of_norm_add (λ x y h, _), | ||
| rw [same_ray_iff_norm_smul_eq, eq_comm, ← inner_eq_norm_mul_iff_real, | ||
| real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, h, | ||
| add_mul_self_eq, sub_sub, add_sub_add_right_eq_sub, add_sub_cancel', mul_assoc, | ||
| mul_div_cancel_left], | ||
| exact _root_.two_ne_zero | ||
| end |
There was a problem hiding this comment.
@urkud, do you wish to keep this proof around? Would it work to prove inner_product_space ℂ E → strict_convex_space ℂ E?
There was a problem hiding this comment.
There was a problem hiding this comment.
Oh exciting! Ping me when it's out.
leanprover-community-bot-assistant
added
merge-conflict
|
This PR/issue depends on: |
leanprover-community-bot-assistant
removed
the
merge-conflict
| @@ -172,6 +172,9 @@ lemma norm_add_le_of_le {g₁ g₂ : E} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ | |||
| ∥g₁ + g₂∥ ≤ n₁ + n₂ := | |||
| le_trans (norm_add_le g₁ g₂) (add_le_add H₁ H₂) | |||
|
|
|||
| lemma norm_add₃_le (x y z : E) : ∥x + y + z∥ ≤ ∥x∥ + ∥y∥ + ∥z∥ := | |||
There was a problem hiding this comment.
Do you want me to rename this lemma? I think abs_add_three is a bad name because it looks like it's about |a + 3|.
src/analysis/convex/uniform.lean
Outdated
| variables [normed_space ℝ E] | ||
|
|
||
| lemma exists_forall_sphere_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) : | ||
| ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ∥x∥ = r → ∀ ⦃y⦄, ∥y∥ = r → ε ≤ ∥x - y∥ → ∥x + y∥ ≤ 2 * r - δ := |
There was a problem hiding this comment.
You don't use this lemma in the next one, so you can move it below exists_forall_ball_dist_add_le_two_mul_sub and easily deduce it from that lemma.
There was a problem hiding this comment.
Hmmm... yeah but actually once you use the modulus of convexity, this is really quite different.
There was a problem hiding this comment.
I will delete it for now.
|
Thanks! |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
Thanks! I will rework this with the modulus of convexity when I have time. bors merge |
Define uniformly convex spaces and prove the implications `inner_product_space ℝ E → uniform_convex_space E` and `uniform_convex_space E → strict_convex_space ℝ E`.
|
Build failed (retrying...): |
Define uniformly convex spaces and prove the implications `inner_product_space ℝ E → uniform_convex_space E` and `uniform_convex_space E → strict_convex_space ℝ E`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…ace.to_uniform_convex_space From #13480.
Define uniformly convex spaces and prove the implications
inner_product_space ℝ E → uniform_convex_space Eanduniform_convex_space E → strict_convex_space ℝ E.sqrt x < y ↔ x < y^2#13546