[Merged by Bors] - feat(Analysis/InnerProductSpace/Dual, Analysis/Normed/Group/SeparationQuotient): add null subspaces by yoh-tanimoto · Pull Request #16707 · leanprover-community/mathlib4

yoh-tanimoto · 2024-09-11T11:35:51Z

Define the null submodule in an InnerProductSpace and the null subgroup in a NormedAddCommGroup and prove basic properties.

~~Define the null space in an InnerProductSpace without definite and add InnerProduceSpace structure to the quotient by the null space.~~

Motivation: This PR has evolved from a PR defining the SeparationQuotient for InnerProductSpace. That has been done in #17452 and now contains some other things.

Depends on: [Merged by Bors] - chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup #17007
Depends on: [Merged by Bors] - chore(Analysis/InnerProductSpace/Dual): weaken assumptions to SeminormedAddCommGroup #17416
Depends on: [Merged by Bors] - feat: add Normed instances for SeparationQuotient #17452

github-actions · 2024-09-11T11:36:40Z

PR summary 6d539fd27f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
30 files `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Analysis.InnerProductSpace.LaxMilgram`	1
`Mathlib.Analysis.Normed.Group.NullSubmodule`	1202

Declarations diff

+ inner_eq_zero_of_left
+ inner_eq_zero_of_right
+ isClosed_nullSubgroup
+ isClosed_nullSubmodule
+ mem_nullSubgroup_iff
+ mem_nullSubmodule_iff
+ mk_eq_one_iff
+ nnnorm_div_eq_nnnorm_left
+ nnnorm_div_eq_nnnorm_right
+ nnnorm_le_mul_nnnorm_add'
+ nnnorm_mul_eq_nnnorm_left
+ nnnorm_mul_eq_nnnorm_right
+ norm_div_eq_norm_left
+ norm_div_eq_norm_right
+ norm_le_mul_norm_add'
+ norm_mul_eq_norm_left
+ norm_mul_eq_norm_right
+ nullSubgroup
+ nullSubmodule
+ nullSubmodule_le_ker_toDualMap_left
+ nullSubmodule_le_ker_toDualMap_right

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

Mathlib/Analysis/InnerProductSpace/Quotient.lean

Mathlib/Analysis/InnerProductSpace/Basic.lean

