volumeIoiPow — Mathlib

English

Define a family of measures on (0,∞) with density r^n with respect to Lebesgue measure, via a pullback from the volume measure on (0,∞).

Русский

Задаётся семейство мер на (0,∞) с плотностью r^n по отношению к мерe Лебегa через тяготение от объёма на (0,∞).

LaTeX

$$$\\mathrm{volumeIoiPow}(n) = (\\mathrm{volume} \\circ \\mathrm{subtype.val})^{-1}\\, \\text{with density } r \\mapsto r^n$$$

Lean4

/-- The measure on `(0, +∞)` that has density `(· ^ n)` with respect to the Lebesgue measure. -/
def volumeIoiPow (n : ℕ) : Measure (Ioi (0 : ℝ)) :=
  .withDensity (.comap Subtype.val volume) fun r ↦ .ofReal (r.1 ^ n)

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