integral_compLp — Mathlib

English

For a subspace L and φ in Lp, the integral over a set s equals the integral of φ restricted to s.

Русский

Для подпространства L и φ в Lp интеграл по множеству s равен интегралу по ограничению φ на s.

LaTeX

$$$\\int_{s} φ(x) dμ = \\int φ(x) d(μ|_{s})$$$

Lean4

theorem integral_compLp (L : E →SL[σ] F) (φ : Lp E p μ) : ∫ x, (L.compLp φ) x ∂μ = ∫ x, L (φ x) ∂μ :=
  integral_congr_ae <| coeFn_compLp _ _

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