-
Notifications
You must be signed in to change notification settings - Fork 39
Expand file tree
/
Copy pathCarleson.lean
More file actions
106 lines (106 loc) · 4.81 KB
/
Carleson.lean
File metadata and controls
106 lines (106 loc) · 4.81 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
import Carleson.Antichain.AntichainOperator
import Carleson.Antichain.AntichainTileCount
import Carleson.Antichain.Basic
import Carleson.Antichain.TileCorrelation
import Carleson.Calculations
import Carleson.Classical.Approximation
import Carleson.Classical.Basic
import Carleson.Classical.CarlesonHunt
import Carleson.Classical.CarlesonOnTheRealLine
import Carleson.Classical.CarlesonOperatorReal
import Carleson.Classical.ClassicalCarleson
import Carleson.Classical.ControlApproximationEffect
import Carleson.Classical.DirichletKernel
import Carleson.Classical.Helper
import Carleson.Classical.HilbertKernel
import Carleson.Classical.HilbertStrongType
import Carleson.Classical.SpectralProjectionBound
import Carleson.Classical.VanDerCorput
import Carleson.Defs
import Carleson.Discrete.Defs
import Carleson.Discrete.ExceptionalSet
import Carleson.Discrete.ForestComplement
import Carleson.Discrete.ForestUnion
import Carleson.Discrete.MainTheorem
import Carleson.Discrete.SumEstimates
import Carleson.DoublingMeasure
import Carleson.FinitaryCarleson
import Carleson.Forest
import Carleson.ForestOperator.AlmostOrthogonality
import Carleson.ForestOperator.Forests
import Carleson.ForestOperator.L2Estimate
import Carleson.ForestOperator.LargeSeparation
import Carleson.ForestOperator.PointwiseEstimate
import Carleson.ForestOperator.QuantativeEstimate
import Carleson.ForestOperator.RemainingTiles
import Carleson.GridStructure
import Carleson.HolderNorm
import Carleson.HolderVanDerCorput
import Carleson.LipschitzNorm
import Carleson.MetricCarleson.Basic
import Carleson.MetricCarleson.Linearized
import Carleson.MetricCarleson.Main
import Carleson.MetricCarleson.Truncation
import Carleson.MinLayerTiles
import Carleson.Operators
import Carleson.ProofData
import Carleson.Psi
import Carleson.TileExistence
import Carleson.TileStructure
import Carleson.ToMathlib.Analysis.Convolution
import Carleson.ToMathlib.Analysis.MeanInequalitiesPow
import Carleson.ToMathlib.Annulus
import Carleson.ToMathlib.BoundedCompactSupport
import Carleson.ToMathlib.BoundedFiniteSupport
import Carleson.ToMathlib.CoveredByBalls
import Carleson.ToMathlib.Data.ENNReal
import Carleson.ToMathlib.Data.Finset.Lattice.Fold
import Carleson.ToMathlib.Data.NNReal
import Carleson.ToMathlib.Data.Real.ConjExponents
import Carleson.ToMathlib.ENorm
import Carleson.ToMathlib.HardyLittlewood
import Carleson.ToMathlib.Interval
import Carleson.ToMathlib.LorentzType
import Carleson.ToMathlib.MeasureTheory.Function.AEEqFun
import Carleson.ToMathlib.MeasureTheory.Function.L1Integrable
import Carleson.ToMathlib.MeasureTheory.Function.LocallyIntegrable
import Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic
import Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Defs
import Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality
import Carleson.ToMathlib.MeasureTheory.Function.LorentzSpace.Basic
import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic
import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
import Carleson.ToMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
import Carleson.ToMathlib.MeasureTheory.Function.LpSpace.Indicator
import Carleson.ToMathlib.MeasureTheory.Function.SimpleFunc
import Carleson.ToMathlib.MeasureTheory.Integral.Average
import Carleson.ToMathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
import Carleson.ToMathlib.MeasureTheory.Integral.IntegrableOn
import Carleson.ToMathlib.MeasureTheory.Integral.Lebesgue
import Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities
import Carleson.ToMathlib.MeasureTheory.Integral.Periodic
import Carleson.ToMathlib.MeasureTheory.Measure.AEMeasurable
import Carleson.ToMathlib.MeasureTheory.Measure.ENNReal
import Carleson.ToMathlib.MeasureTheory.Measure.Haar.Unique
import Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling
import Carleson.ToMathlib.MeasureTheory.Measure.NNReal
import Carleson.ToMathlib.MeasureTheory.Measure.Prod
import Carleson.ToMathlib.MinLayer
import Carleson.ToMathlib.Misc
import Carleson.ToMathlib.Order.CompleteLattice.Basic
import Carleson.ToMathlib.Order.ConditionallyCompleteLattice.Basic
import Carleson.ToMathlib.Order.LiminfLimsup
import Carleson.ToMathlib.RealInterpolation.InterpolatedExponents
import Carleson.ToMathlib.RealInterpolation.LorentzInterpolation
import Carleson.ToMathlib.RealInterpolation.Main
import Carleson.ToMathlib.RealInterpolation.Minkowski
import Carleson.ToMathlib.RealInterpolation.Misc
import Carleson.ToMathlib.Rearrangement
import Carleson.ToMathlib.Topology.Instances.AddCircle.Defs
import Carleson.ToMathlib.Topology.Order.Basic
import Carleson.ToMathlib.WeakType
import Carleson.TwoSidedCarleson.Basic
import Carleson.TwoSidedCarleson.MainTheorem
import Carleson.TwoSidedCarleson.NontangentialOperator
import Carleson.TwoSidedCarleson.RestrictedWeakType
import Carleson.TwoSidedCarleson.WeakCalderonZygmund