Documentation
Carleson
.
ToMathlib
.
Analysis
.
Fourier
.
AddCircle
Search
return to top
source
Imports
Init
Carleson.ToMathlib.Topology.Instances.AddCircle.Defs
Imported by
fourier_comp_equivAddCircle
fourierCoeff_comp_equivAddCircle
source
theorem
fourier_comp_equivAddCircle
{
p
q
:
ℝ
}
[
hp
:
Fact
(
0
<
p
)
]
[
hq
:
Fact
(
0
<
q
)
]
{
x
:
AddCircle
p
}
{
n
:
ℤ
}
:
(
fourier
n
)
(
(
AddCircle.equivAddCircle
p
q
⋯
⋯
)
x
)
=
(
fourier
n
)
x
source
theorem
fourierCoeff_comp_equivAddCircle
{
p
q
:
ℝ
}
[
hp
:
Fact
(
0
<
p
)
]
[
hq
:
Fact
(
0
<
q
)
]
{
f
:
AddCircle
q
→
ℂ
}
{
n
:
ℤ
}
:
fourierCoeff
(fun (
x
:
AddCircle
p
) =>
f
(
(
AddCircle.equivAddCircle
p
q
⋯
⋯
)
x
)
)
n
=
fourierCoeff
f
n