| Carleson/Antichain/AntichainOperator.lean | 15 | 15 | 1 |
| Carleson/Antichain/AntichainTileCount.lean | 69 | 11 | 1 |
| Carleson/Antichain/Basic.lean | 29 | 11 | 2 |
| Carleson/Antichain/TileCorrelation.lean | 32 | 12 | 1 |
| Carleson/Calculations.lean | 29 | 3 | 10 |
| Carleson/Classical/Approximation.lean | 9 | 2 | 2 |
| Carleson/Classical/Basic.lean | 27 | 3 | 6 |
| Carleson/Classical/CarlesonHunt.lean | 7 | 10 | 0 |
| Carleson/Classical/CarlesonHuntBasic.lean | 2 | 1 | 2 |
| Carleson/Classical/CarlesonOnTheRealLine.lean | 2 | 5 | 1 |
| Carleson/Classical/CarlesonOnTheRealLineBasic.lean | 21 | 7 | 2 |
| Carleson/Classical/CarlesonOnTheRealLineContinuous.lean | 2 | 4 | 1 |
| Carleson/Classical/CarlesonOperatorReal.lean | 12 | 1 | 4 |
| Carleson/Classical/ClassicalCarleson.lean | 4 | 7 | 1 |
| Carleson/Classical/ControlApproximationEffect.lean | 9 | 6 | 1 |
| Carleson/Classical/ControlApproximationEffectBasic.lean | 13 | 6 | 2 |
| Carleson/Classical/ControlApproximationEffectContinuous.lean | 13 | 7 | 1 |
| Carleson/Classical/DirichletKernel.lean | 13 | 1 | 2 |
| Carleson/Classical/Helper.lean | 8 | 0 | 2 |
| Carleson/Classical/HilbertKernel.lean | 12 | 1 | 4 |
| Carleson/Classical/HilbertStrongType.lean | 52 | 9 | 2 |
| Carleson/Classical/SpectralProjectionBound.lean | 6 | 1 | 1 |
| Carleson/Classical/VanDerCorput.lean | 3 | 0 | 1 |
| Carleson/Defs.lean | 33 | 0 | 49 |
| Carleson/Discrete/Defs.lean | 81 | 3 | 4 |
| Carleson/Discrete/ExceptionalSet.lean | 41 | 7 | 1 |
| Carleson/Discrete/ForestComplement.lean | 48 | 9 | 1 |
| Carleson/Discrete/ForestUnion.lean | 58 | 11 | 2 |
| Carleson/Discrete/MainTheorem.lean | 4 | 7 | 2 |
| Carleson/DoublingMeasure.lean | 76 | 5 | 31 |
| Carleson/FinitaryCarleson.lean | 10 | 8 | 1 |
| Carleson/Forest.lean | 22 | 1 | 5 |
| Carleson/ForestOperator/AlmostOrthogonality.lean | 16 | 11 | 3 |
| Carleson/ForestOperator/Forests.lean | 56 | 16 | 1 |
| Carleson/ForestOperator/L2Estimate.lean | 33 | 13 | 3 |
| Carleson/ForestOperator/LargeSeparation.lean | 74 | 20 | 1 |
| Carleson/ForestOperator/PointwiseEstimate.lean | 70 | 11 | 5 |
| Carleson/ForestOperator/QuantativeEstimate.lean | 14 | 9 | 2 |
| Carleson/ForestOperator/RemainingTiles.lean | 19 | 18 | 1 |
| Carleson/GridStructure.lean | 62 | 2 | 17 |
| Carleson/HolderNorm.lean | 8 | 0 | 3 |
| Carleson/HolderVanDerCorput.lean | 31 | 6 | 2 |
| Carleson/LipschitzNorm.lean | 8 | 1 | 3 |
| Carleson/MetricCarleson/Basic.lean | 35 | 6 | 3 |
| Carleson/MetricCarleson/Linearized.lean | 6 | 4 | 2 |
| Carleson/MetricCarleson/Main.lean | 18 | 4 | 2 |
| Carleson/MetricCarleson/Truncation.lean | 40 | 12 | 2 |
| Carleson/MinLayerTiles.lean | 4 | 3 | 1 |
| Carleson/Operators.lean | 34 | 4 | 14 |
| Carleson/ProofData.lean | 30 | 2 | 15 |
| Carleson/Psi.lean | 76 | 5 | 12 |
| Carleson/TileExistence.lean | 91 | 7 | 1 |
| Carleson/TileStructure.lean | 90 | 5 | 19 |
| Carleson/ToMathlib/Analysis/Convolution.lean | 5 | 0 | 0 |
| Carleson/ToMathlib/Analysis/Fourier/AddCircle.lean | 2 | 1 | 1 |
| Carleson/ToMathlib/Analysis/RCLike/Components.lean | 18 | 1 | 1 |
| Carleson/ToMathlib/Analysis/RCLike/Misc.lean | 2 | 0 | 1 |
| Carleson/ToMathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean | 1 | 0 | 1 |
| Carleson/ToMathlib/Analysis/SpecialFunctions/Integrals/Basic.lean | 2 | 2 | 1 |
| Carleson/ToMathlib/Annulus.lean | 137 | 1 | 7 |
| Carleson/ToMathlib/BoundedCompactSupport.lean | 44 | 2 | 11 |
| Carleson/ToMathlib/BoundedFiniteSupport.lean | 11 | 1 | 2 |
| Carleson/ToMathlib/CoveredByBalls.lean | 20 | 2 | 0 |
| Carleson/ToMathlib/Data/ENNReal.lean | 14 | 0 | 11 |
| Carleson/ToMathlib/Data/NNReal.lean | 2 | 0 | 3 |
| Carleson/ToMathlib/Distribution.lean | 49 | 1 | 17 |
| Carleson/ToMathlib/ENorm.lean | 11 | 1 | 8 |
| Carleson/ToMathlib/HardyLittlewood.lean | 16 | 5 | 0 |
| Carleson/ToMathlib/IntegralBallContinuity.lean | 5 | 0 | 0 |
| Carleson/ToMathlib/LorentzType.lean | 11 | 11 | 2 |
| Carleson/ToMathlib/MeasureTheory/Function/AEEqFun.lean | 1 | 0 | 1 |
| Carleson/ToMathlib/MeasureTheory/Function/L1Integrable.lean | 2 | 1 | 0 |
| Carleson/ToMathlib/MeasureTheory/Function/LocallyIntegrable.lean | 2 | 0 | 0 |
| Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean | 26 | 14 | 3 |
| Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Defs.lean | 13 | 3 | 5 |
| Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean | 16 | 12 | 2 |
| Carleson/ToMathlib/MeasureTheory/Function/LorentzSpace/Basic.lean | 1 | 3 | 0 |
| Carleson/ToMathlib/MeasureTheory/Function/LpNorm/Misc.lean | 4 | 2 | 2 |
| Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean | 14 | 1 | 6 |
| Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean | 7 | 2 | 1 |
| Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean | 2 | 1 | 2 |
| Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean | 20 | 0 | 3 |
| Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean | 6 | 0 | 3 |
| Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean | 3 | 0 | 0 |
| Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean | 8 | 1 | 3 |
| Carleson/ToMathlib/MeasureTheory/Integral/Layercake.lean | 5 | 3 | 1 |
| Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean | 12 | 0 | 3 |
| Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean | 24 | 2 | 8 |
| Carleson/ToMathlib/MeasureTheory/Integral/Misc.lean | 1 | 1 | 1 |
| Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean | 23 | 1 | 3 |
| Carleson/ToMathlib/MeasureTheory/Measure/AEMeasurable.lean | 5 | 0 | 3 |
| Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean | 28 | 2 | 17 |
| Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean | 55 | 1 | 12 |
| Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Basics.lean | 41 | 1 | 1 |
| Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Defs.lean | 9 | 0 | 4 |
| Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Metric.lean | 1 | 1 | 0 |
| Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Prod.lean | 27 | 1 | 0 |
| Carleson/ToMathlib/MeasureTheory/Measure/Prod.lean | 2 | 0 | 0 |
| Carleson/ToMathlib/MinLayer.lean | 25 | 0 | 4 |
| Carleson/ToMathlib/Misc.lean | 85 | 0 | 31 |
| Carleson/ToMathlib/Order/CompleteLattice/Basic.lean | 1 | 0 | 0 |
| Carleson/ToMathlib/Order/ConditionallyCompleteLattice/Basic.lean | 3 | 0 | 1 |
| Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean | 127 | 0 | 7 |
| Carleson/ToMathlib/RealInterpolation/LorentzInterpolation.lean | 3 | 3 | 1 |
| Carleson/ToMathlib/RealInterpolation/Main.lean | 62 | 7 | 4 |
| Carleson/ToMathlib/RealInterpolation/Minkowski.lean | 41 | 5 | 1 |
| Carleson/ToMathlib/RealInterpolation/Misc.lean | 90 | 3 | 4 |
| Carleson/ToMathlib/Rearrangement.lean | 52 | 6 | 3 |
| Carleson/ToMathlib/Topology/ContinuousOn.lean | 4 | 0 | 1 |
| Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean | 10 | 0 | 3 |
| Carleson/ToMathlib/WeakType.lean | 67 | 7 | 13 |
| Carleson/TwoSidedCarleson/Basic.lean | 8 | 3 | 5 |
| Carleson/TwoSidedCarleson/MainTheorem.lean | 3 | 7 | 3 |
| Carleson/TwoSidedCarleson/NontangentialOperator.lean | 23 | 14 | 1 |
| Carleson/TwoSidedCarleson/RestrictedWeakType.lean | 8 | 9 | 2 |
| Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean | 127 | 11 | 2 |
| Challenge.lean | 3 | 1 | 0 |
| Solution.lean | 3 | 4 | 0 |