aestronglyMeasurable_rpowIntegrand₀₁

English

Let p ∈ (0,1) and x ≥ 0. Then the map t ↦ (rpowIntegrand₀₁ p t) · x is AEStronglyMeasurable with respect to the restricted volume on (0, ∞). In other words, the function t ↦ x · rpowIntegrand₀₁(p,t) is AEStronglyMeasurable on (0,∞) under the Lebesgue measure restricted to (0,∞).

Русский

Пусть p ∈ (0,1) и x ≥ 0. Тогда отображение t ↦ (rpowIntegrand₀₁ p t) · x является AES-сильно измеримым относительно ограниченной объёмной меры на (0, ∞). Другими словами, функция t ↦ x · rpowIntegrand₀₁(p,t) измерима на (0,∞) по ограниченной мере Лебега.

LaTeX

$$$\\mathrm{AEStronglyMeasurable}\\bigl((rpowIntegrand_{01}\\,p)\\cdot x\\bigr)\\bigl(\\mathrm{volume}\\restriction (I^+_0)\\bigr)$$$

Lean4

theorem aestronglyMeasurable_rpowIntegrand₀₁ (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
    AEStronglyMeasurable (rpowIntegrand₀₁ p · x) (volume.restrict (Ioi 0)) :=
  (continuousOn_rpowIntegrand₀₁ hp hx).aestronglyMeasurable measurableSet_Ioi

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