Documentation
Carleson
.
Classical
.
CarlesonOnTheRealLine
Search
return to top
source
Imports
Init
Carleson.Classical.CarlesonOnTheRealLineBasic
Carleson.TwoSidedCarleson.RestrictedWeakType
Imported by
general_carlesonOperator_on_the_reals_hasStrongType
rcarleson'
source
theorem
general_carlesonOperator_on_the_reals_hasStrongType
{
q
:
NNReal
}
(
hq
:
q
∈
Set.Ioo
1
2
)
:
MeasureTheory.HasStrongType
(
carlesonOperator
K
)
(↑
q
)
(↑
q
)
MeasureTheory.volume
MeasureTheory.volume
↑
(
C_carleson_hasStrongType
4
q
)
source
theorem
rcarleson'
{
q
:
NNReal
}
(
hq
:
q
∈
Set.Ioo
1
2
)
{
f
:
ℝ
→
ℂ
}
(
hf
:
MeasureTheory.MemLp
f
(↑
q
)
MeasureTheory.volume
)
:
MeasureTheory.eLpNorm
(
carlesonOperatorReal
K
f
)
(↑
q
)
MeasureTheory.volume
≤
↑
(
C_carleson_hasStrongType
4
q
)
*
MeasureTheory.eLpNorm
f
(↑
q
)
MeasureTheory.volume