feat(Analysis/LocallyConvex/Polar): Bipolar theorem #26345
Conversation
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
This reverts commit f8148c2.
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
|
I wonder what next steps on this are? Would it help if I broke it into smaller PRs to see if we can get some of the prerequisites for the main result merged? |
My fault, I took some delay. I hope to finish reviewing this by tonight (European time). |
There was a problem hiding this comment.
Thank you for all the work and the patience for my delay. I still find the proof of the bipolar theorem a bit intricate, but it is converging to a nice one. Perhaps we could add in the Geometric Hahn-Banach file a "normalized" version (with basic API) that might be useful elsewhere and would avoid introducing g out of f? If you think this would be reasonable, it would be the object of a separated PR, upon which the current one would depend — and, if so, please do mark it into the PR description.
| rw [← smul_eq_mul, ← smul_assoc] | ||
| norm_cast | ||
| have unz : u ≠ 0 := (ne_of_lt e3).symm | ||
| aesop |
There was a problem hiding this comment.
| aesop | |
| simp_all only [nonempty_subtype, Set.mem_compl_iff, one_div, ne_eq, not_false_eq_true, | |
| smul_inv_smul₀, ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul, mul_inv_cancel₀, | |
| map_one, one_mul] | |
| rfl |
This is certainly faster than aesop and reveals what is going on, but the terminal rfl is not super-nice: it somewhat shows that something should have been set up differently, so that the above simp_all call already closes the goal. If you can try to investigate, if not I'll give it another check later.
There was a problem hiding this comment.
I would have expected simp to be able to close this with flip_apply. If I change it to:
rw [flip_apply]
this fails with:
Tactic `rewrite` failed: Did not find an occurrence of the pattern
((flip ?f) ?n) ?m
in the target expression
(B.flip f₀) x = (B x) f₀
If I try
rw [← flip_apply]
Then the goal becomes:
⊢ (B.flip f₀) x = (B.flip f₀) x
The output with set_option pp.all true is too long for me to make sense of it.
faenuccio
added
the
awaiting-author
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
|
@mans0954 I let you check all my comments, then please ping me so that I can come back for another round of review. |
… a single ring of scalars (#29342) Currently the definition of Absolutely Convex in Mathlib is a little unexpected: ``` def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s ``` At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`. Recently the requirements for the definition of `Convex` have been relaxed (#24392, #20595) so it is now possible to use a single scalar ring in common with the literature. Previous discussion: - #17029 (comment) - #26345 (comment)
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
9 participants
The bipolar theorem states that the polar of the polar of a set
sis equal to the closed absolutely convex hull ofs.The argument here follows Conway, Chapter V. 1.8.
This PR continues the work from #20843.
Original PR: #20843