refactor: allow for bilinear maps of norm greater than one in Hölder's inequality and use HolderTriple

[j-loreaux]

This PR does two things, both related to statements of Hölder's inequality:

1. In the generic statements involving a general map b : E → F → G (which we think of as a continuous bilinear map despite the fact that these are not quite the hypotheses), we loosen the assumptions on b so that it need not have norm bounded by 1. This makes it possible to use general continuous bilinear maps in the forthcoming feat: Hölder triples and multiplication of MeasureTheory.Lp functions #21583, and addresses the concerns in Consequences of Hölder inequality for continuous bilinear maps #6108.
2. Changes the statements to make use of the new ENNReal.HolderTriple type class. Among other things, this makes some existing lemmas specialized to ∞ redundant, so we deprecate them.

Closes #6108.

---

• depends on: [Merged by Bors] - feat: Hölder triples / conjugates as a type class #21854

If this doesn't completely address #6108, let me know and I can do the rest of what you wanted.

[github-actions]

PR summary c38f1f2b04

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp	1716	1718	+2 (+0.12%)
Mathlib.MeasureTheory.Function.L1Space.Integrable	1904	1906	+2 (+0.11%)
Mathlib.MeasureTheory.Function.ContinuousMapDense	1933	1935	+2 (+0.10%)
Mathlib.Probability.CondVar	2017	2019	+2 (+0.10%)

Import changes for all files

Files	Import difference
Mathlib.Tactic	1
294 files Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.UnitPartition 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.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral 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.Convolution 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.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.SobolevInequality 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.PolarCoord Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SumIntegralComparisons Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable 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.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSpace.Basic Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.BochnerL1 Mathlib.MeasureTheory.Integral.Bochner Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.VectorMeasure.WithDensity 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.WellApproximable Mathlib.NumberTheory.ZetaValues Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Density Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Uniform Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Integration Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.Lemmas Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.MeasureComp Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.Basic 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.Integral Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.WithDensity 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.Moments.ComplexMGF Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Integrals 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 Mathlib.RingTheory.Polynomial.Selmer Mathlib.Tactic.NormNum.LegendreSymbol	2

---

Declarations diff

+ Memℒp.of_bilin

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: Hölder triples / conjugates as a type class #21854
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

Is there any chance you can split this PR into:

• "allow for bilinear maps of norm greater than one in Hölder's inequality"
• "use HolderTriple"

? The current diff is quite hard to read and the two changes seem essentially disjoint

[j-loreaux]

I don't think the diff being hard to read would change much if I split it. The "use Hölder triple" changes are pretty minor in terms of diff size (but I would essentially have to recreate them from scratch if I were to try and split the PR, and then I would have an annoying merge for the second PR unless I was very careful with git).

The main issue for the diff is that when generalizing to bilinear maps, I found it much easier to reprove some of the results from scratch (and in at least one case, shorten the proof considerably), by taking another approach. For example, I used ENNReal.trichotomy in one proof to give myself nicer case splits, and I stayed in the realm of eLpNorm before passing to the integral in another in order to make it easier to pull the constant out.

[YaelDillies]

Thanks!

maintainer delegate

[YaelDillies]

Do you think we should keep the c = 1 lemmas as convenient special cases?

[j-loreaux]

no, as you can see with the mul and smul results, it seems to only add an extra invocation of simp, so it's minor, and I think those are currently the only places the results are used in Mathlib.

[YaelDillies]

Would you mind commenting that on fpvandoorn/carleson#231? @js2357 is similarly adding c = 1 special cases there

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.