Documentation

Carleson.ToMathlib.MeasureTheory.Integral.SetIntegral

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‖₊ μ