feat(Analysis.Normed.Module.Milman-Pettis): add Milman-Pettis theorem

[faenuccio]

We add the Milman-Pettis theorem stating that an uniformly convex Banach space is reflexive.

---

[github-actions[bot]]

PR summary 45f9a2993d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Normed.Module.Milman-Pettis (new file)	1901

---

Declarations diff

+ IsClosed_image_ball + LinearIsometryEquiv_of_uniformConvexSpace + WeakClosure_subset_closedBall + WeakSpace.closure_subset + WeakSpace.isOpen_of_isClosed + double_dual_norm_eq + exists_ball_lt + exists_forall_closedBall_dist_lt + exists_forall_sphere_dist_lt + exists_functional_sub_one_lt + exists_nnorm_eq_one_lt_apply_of_lt_opNorm + exists_nnorm_eq_one_lt_apply_of_lt_opNorm' + instance : Module.IsReflexive ℝ E + milman_pettis + sphere_subset_closure + sphere_subset_image + surjective_iff_closedBall_subset_range + surjective_iff_sphere_subset_range + surjective_of_uniformConvexSpace

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Can you also update 1000.yaml once you finish proving the theorem? Completing a named theorem should be celebrated appropriately :-)

[faenuccio]

Can you also update 1000.yaml once you finish proving the theorem? Completing a named theorem should be celebrated appropriately :-)

Sure, good idea! As you see, I've just started off this morning (mainly as a training exercice towards our joint work) so it's still a long way to go. But I will certainly add it there when done!

[yhx-12243]

Goldstine.txt

Here is a proof for Goldstine theorem and several lemmas.

[faenuccio]

Goldstine.txt

Here is a proof for Goldstine theorem and several lemmas.

Thanks! I will incorporate this very soon (probably next week) and will ping you so that you can have a look.