Documentation
Carleson
.
Classical
.
VanDerCorput
Search
return to top
source
Imports
Init
Carleson.Classical.Basic
Imported by
ContinuousOn
.
intervalIntegrable_Ioo_of_bound
intervalIntegrable_continuous_mul_lipschitzOnWith
van_der_Corput
source
theorem
ContinuousOn
.
intervalIntegrable_Ioo_of_bound
{
a
b
C
:
ℝ
}
{
f
:
ℝ
→
ℂ
}
(
hf
:
ContinuousOn
f
(
Set.Ioo
a
b
)
)
(
hab
:
a
≤
b
)
(
h'f
:
∀
x
∈
Set.Ioo
a
b
,
‖
f
x
‖
≤
C
)
:
IntervalIntegrable
f
MeasureTheory.volume
a
b
source
theorem
intervalIntegrable_continuous_mul_lipschitzOnWith
{
a
b
:
ℝ
}
{
K
:
NNReal
}
{
f
g
:
ℝ
→
ℂ
}
(
hab
:
a
≤
b
)
(
hf
:
Continuous
f
)
(
hg
:
LipschitzOnWith
K
g
(
Set.Ioo
a
b
)
)
:
IntervalIntegrable
(fun (
x
:
ℝ
) =>
f
x
*
g
x
)
MeasureTheory.volume
a
b
source
theorem
van_der_Corput
{
a
b
:
ℝ
}
(
hab
:
a
≤
b
)
{
n
:
ℤ
}
{
ϕ
:
ℝ
→
ℂ
}
{
B
K
:
NNReal
}
(
h1
:
LipschitzOnWith
K
ϕ
(
Set.Ioo
a
b
)
)
(
h2
:
∀
x
∈
Set.Ioo
a
b
,
‖
ϕ
x
‖
≤
↑
B
)
:
‖
∫
(
x
:
ℝ
)
in
a
..
b
,
Complex.exp
(
Complex.I
*
↑
n
*
↑
x
)
*
ϕ
x
‖
≤
2
*
Real.pi
*
(
b
-
a
)
*
(
↑
B
+
↑
K
*
(
b
-
a
)
/
2
)
*
(
1
+
↑
|
n
|
*
(
b
-
a
))
⁻¹