Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex #21002

Open
wants to merge 33 commits into
base: master
Choose a base branch
from

Conversation

mans0954
Copy link
Collaborator

@mans0954 mans0954 commented Jan 23, 2025

Show that the absolute polar is weak*-closed and absolutely convex.

Via closedAbsConvexHull_min this establishes the easy direction of the Bipolar Theorem #20843


Open in Gitpod

@mans0954 mans0954 added the WIP Work in progress label Jan 23, 2025
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 23, 2025
Copy link

github-actions bot commented Jan 23, 2025

PR summary 89774b7a34

Import changes exceeding 2%

% File
+4.59% Mathlib.Analysis.LocallyConvex.Polar

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Analysis.LocallyConvex.Polar 1308 1368 +60 (+4.59%)
Mathlib.Analysis.Normed.Module.Dual 1764 1768 +4 (+0.23%)
Import changes for all files
Files Import difference
158 files Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.NumberTheory.ZetaValues Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.MGFAnalytic Mathlib.RingTheory.Polynomial.Selmer Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic
2
69 files Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Density Mathlib.Probability.Distributions.Uniform Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Notation Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Stopping Mathlib.Probability.StrongLaw Mathlib.Probability.Variance
3
6 files Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.WeakDual
4
Mathlib.Analysis.LocallyConvex.Polar 60

Declarations diff

+ AbsConvex.iInter₂
+ Balanced.mulActionHom_preimage
+ balanced_closedBall_zero
+ closedBall_normSeminorm
+ polar_AbsConvex
+ polar_eq_biInter_preimage
+ polar_isClosed

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

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Jan 23, 2025
@mans0954 mans0954 changed the title Show that the polar is absolutely convex feature(Analysis/LocallyConvex/Polar): Show that the polar is absolutely convex Jan 23, 2025
@mans0954 mans0954 changed the title feature(Analysis/LocallyConvex/Polar): Show that the polar is absolutely convex feature(Analysis/LocallyConvex/Polar): Show that the polar is weak*-closed and absolutely convex Jan 23, 2025
@mans0954 mans0954 marked this pull request as ready for review January 23, 2025 22:28
@mans0954 mans0954 removed the WIP Work in progress label Jan 29, 2025
@mans0954
Copy link
Collaborator Author

Oops - forgot to remove the WIP label.

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes label Feb 14, 2025
@mans0954 mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes label Feb 14, 2025
@mans0954 mans0954 requested a review from j-loreaux February 14, 2025 21:48
@j-loreaux
Copy link
Collaborator

j-loreaux commented Feb 15, 2025

The import increase is unacceptably large. Can you try to find a better place with #find_home? Probably something in Analysis.Normed is the way to go, but I'm not certain.

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes label Feb 15, 2025
@mans0954
Copy link
Collaborator Author

The import increase is unacceptably large. Can you try to find a better place with #find_home? Probably something in Analysis.Normed is the way to go, but I'm not certain.

#find_home LinearMap.polar_AbsConvex and #find_home! LinearMap.polar_AbsConvex both say [Mathlib.Analysis.LocallyConvex.Polar].

(N.B. I haven't used #find_home before, so perhaps I'm doing something wrong?)

@leanprover-community-bot-assistant 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 Feb 17, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 17, 2025
@j-loreaux
Copy link
Collaborator

I think that's because in your branch you've edited the Polar file to have the necessary imports already.

@mans0954
Copy link
Collaborator Author

I think that's because in your branch you've edited the Polar file to have the necessary imports already.

I'm not really getting how this is supposed to work. I removed LinearMap.polar_AbsConvex from Mathlib/Analysis/LocallyConvex/Polar.lean and ran lake build. Then I created Mathlib/mwe.lean as:

import Mathlib

variable {𝕜 E F : Type*}

section NormedAlgebra

variable [NormedField 𝕜] [NormedSpace ℝ 𝕜] [AddCommMonoid E] [AddCommMonoid F]
variable [Module 𝕜 E] [Module 𝕜 F]

variable {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E)

variable [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 𝕜]

namespace LinearMap

theorem polar_AbsConvex : AbsConvex 𝕜 (B.polar s) := by
  rw [polar_eq_biInter_preimage]
  exact AbsConvex.iInter₂ fun i hi =>
    ⟨Balanced.mulActionHom_preimage (E := F) (balanced_closedBall_zero (E := 𝕜) (r := (1 : ℝ)))
      (𝕜 := 𝕜) (B i), Convex.linear_preimage (convex_closedBall _ _) (B i)⟩

#find_home! polar_AbsConvex

end LinearMap

But #find_home! polar_AbsConvex just says [Mathlib]?

@mans0954
Copy link
Collaborator Author

I had another go, copying the lemma into Mathlib.lean itself and renaming it. Now #find_home says [Mathlib.Analysis.Normed.Module.Dual], so I guess that's our answer?

@mans0954
Copy link
Collaborator Author

mans0954 commented Feb 21, 2025

Weirdly Analysis.LocallyConvex.Polar is still showing a change?

| File | Base Count | Head Count | Change |
| --- | --- | --- | --- |
| Mathlib.Analysis.LocallyConvex.Polar | 1308 | 1368 | +60 (+4.59%) |
| Mathlib.Analysis.Normed.Module.Dual | 1764 | 1768 | +4 (+0.23%) |

I don't understand what's happening here?

@mans0954 mans0954 added help-wanted The author needs attention to resolve issues and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 21, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
help-wanted The author needs attention to resolve issues large-import Automatically added label for PRs with a significant increase in transitive imports t-analysis Analysis (normed *, calculus)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants