Documentation
Carleson
.
ToMathlib
.
MeasureTheory
.
Integral
.
SetIntegral
Search
return to top
source
Imports
Init
Mathlib.MeasureTheory.Integral.SetIntegral
Imported by
Carleson.ForestOperator.Forests
Carleson
ennnorm_integral_starRingEnd_mul_eq_lintegral_ennnorm
source
theorem
ennnorm_integral_starRingEnd_mul_eq_lintegral_ennnorm
{𝕜 :
Type
u_1}
[
RCLike
𝕜
]
{α :
Type
u_2}
[
MeasurableSpace
α
]
{μ :
MeasureTheory.Measure
α
}
{f :
α
→
𝕜
}
(hf :
MeasureTheory.Integrable
f
μ
)
:
↑
‖
∫
(
x
:
α
)
,
(
starRingEnd
𝕜
)
(
f
x
/
↑
‖
f
x
‖
)
*
f
x
∂
μ
‖₊
=
∫⁻
(
x
:
α
)
,
↑
‖
f
x
‖₊
∂
μ