Skip to content

[Merged by Bors] - feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule#20084

Closed
mans0954 wants to merge 9 commits intomasterfrom
mans0954/normed-polarSubmodule
Closed

[Merged by Bors] - feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule#20084
mans0954 wants to merge 9 commits intomasterfrom
mans0954/normed-polarSubmodule

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented Dec 19, 2024

@mans0954 mans0954 added the t-analysis Analysis (normed *, calculus) label Dec 19, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 19, 2024 •
edited
Loading

PR summary 01bcb62aae

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ mem_polarSubmodule
+ polarSubmodule
+ polarSubmodule_eq_polar
+ polarSubmodule_eq_setOf

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).

@mans0954 mans0954 mentioned this pull request Dec 19, 2024
Closed
2 tasks
jcommelin
jcommelin reviewed Jan 22, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you please add a lemma mem_polarSubmodule that proves the characterization "consisting of those functionals which evaluate to zero at all points z ∈ s"?

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 22, 2025
mans0954 and others added 3 commits January 22, 2025 18:12
@mans0954 mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 22, 2025
jcommelin
jcommelin reviewed Jan 31, 2025
View reviewed changes
jcommelin
jcommelin reviewed Jan 31, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 31, 2025

✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 31, 2025
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 1, 2025
@mans0954 @jcommelin
Update Mathlib/Analysis/Normed/Module/Dual.lean
01bcb62 
Co-authored-by: Johan Commelin <johan@commelin.net>
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Feb 1, 2025

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 1, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 1, 2025
@mans0954
feat(Analysis/Normed/Module/Dual): polar in a normed space as a submo…
e736b5a 
…dule (#20084)

Definition of the polar of a subspace closed under scalar multiplication as a submodule.

- Follows on from #14458
- Motivation #14369




Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 1, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule [Merged by Bors] - feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule Feb 1, 2025
@mathlib-bors mathlib-bors bot closed this Feb 1, 2025
@mathlib-bors mathlib-bors bot deleted the mans0954/normed-polarSubmodule branch February 1, 2025 08:59
Julian added a commit that referenced this pull request Feb 2, 2025
@Julian
Merge branch 'factorial-dvd-int' into bhargava-factorial
4aa075f 
* factorial-dvd-int: (143 commits)
  Apply suggestions from code review
  feat(Factorial): k! divides the product of any k successive integers
  feat(CategoryTheory): creation of finite limits (#21320)
  chore: update Mathlib dependencies 2025-02-01 (#21328)
  chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314)
  feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306)
  chore: cleanup imports in Archive/IfNormalization (#21318)
  doc: fix several typos (#21315)
  feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310)
  chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271)
  feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084)
  chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308)
  feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522)
  feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168)
  chore: update Mathlib dependencies 2025-02-01 (#21312)
  chore: update Mathlib dependencies 2025-01-31 (#21311)
  feat: generalize `mem_dite` to `Membership α β` (#21262)
  feat: Lemmas for some monomial orders (#16177)
  feat(CategoryTheory): the localized category is monoidal (#12728)
  feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289)
  feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295)
  feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284)
  fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299)
  feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199)
  refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653)
  feat(RingTheory/PowerSeries): binomial series (#20192)
  chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff  (#21290)
  chore (RingTheory/HahnSeries): fix names that use coeff (#21279)
  feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233)
  chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273)
  feat(CategoryTheory): the monoidal category structure on a localization (#20951)
  feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009)
  feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328)
  feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486)
  feat: Function.const as a PartialEquiv (#21137)
  chore(NonZeroDivisors): don't import rings (#20871)
  feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267)
  feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190)
  feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285)
  perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179)
  feat(Order): order isomorphisms from `Fin n` for small `n` (#21120)
  refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740)
  feat: Sylow's first theorem for elementary `p`-groups (#21072)
  chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748)
  refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213)
  feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186)
  feat(Algebra/Group/Action): add definition of equidecomposition (#16936)
  feat(CategoryTheory/Subpresheaf): equalizer (#21096)
  feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204)
  chore: update Mathlib dependencies 2025-01-31 (#21282)
  ...
jt496 pushed a commit that referenced this pull request Feb 3, 2025
@mans0954 @jt496
feat(Analysis/Normed/Module/Dual): polar in a normed space as a submo…
83c970a 
…dule (#20084)

Definition of the polar of a subspace closed under scalar multiplication as a submodule.

- Follows on from #14458
- Motivation #14369




Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mans0954 @jcommelin