setIntegral_compLp — Mathlib

English

If a map preserves scalar multiplication, then integral with L is equal to integral of L applied to φ.

Русский

Если отображение сохраняет умножение на скаляры, то интеграл от L(φ) равен L от интеграла φ.

LaTeX

$$$\\int φ = L(\\int φ)$$$

Lean4

theorem setIntegral_compLp (L : E →SL[σ] F) (φ : Lp E p μ) {s : Set X} (hs : MeasurableSet s) :
    ∫ x in s, (L.compLp φ) x ∂μ = ∫ x in s, L (φ x) ∂μ :=
  setIntegral_congr_ae hs ((L.coeFn_compLp φ).mono fun _x hx _ => hx)

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