integrablePower — Mathlib

English

For a measure μ with temperate growth, the function x ↦ (1+‖x‖)^(-μ.integrablePower) is integrable over the measure space.

Русский

Для меры μ с темперированным ростом функция x ↦ (1+‖x‖)^(- μ.integrablePower) интегрируема по μ.

LaTeX

$$$\\int (1+‖x‖)^{-(μ.integrablePower)}\,dμ(x) < \\infty$ (in the appropriate measure-theoretic sense).$$

Lean4

/-- An integer exponent `l` such that `(1 + ‖x‖) ^ (-l)` is integrable if `μ` has
temperate growth. -/
def _root_.MeasureTheory.Measure.integrablePower (μ : Measure D) : ℕ :=
  if h : μ.HasTemperateGrowth then h.exists_integrable.choose else 0

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