Upstreaming dashboard
Files ready to upstream
The following files are sorry-free and do not depend on any other files, meaning they can be readily PRed to Mathlib.
Carleson.HolderNormCarleson.Discrete.SumEstimatesCarleson.Classical.VanDerCorputCarleson.Classical.HelperCarleson.ToMathlib.MinLayerCarleson.ToMathlib.BoundedFiniteSupportCarleson.ToMathlib.ENormCarleson.ToMathlib.IntervalCarleson.ToMathlib.Order.LiminfLimsupCarleson.ToMathlib.RealInterpolation.InterpolatedExponentsCarleson.ToMathlib.Data.ENNRealCarleson.ToMathlib.Data.NNRealCarleson.ToMathlib.Analysis.ConvolutionCarleson.ToMathlib.Topology.Order.BasicCarleson.ToMathlib.Topology.Instances.AddCircle.DefsCarleson.ToMathlib.Order.ConditionallyCompleteLattice.BasicCarleson.ToMathlib.MeasureTheory.Integral.IntegrableOnCarleson.ToMathlib.MeasureTheory.Integral.AverageCarleson.ToMathlib.MeasureTheory.Integral.LebesgueCarleson.ToMathlib.MeasureTheory.Measure.ProdCarleson.ToMathlib.MeasureTheory.Measure.ENNRealCarleson.ToMathlib.MeasureTheory.Measure.NNRealCarleson.ToMathlib.MeasureTheory.Function.SimpleFuncCarleson.ToMathlib.MeasureTheory.Function.LocallyIntegrableCarleson.ToMathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMapCarleson.ToMathlib.MeasureTheory.Measure.Haar.UniqueCarleson.ToMathlib.MeasureTheory.Function.LpSpace.IndicatorCarleson.ToMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctionsCarleson.ToMathlib.Data.Real.ConjExponentsCarleson.ToMathlib.Data.Finset.Lattice.Fold
Files easy to unlock
The following files do not depend on any other Carleson file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.