Mathlib/Analysis/InnerProductSpace/Quotient.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…ddCommGroup` (#17007) replace the assumption `NormedAddCommGroup` to `SemiNormedAddCommGroup` in various places. motivation: with the weakened assumption the results apply to `InnerProductSpace` without `definite` assumption. This is suggested in #16707, and continues from #14024. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

j-loreaux

I suspect that this is not the way to proceed here. Instead, I recommend using SeparationQuotient.

If we don't already have it, you could show that if X is a Seminormed* then SeparationQuotient X is a Normed*. Then you could define the inner product space isntance on SeparationQuotient X.

The problem with putting this InnerProductSpace instance on E / nullSpace \bbk E is that we could end up with non-defeq instances later down the line. Moreover, SeparationQuotient does almost exactly what you want already, it just doesn't have the necessary instances yet.

…roductspace-quotient

Mathlib/Analysis/InnerProductSpace/Quotient.lean

sync to master

yoh-tanimoto · 2024-09-26T11:06:57Z

@j-loreaux If I use SeparationQuotient and take the instance SeparationQuotient.instAddCommGroup, it is different from AddSubgroup.seminormedAddCommGroupQuotient, correct? Do I have to define the norm again for SeparationQuotient?

j-loreaux · 2024-09-29T01:36:52Z

Yes, it is certainly different, and you'll need to define the norm again, assuming the instance doesn't already exist. But I think this is the cleaner approach.

…roductspace-quotient

Mathlib/Analysis/Normed/Group/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Analysis/Normed/Group/Basic.lean

Mathlib/Analysis/Normed/Group/Uniform.lean

Mathlib/Analysis/Normed/Group/Basic.lean

Mathlib/Analysis/Normed/Group/SeparationQuotient.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser

bors d+

(again)

Thanks! Just a file rename to go.

Mathlib/Analysis/Normed/Group/SeparationQuotient.lean

eric-wieser · 2024-11-15T18:38:35Z

Mathlib/Analysis/Normed/Group/SeparationQuotient.lean

Now that this file doesn't mention SeparationQuotient.lean, perhaps it should be called NullSubmodule.lean or NullSpace.lean?

mathlib-bors · 2024-11-15T18:40:14Z

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

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…roductspace-quotient

yoh-tanimoto · 2024-11-15T20:09:38Z

bors r+

…nQuotient): add null subspaces (#16707) Define the null submodule in an `InnerProductSpace` and the null subgroup in a `NormedAddCommGroup` and prove basic properties. ~~Define the null space in an `InnerProductSpace` without `definite` and add `InnerProduceSpace` structure to the quotient by the null space.~~ Motivation: This PR has evolved from a PR defining the `SeparationQuotient` for `InnerProductSpace`. That has been done in #17452 and now contains some other things. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

mathlib-bors · 2024-11-15T20:19:18Z

Pull request successfully merged into master.

Build succeeded:

…nQuotient): add null subspaces (#16707) Define the null submodule in an `InnerProductSpace` and the null subgroup in a `NormedAddCommGroup` and prove basic properties. ~~Define the null space in an `InnerProductSpace` without `definite` and add `InnerProduceSpace` structure to the quotient by the null space.~~ Motivation: This PR has evolved from a PR defining the `SeparationQuotient` for `InnerProductSpace`. That has been done in #17452 and now contains some other things. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

yoh-tanimoto added 7 commits September 6, 2024 19:32

put Semi

58dbb79

put Semi

cbe33c3

Create Quotient.lean

e973783

Update Quotient.lean

01c83b1

Update Quotient.lean

ef8ba7c

add line to Mathlib.lean

57289ae

add docstring

795b1a3

yoh-tanimoto added RFC Request for comment t-analysis Analysis (normed *, calculus) labels Sep 11, 2024

eric-wieser reviewed Sep 11, 2024

View reviewed changes

yoh-tanimoto and others added 5 commits September 13, 2024 00:39

Update Mathlib/Analysis/InnerProductSpace/Quotient.lean

b3d12f0

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Mathlib/Analysis/InnerProductSpace/Quotient.lean

5432128

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Mathlib/Analysis/InnerProductSpace/Quotient.lean

77411bd

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Mathlib/Analysis/InnerProductSpace/Quotient.lean

e9ded34

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Quotient.lean

130243e

yoh-tanimoto changed the title ~~feat(Analysis/InnerProductSpace/Quotient): add the quotient InnerProductSpace.Core by the null space~~ feat(Analysis/InnerProductSpace/Quotient): add the quotient InnerProductSpace by the null space Sep 12, 2024

yoh-tanimoto mentioned this pull request Sep 21, 2024

[Merged by Bors] - chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup #17007

Closed

j-loreaux reviewed Sep 25, 2024

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 25, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 25, 2024

Merge remote-tracking branch 'origin/master' into yoh-tanimoto-innerp…

72dd13e

…roductspace-quotient

eric-wieser reviewed Sep 25, 2024

View reviewed changes

Mathlib/Analysis/InnerProductSpace/Quotient.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 25, 2024

Merge pull request #17157 from leanprover-community/master

a1a093f

sync to master

Update Quotient.lean

1d99e4b

Merge remote-tracking branch 'origin/master' into yoh-tanimoto-innerp…

9e29b5d

…roductspace-quotient

yoh-tanimoto added 3 commits November 15, 2024 09:41

Merge remote-tracking branch 'origin/master' into yoh-tanimoto-innerp…

cba365c

…roductspace-quotient

#min_imports and cleanup

92c9a4c

correct name

f48088a