English
For any f: R → F, the function x ↦ f(∥x∥) is integrable with respect to Haar measure μ if and only if the radial function y ↦ y^(dim E − 1) f(y) is integrable over the positive real axis with respect to the standard measure on (0, ∞).
Русский
Для любой функции f: R → F интегрируемость функции x ↦ f(∥x∥) по мере Хаара μ эквивалентна интегрируемости функции y ↦ y^(dim E − 1) f(y) по мере на оси (0, ∞).
LaTeX
$$$\text{Integrable}(f\circ\lVert\cdot\rVert)\;\mu \iff \text{IntegrableOn}\ (y \mapsto y^{\dim E - 1}\,f(y))\ (\mathrm{Ioi}(0)).$$$
Lean4
theorem integrable_fun_norm_addHaar {f : ℝ → F} :
Integrable (f ‖·‖) μ ↔ IntegrableOn (fun y : ℝ ↦ y ^ (dim E - 1) • f y) (Ioi 0) :=
by
have :=
μ.measurePreserving_homeomorphUnitSphereProd.integrable_comp_emb (g := f ∘ (↑) ∘ Prod.snd)
(Homeomorph.measurableEmbedding _)
simp only [comp_def, homeomorphUnitSphereProd_apply_snd_coe] at this
rw [← restrict_compl_singleton (μ := μ) 0, ← IntegrableOn, integrableOn_iff_comap_subtypeVal (by measurability),
comp_def, this, Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)), integrableOn_iff_comap_subtypeVal,
comp_def, Measure.volumeIoiPow, integrable_withDensity_iff_integrable_smul', integrable_congr]
· refine .of_forall ?_
rintro ⟨x, hx : 0 < x⟩
simp (disch := positivity) [ENNReal.toReal_ofReal]
· fun_prop
· simp
· measurability
· simp
