integral_fun_norm_addHaar — Mathlib

English

For all f: R → F, the integral over E of f(∥x∥) with respect to Haar measure μ equals (dim E) times the real measure of the unit ball times the radial integral ∫_{0}^{∞} y^(dim E − 1) f(y) dy.

Русский

При интегрировании по мере Хаара μ функция f(∥x∥) по объему равна (dim E) · μ(ball(0,1)) × интеграл по оси (0, ∞) от y^(dim E−1) f(y).

LaTeX

$$$\int_{E} f(\|x\|)\,d\mu(x) = \dim(E)\, \mu(\text{real}(\text{ball}(0,1)))\; \int_{0}^{\infty} y^{\dim(E)-1}\,f(y)\,dy.$$$

Lean4

theorem integral_fun_norm_addHaar (f : ℝ → F) :
    ∫ x, f (‖x‖) ∂μ = dim E • μ.real (ball 0 1) • ∫ y in Ioi (0 : ℝ), y ^ (dim E - 1) • f y :=
  calc
    ∫ x, f (‖x‖) ∂μ = ∫ x : ({(0)}ᶜ : Set E), f (‖x.1‖) ∂(μ.comap (↑)) := by
      rw [integral_subtype_comap (measurableSet_singleton _).compl fun x ↦ f (‖x‖), restrict_compl_singleton]
    _ = ∫ x : sphere (0 : E) 1 × Ioi (0 : ℝ), f x.2 ∂μ.toSphere.prod (.volumeIoiPow (dim E - 1)) :=
      (μ.measurePreserving_homeomorphUnitSphereProd.integral_comp (Homeomorph.measurableEmbedding _)
        (f ∘ Subtype.val ∘ Prod.snd))
    _ = μ.toSphere.real univ • ∫ x : Ioi (0 : ℝ), f x ∂.volumeIoiPow (dim E - 1) := (integral_fun_snd (f ∘ Subtype.val))
    _ = _ := by
      simp only [Measure.volumeIoiPow, ENNReal.ofReal]
      rw [integral_withDensity_eq_integral_smul, μ.toSphere_real_apply_univ, ← nsmul_eq_mul, smul_assoc,
        integral_subtype_comap measurableSet_Ioi fun a ↦ Real.toNNReal (a ^ (dim E - 1)) • f a,
        setIntegral_congr_fun measurableSet_Ioi fun x hx ↦ ?_]
      · rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hx.out.le _)]
      · exact (measurable_subtype_coe.pow_const _).real_toNNReal

Похожие утверждения