[Merged by Bors] - chore(MeasureTheory): move Measure.comap to a new file

[urkud]

---

[github-actions]

PR summary 5d06c56807

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
383 files Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.Probability.BorelCantelli Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.Probability.Kernel.Defs Mathlib.Probability.Variance Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Probability.Distributions.Geometric Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Function.UnifTight Mathlib.NumberTheory.GaussSum Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.Analysis.Complex.AbsMax Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.MeasureTheory.Order.Lattice Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Complex Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.MeasureTheory.Group.Measure Mathlib.Probability.Kernel.Composition Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Probability.Martingale.OptionalSampling Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Algebra.Module.ZLattice.Basic Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Category.MeasCat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.Fourier.Inversion Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Dynamics.Ergodic.Conservative Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.MeasureTheory.Integral.Bochner Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Probability.Martingale.Basic Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.Sub Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Probability.Kernel.IntegralCompProd Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Data.Real.Pi.Leibniz Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.MeasureTheory.Group.LIntegral Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Kernel.Invariance Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Probability.Distributions.Uniform Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.NumberTheory.Liouville.Measure Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.MeasureTheory.Group.Pointwise Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Probability.Distributions.Poisson Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.LSeries.QuadraticNonvanishing Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.Fermat Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Probability.ConditionalProbability Mathlib.Analysis.BoxIntegral.Basic Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Analysis.BoxIntegral.Integrability Mathlib.MeasureTheory.Measure.VectorMeasure Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.L1Space Mathlib.MeasureTheory.Measure.Count Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Probability.Kernel.Basic Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Complex.Liouville Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.MeasureTheory.Function.Jacobian Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.MeasureTheory.Function.LpOrder Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.Topology.Baire.BaireMeasurable Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Dynamics.Ergodic.Ergodic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Measure.Dirac Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.Probability.Process.Stopping Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.Probability.Kernel.MeasureCompProd Mathlib.NumberTheory.ZetaValues Mathlib.MeasureTheory.Function.Egorov Mathlib.Probability.Independence.Basic Mathlib.Analysis.Complex.Positivity Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Fourier.FourierTransform Mathlib.Probability.Independence.Integrable Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.Convolution Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.Analysis.MellinInversion Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Dynamics.Ergodic.Function Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.BoundedVariation Mathlib.MeasureTheory.Measure.Restrict Mathlib.NumberTheory.WellApproximable Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Probability.Process.Adapted Mathlib.Probability.Distributions.Pareto Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Analysis.Calculus.Rademacher Mathlib.Probability.Independence.Kernel Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Integral.Periodic Mathlib.Probability.Process.Filtration Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.MellinTransform Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Measure.Prod Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Probability.Kernel.Condexp Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.BorelCantelli Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Group.Action Mathlib.Probability.Density Mathlib.Analysis.Complex.OpenMapping Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.ODE.PicardLindelof Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Probability.ConditionalExpectation Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.MeasureTheory.Integral.Indicator Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Measure.Complex Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Probability.UniformOn Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Data.Real.Pi.Wallis Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.Probability.CDF Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.Probability.Martingale.Centering Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient	1
Mathlib.MeasureTheory.Measure.Comap	1298

---

Declarations diff

+ MeasurableEmbedding.comap_add
- comap_add

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

[grunweg]

Thanks! This PR is code motion; I trust that you ported the assumptions over faithfully. (This is a pain to review in the diff --- I really with for better tooling here, this is not about this PR.)
maintainer merge

[github-actions]

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

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style