Map

How this project builds on itself. An arrow goes from a file to a file that uses something in it, so the foundations are on the left. These links come from names in the source code, not from kernel dependency facts; the separate Trust page says exactly what Lean checked. every declaration's own map, on its file page, shows the same thing one result at a time.

Files as a table

The same map data in a searchable keyboard- and screen-reader-friendly form.

Files and cross-file dependency counts
FileDeclarationsBuilds onUsed by
Carleson/Antichain/AntichainOperator.lean15151
Carleson/Antichain/AntichainTileCount.lean69111
Carleson/Antichain/Basic.lean29112
Carleson/Antichain/TileCorrelation.lean32121
Carleson/Calculations.lean29310
Carleson/Classical/Approximation.lean922
Carleson/Classical/Basic.lean2736
Carleson/Classical/CarlesonHunt.lean7100
Carleson/Classical/CarlesonHuntBasic.lean212
Carleson/Classical/CarlesonOnTheRealLine.lean251
Carleson/Classical/CarlesonOnTheRealLineBasic.lean2172
Carleson/Classical/CarlesonOnTheRealLineContinuous.lean241
Carleson/Classical/CarlesonOperatorReal.lean1214
Carleson/Classical/ClassicalCarleson.lean471
Carleson/Classical/ControlApproximationEffect.lean961
Carleson/Classical/ControlApproximationEffectBasic.lean1362
Carleson/Classical/ControlApproximationEffectContinuous.lean1371
Carleson/Classical/DirichletKernel.lean1312
Carleson/Classical/Helper.lean802
Carleson/Classical/HilbertKernel.lean1214
Carleson/Classical/HilbertStrongType.lean5292
Carleson/Classical/SpectralProjectionBound.lean611
Carleson/Classical/VanDerCorput.lean301
Carleson/Defs.lean33049
Carleson/Discrete/Defs.lean8134
Carleson/Discrete/ExceptionalSet.lean4171
Carleson/Discrete/ForestComplement.lean4891
Carleson/Discrete/ForestUnion.lean58112
Carleson/Discrete/MainTheorem.lean472
Carleson/DoublingMeasure.lean76531
Carleson/FinitaryCarleson.lean1081
Carleson/Forest.lean2215
Carleson/ForestOperator/AlmostOrthogonality.lean16113
Carleson/ForestOperator/Forests.lean56161
Carleson/ForestOperator/L2Estimate.lean33133
Carleson/ForestOperator/LargeSeparation.lean74201
Carleson/ForestOperator/PointwiseEstimate.lean70115
Carleson/ForestOperator/QuantativeEstimate.lean1492
Carleson/ForestOperator/RemainingTiles.lean19181
Carleson/GridStructure.lean62217
Carleson/HolderNorm.lean803
Carleson/HolderVanDerCorput.lean3162
Carleson/LipschitzNorm.lean813
Carleson/MetricCarleson/Basic.lean3563
Carleson/MetricCarleson/Linearized.lean642
Carleson/MetricCarleson/Main.lean1842
Carleson/MetricCarleson/Truncation.lean40122
Carleson/MinLayerTiles.lean431
Carleson/Operators.lean34414
Carleson/ProofData.lean30215
Carleson/Psi.lean76512
Carleson/TileExistence.lean9171
Carleson/TileStructure.lean90519
Carleson/ToMathlib/Analysis/Convolution.lean500
Carleson/ToMathlib/Analysis/Fourier/AddCircle.lean211
Carleson/ToMathlib/Analysis/RCLike/Components.lean1811
Carleson/ToMathlib/Analysis/RCLike/Misc.lean201
Carleson/ToMathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean101
Carleson/ToMathlib/Analysis/SpecialFunctions/Integrals/Basic.lean221
Carleson/ToMathlib/Annulus.lean13717
Carleson/ToMathlib/BoundedCompactSupport.lean44211
Carleson/ToMathlib/BoundedFiniteSupport.lean1112
Carleson/ToMathlib/CoveredByBalls.lean2020
Carleson/ToMathlib/Data/ENNReal.lean14011
Carleson/ToMathlib/Data/NNReal.lean203
Carleson/ToMathlib/Distribution.lean49117
Carleson/ToMathlib/ENorm.lean1118
Carleson/ToMathlib/HardyLittlewood.lean1650
Carleson/ToMathlib/IntegralBallContinuity.lean500
Carleson/ToMathlib/LorentzType.lean11112
Carleson/ToMathlib/MeasureTheory/Function/AEEqFun.lean101
Carleson/ToMathlib/MeasureTheory/Function/L1Integrable.lean210
Carleson/ToMathlib/MeasureTheory/Function/LocallyIntegrable.lean200
Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean26143
Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Defs.lean1335
Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean16122
Carleson/ToMathlib/MeasureTheory/Function/LorentzSpace/Basic.lean130
Carleson/ToMathlib/MeasureTheory/Function/LpNorm/Misc.lean422
Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean1416
Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean721
Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean212
Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean2003
Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean603
Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean300
Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean813
Carleson/ToMathlib/MeasureTheory/Integral/Layercake.lean531
Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean1203
Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean2428
Carleson/ToMathlib/MeasureTheory/Integral/Misc.lean111
Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean2313
Carleson/ToMathlib/MeasureTheory/Measure/AEMeasurable.lean503
Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean28217
Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean55112
Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Basics.lean4111
Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Defs.lean904
Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Metric.lean110
Carleson/ToMathlib/MeasureTheory/Measure/NoAtoms/Prod.lean2710
Carleson/ToMathlib/MeasureTheory/Measure/Prod.lean200
Carleson/ToMathlib/MinLayer.lean2504
Carleson/ToMathlib/Misc.lean85031
Carleson/ToMathlib/Order/CompleteLattice/Basic.lean100
Carleson/ToMathlib/Order/ConditionallyCompleteLattice/Basic.lean301
Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean12707
Carleson/ToMathlib/RealInterpolation/LorentzInterpolation.lean331
Carleson/ToMathlib/RealInterpolation/Main.lean6274
Carleson/ToMathlib/RealInterpolation/Minkowski.lean4151
Carleson/ToMathlib/RealInterpolation/Misc.lean9034
Carleson/ToMathlib/Rearrangement.lean5263
Carleson/ToMathlib/Topology/ContinuousOn.lean401
Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean1003
Carleson/ToMathlib/WeakType.lean67713
Carleson/TwoSidedCarleson/Basic.lean835
Carleson/TwoSidedCarleson/MainTheorem.lean373
Carleson/TwoSidedCarleson/NontangentialOperator.lean23141
Carleson/TwoSidedCarleson/RestrictedWeakType.lean892
Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean127112
Challenge.lean310
Solution.lean340